Constructing the constructible universe constructively

DOI10.1016/j.apal.2023.103392arXiv2206.08283OpenAlexW4389430687MaRDI QIDQ6145038

Michael Rathjen, Richard Matthews

Publication date: 8 January 2024

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

constructive mathematicsconstructible universeconstructive Zermelo-Fraenkelintuitionistic Kripke-Platekintuitionistic Zermelo-Fraenkel

Mathematics Subject Classification ID

Inner models, including constructibility, ordinal definability, and core models (03E45) Nonclassical and second-order set theories (03E70) Ordinal and cardinal numbers (03E10) Intuitionistic mathematics (03F55) Higher-type and set recursion theory (03D65)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• From the weak to the strong existence property
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Power set recursion
• Rudimentary and arithmetical constructive set theory
• Rudimentary recursion, gentle functions and provident sets
• Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory
• Axiom of Choice and Complementation
• Set Theory
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Consistency of the Continuum Hypothesis. (AM-3)
• The strength of Mac Lane set theory