TL;DR
This paper employs classical realizability to construct models of ZF + DC where the real numbers are not well ordered, providing new consistency results and a novel approach to program extraction from proofs involving dependent choice.
Contribution
It introduces a new method using classical realizability to build models of set theory with specific properties and derives programs from proofs with dependent choice.
Findings
Constructed models of ZF + DC where R is not well ordered.
Provided alternative consistency results beyond forcing.
Developed a new method for program extraction from proofs.
Abstract
We use the technique of "classical realizability" to build new models of ZF + DC in which R is not well ordered. This gives new relative consistency results, probably not obtainable by forcing. This gives also a new method to get programs from proofs of arithmetical formulas with dependent choice.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.