Well-foundedness in realizability

DOI10.1007/s00153-006-0003-5zbMath1112.03058OpenAlexW2103412807MaRDI QIDQ850808

Jaap van Oosten, Thomas Streicher, Martin Hofmann

Publication date: 6 November 2006

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://dspace.library.uu.nl/handle/1874/15457

zbMATH Keywords

effective toposrealizability toposglobal sections functorgeneralized Markov principlewell-foundedness of binary relations

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Intuitionistic mathematics (03F55)

Related Items

Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, Constructive hybrid games

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A presentation of the initial lift-algebra
• Axiomatizing higher-order Kleene realizability
• Wellfounded trees in categories
• Axioms and (counter)examples in synthetic domain theory
• Intuitionistically provable recursive well-orderings
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Words, free algebras, and coequalizers
• Number theoretic concepts and recursive well-orderings
• Algebraic set theory and the effective topos
• On the concepts of completeness and interpretation of formal systems