Notation systems for infinitary derivations

DOI10.1007/BF01621472MaRDI QIDQ2277451zbMATH OpenOpenAlexFDO

Authors 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 arithmetictransfinite inductionreduction operatorinversion operator\(\omega \) -arithmeticcut-elimination operatorinfinite derivationsnotation system

Mathematics Subject Classification ID

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

Recommendations

• Finite notations for infinite terms
• Explaining the Gentzen-Takeuti reduction steps: A second-order system
• Reduction of finite and infinite derivations
• Some results on cut-elimination, provable well-orderings, induction and reflection
• Finitary treatment of operator controlled derivations

Cites work

• scientific article; zbMATH DE number 3167150 (Why is no real title available?)
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 4033742 (Why is no real title available?)
• scientific article; zbMATH DE number 4068861 (Why is no real title available?)
• scientific article; zbMATH DE number 3497842 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• A survey of proof theory
• Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
• Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie
• Finite investigations of transfinite derivations
• Proof theory. 2nd ed
• Proof-theoretical analysis: Weak systems of functions and classes
• The consistency of arithmetics

Cited in

(37)

• Type-theoretic approaches to ordinals
• A termination proof for epsilon substitution using partial derivations
• Fundamental sequences and fast-growing hierarchies for the Bachmann-Howard ordinal
• How to characterize provably total functions by local predicativity
• 1998 European Summer Meeting of the Association for Symbolic Logic
• A Characterisation of Definable NP Search Problems in Peano Arithmetic
• Proof theory of reflection
• Proof theory and ordinal analysis
• 2006 Summer Meeting of the Association for Symbolic Logic: Logic Colloquium '06
• Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones
• Mining the surface: witnessing the low complexity theorems of arithmetic
• Infix and postfix notations
• Slow reflection
• How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
• Reduction of finite and infinite derivations
• Cut elimination for a simple formulation of epsilon calculus
• Further applications of ultra-conservative ω-rules
• Finite notations for infinite terms
• Peano arithmetic, games and descent recursion
• Classifying the Provably Total Functions of PA
• scientific article; zbMATH DE number 3941504 (Why is no real title available?)
• scientific article; zbMATH DE number 1420858 (Why is no real title available?)
• Reflection ranks via infinitary derivations
• On the computational complexity of cut-reduction
• A note on iterated consistency and infinite proofs
• Short proofs for slow consistency
• Finitary treatment of operator controlled derivations
• Witnessing flows in arithmetic
• Intuitionistic fixed point theories over set theories
• Completeness of the primitive recursive \(\omega \)-rule
• \(\Pi_1^1\)-comprehension as a well-ordering principle
• Continuous normalization for the lambda-calculus and Gödel's T
• The consistency of arithmetic
• A note on fragments of uniform reflection in second order arithmetic
• AN INCOMPLETENESS THEOREM VIA ORDINAL ANALYSIS
• A mathematical commitment without computational strength
• Proof lengths for instances of the Paris-Harrington principle

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2277451)