Notation systems for infinitary derivations

DOI10.1007/BF01621472zbMath0726.03038OpenAlexW2068743712MaRDI QIDQ2277451

Wilfried Buchholz

Publication date: 1991

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01621472

zbMATH Keywords

Peano arithmeticreduction operatortransfinite inductioninversion operator\(\omega \) -arithmeticcut-elimination operatorinfinite derivationsnotation system

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

1998 European Summer Meeting of the Association for Symbolic Logic, How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study, Proof theory of reflection, A NOTE ON FRAGMENTS OF UNIFORM REFLECTION IN SECOND ORDER ARITHMETIC, A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH, Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones, Slow reflection, Short proofs for slow consistency, AN INCOMPLETENESS THEOREM VIA ORDINAL ANALYSIS, A termination proof for epsilon substitution using partial derivations, Mining the surface: witnessing the low complexity theorems of arithmetic, On the computational complexity of cut-reduction, Type-theoretic approaches to ordinals, How to characterize provably total functions by local predicativity, A note on iterated consistency and infinite proofs, The consistency of arithmetic, Intuitionistic fixed point theories over set theories, Proof lengths for instances of the Paris-Harrington principle, Cut elimination for a simple formulation of epsilon calculus, 2006 Summer Meeting of the Association for Symbolic Logic: Logic Colloquium '06, Continuous normalization for the lambda-calculus and Gödel's T, \(\Pi_1^1\)-comprehension as a well-ordering principle, Proof theory and ordinal analysis, A Characterisation of Definable NP Search Problems in Peano Arithmetic, Reduction of finite and infinite derivations, Completeness of the primitive recursive \(\omega \)-rule, Finite notations for infinite terms, Classifying the Provably Total Functions of PA

Cites Work

• Proof-theoretical analysis: Weak systems of functions and classes
• Proof theory. 2nd ed
• Finite investigations of transfinite derivations
• Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• A survey of proof theory
• The consistency of arithmetics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item