Realizability algebras III: some examples
Logic in Computer Science
2018-03-20 v2 Logic
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.
Cite
@article{arxiv.1210.5065,
title = {Realizability algebras III: some examples},
author = {Jean-Louis Krivine},
journal= {arXiv preprint arXiv:1210.5065},
year = {2018}
}
Comments
30 pages