Realizability algebras III: some examples
arXiv:1210.5065 · doi:10.1017/S0960129516000050
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.
30 pages