Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory

DOI10.1007/978-3-319-29198-7_4zbMath1439.03108arXiv1603.03358OpenAlexW2296270830WikidataQ59893880 ScholiaQ59893880MaRDI QIDQ3305554

Jacob Cook, Michael Rathjen

Publication date: 7 August 2020

Published in: Advances in Proof Theory (Search for Journal in Brave)

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

zbMATH Keywords

proof-theoretic ordinalsexistential dimensionintuitionistic powerordination analysispowerset axiom

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Nonclassical and second-order set theories (03E70) Recursive ordinals and ordinal notations (03F15) Intuitionistic mathematics (03F55)

Related Items

Constructing the constructible universe constructively

Cites Work

• 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
• A new system of proof-theoretic ordinal functions
• Proof theory of reflection
• An ordinal analysis of parameter free \(\Pi^{1}_{2}\)-comprehension
• Proof theory for theories of ordinals. II: \(\Pi_{3}\)-reflection
• Characterizing the interpretation of set theory in Martin-Löf type theory
• CZF does not have the existence property
• Beweistheorie vonKPN
• Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
• How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item