LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION

DOI10.1017/jsl.2021.1zbMath1485.03222arXiv1806.10047OpenAlexW2810870528MaRDI QIDQ5858930

Andrew Swan, Michael Rathjen

Publication date: 15 April 2021

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1806.10047

zbMATH Keywords

realizabilityconstructive set theorytopological models

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Other constructive mathematics (03F65) Metamathematics of constructive systems (03F50)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• Basic subtoposes of the effective topos
• Polynomials and linear transformations
• Realizability. An introduction to its categorical side
• Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory
• Heyting-valued interpretations for constructive set theory
• SEPARATING FRAGMENTS OF WLEM, LPO, AND MP
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Lifschitz' realizability
• The disjunction property implies the numerical existence property
• CT 0 is Stronger than CT 0 !
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• Propositions as [Types]
• Two remarks on the Lifschitz realizability topos
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• The Herbrand topos