Cut-elimination for impredicative infinitary systems part I. Ordinal-analysis for ID1

DOI10.1007/BF02011638zbMath0484.03030OpenAlexW1992414919MaRDI QIDQ3942955

Wolfram Pohlers

Publication date: 1981

Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/137980

zbMATH Keywords

noniterated generalized inductive definitions

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Inductive definability (03D70)

Related Items (7)

Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen ⋮ Simplified Cut Elimination for Kripke-Platek Set Theory ⋮ Epsilon substitution for \(ID_1\) via cut-elimination ⋮ From Subsystems of Analysis to Subsystems of Set Theory ⋮ Ordinal analysis of non-monotone \(\Pi_1^0\)-definable inductive definitions ⋮ Ordinal analysis by transformations ⋮ Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results

Cites Work

• Consistency proofs of subsystems of classical analysis
• Beweistheorie vonKPN
• A simplification of the Bachmann method for generating large countable ordinals
• Über Teilsysteme von $$\bar \Theta $$ ({g})
• Ordinals connected with formal theories for transfinitely iterated inductive definitions
• Provable wellorderings of formal theories for transfinitely iterated inductive definitions
• Systems of predicative analysis
• A system of abstract constructive ordinals
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Cut-elimination for impredicative infinitary systems part I. Ordinal-analysis for ID1