scientific article
From MaRDI portal
Publication:3138829
zbMath0795.03078MaRDI QIDQ3138829
Publication date: 1 September 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
ordinal analysiscollapsing functionlocal predicativityconstructible hierarchyweakly inaccessible cardinaladmissible proof theoryimpredicative cut elimination theoreminfinitary proof system for a ramified set theoryKripke- Platek theory of admissible sets with iteration
Cut-elimination and normal-form theorems (03F05) Recursive ordinals and ordinal notations (03F15) Complexity of proofs (03F20) Set theory (03E99)
Related Items
Proof theory of reflection, Simplified Cut Elimination for Kripke-Platek Set Theory, On the Performance of Axiom Systems, Primitive recursive analogues of regular cardinals based on ordinal representation systems for KPi and KPM, Relativized ordinal analysis: the case of power Kripke-Platek set theory, Proof theory for theories of ordinals. I: Recursively Mahlo ordinals, Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory, From Subsystems of Analysis to Subsystems of Set Theory, On Relating Theories: Proof-Theoretical Reduction, Ordinal analysis of non-monotone \(\Pi_1^0\)-definable inductive definitions, An ordinal analysis of stability, An ordinal analysis of parameter free \(\Pi^{1}_{2}\)-comprehension, \(\Pi_1^1\)-comprehension as a well-ordering principle, Notes on some second-order systems of iterated inductive definitions and \(\Pi_1^1\)-comprehensions and relevant subsystems of set theory, Cut-elimination for \(\omega_{1}\), Pure \(\Sigma_2\)-elementarity beyond the core, Iterated Inductive Definitions Revisited, Proof Theory of Constructive Systems: Inductive Types and Univalence, Patterns of resemblance of order 2, Functional interpretation of Aczel's constructive set theory, Well-ordering proofs for Martin-Löf type theory, A SIMPLIFIED ORDINAL ANALYSIS OF FIRST-ORDER REFLECTION, Cut-Elimination for SBL, An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe, A Glimpse of $$ \sum_{3} $$-elementarity, Zur Beweistheorie Von KPM, Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM