scientific article

zbMath0795.03078MaRDI QIDQ3138829

Wilfried Buchholz

Publication date: 1 September 1994

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

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

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Recursive ordinals and ordinal notations (03F15) Complexity of proofs (03F20) Set theory (03E99)

Related Items (27)

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

This page was built for publication: