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 (28)

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

This page was built for publication: Notation systems for infinitary derivations