Constructing the constructible universe constructively

DOI10.1016/J.APAL.2023.103392MaRDI QIDQ6145038zbMATH OpenOpenAlexFDO

Authors Richard Matthews, Michael Rathjen

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

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

Abstract: We study the properties of the constructible universe, L, over intuitionistic theories. We give an extended set of fundamental operations which is sufficient to generate the universe over Intuitionistic Kripke-Platek set theory without Infinity. Following this, we investigate when L can fail to be an inner model in the traditional sense. Namely, we show that over Constructive Zermelo-Fraenkel (even with the Power Set axiom) one cannot prove that the Axiom of Exponentiation holds in L.

Cites work

• scientific article; zbMATH DE number 2184445 (Why is no real title available?)
• scientific article; zbMATH DE number 3861143 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 194101 (Why is no real title available?)
• scientific article; zbMATH DE number 749933 (Why is no real title available?)
• scientific article; zbMATH DE number 3370318 (Why is no real title available?)
• Axiom of Choice and Complementation
• Consistency of the Continuum Hypothesis. (AM-3)
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• From the weak to the strong existence property
• Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
• Power set recursion
• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• Rudimentary and arithmetical constructive set theory
• Rudimentary recursion, gentle functions and provident sets
• Set Theory
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• The strength of Mac Lane set theory
• Weak systems of Gandy, Jensen and Devlin

Cited in

(1)

• Very large set axioms over constructive set theories

This page was built for publication: Constructing the constructible universe constructively

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6145038)