Some results on cut-elimination, provable well-orderings, induction and reflection
type: Item
instance of: scholarly article
title: Some results on cut-elimination, provable well-orderings, induction and reflection
zbMATH Open document ID: 0936.03054
DOI: 10.1016/S0168-0072(98)00020-7
author: Toshiyasu Arai
published in: Annals of Pure and Applied Logic
publication date: 2000-05-17T00:00:00Z
review text: The author begins this long paper by saying ``We gather the following miscellaneous results in proof theory from the attic''. This attic must be large and full of stuff. Apparently, in studying other people's papers, ideas, etc., the author came up with his own new, improved, etc. approaches, and kept them in the attic. Among them are the following eight topics. \S 1. A provably well-founded relation in PA can be embedded into an initial segment of \(\varepsilon_0\) by an elementary function. (This improves results of Gentzen, Takeuti, and Harrington.) \S 2. Shortest cut-free proofs in propositional calculus. Here, pruning is applicable, and so the length is bounded by an elementary function. This result in turn, is applied to bounded arithmetic, and various provabilities and non-provabilities are shown. \S 3 is about bar induction; in particular, its relation with reflection schema in \(\omega\)-logic, and with transfinite induction. \S 4 is of a quite different nature; it is about equational calculus. The possibility of direct computations (i.e. without extraneous function symbols) is discussed, and the decidability of inequalities is solved affirmatively. In \S 5, intuitionistic iterated fixed point theories for strongly positive operator forms are shown to be conservative over HA, via interpretation in elementary analysis. \S 6 bears a similar title: classical fixed point theories. But it is about computation of proof-theoretic ordinals, carrying on Kreisel's work of four decades ago. The themes of \S 7 are the equivalence of transfinite induction rule and iterated reflection schema over \(I\Sigma_n\), and that of iterated \(\Pi_2\)-reflection schema and the totality of the fast growing functions over \(I\Sigma_1\) . The final \S 8 is more in computer science, and the author estimates derivation lengths of finite rewriting systems by means of ordinal analysis, slow growing functions, etc. These eight sections are independent of one another, and ample background …
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 1308093
zbMATH Keywords: proof theory
zbMATH Keywords: provably well-founded relation
zbMATH Keywords: PA
zbMATH Keywords: cut-free proofs
zbMATH Keywords: pruning
zbMATH Keywords: bounded arithmetic
zbMATH Keywords: bar induction
zbMATH Keywords: transfinite induction
zbMATH Keywords: equational calculus
zbMATH Keywords: direct computations
zbMATH Keywords: decidability
zbMATH Keywords: intuitionistic iterated fixed point theories
zbMATH Keywords: interpretation
zbMATH Keywords: elementary analysis
zbMATH Keywords: classical fixed point theories
zbMATH Keywords: computation of proof-theoretic ordinals
zbMATH Keywords: iterated reflection schema
zbMATH Keywords: derivation lengths of finite rewriting systems
MaRDI profile type: Publication
cites work: Variations on a theme by Weiermann
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q5691043
cites work: Recursive models for constructive set theories
cites work: Induction rules, reflection principles, and provably recursive functions
cites work: Proof-theoretic analysis of termination proofs
cites work: An intuitionistic fixed point theory
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q3794177
cites work: An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
cites work: Q3138831
cites work: Term rewriting theory for the primitive recursive functions
cites work: Q4850548
cites work: Q4385532
cites work: Q3671968
cites work: Provable equality in primitive recursive arithmetic with and without induction
cites work: Elementary descent recursion and proof theory
cites work: Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
cites work: Q3956931
cites work: Q3773876
cites work: Relativized realizability in intuitionistic arithmetic of all finite types
cites work: Termination proofs by multiset path orderings imply primitive recursive derivation lengths
cites work: Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
cites work: Bounds for cut elimination in intuitionistic propositional logic
cites work: The proof-theoretic analysis of transfinitely iterated fixed point theories
cites work: About the proof-theoretic ordinals of weak fixed point theories
cites work: Fixed point theories and dependent choice
cites work: A note on sharply bounded arithmetic
cites work: Q4856172
cites work: Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
cites work: Q3999386
cites work: Elementary induction on abstract structures
cites work: Q3138827
cites work: Q3866106
cites work: Q4143279
cites work: Q5534937
cites work: Q3960691
cites work: Q4944925
cites work: Transfinite induction within Peano arithmetic
cites work: A Remark on Gentzen's paper “Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten induktionin der reinen zahlentheorie”, I
cites work: Proof theory. 2nd ed
cites work: Q3140644

Some results on cut-elimination, provable well-orderings, induction and reflection (cites work)
cites work: Separations of theories in weak bounded arithmetic

Some results on cut-elimination, provable well-orderings, induction and reflection (cites work)
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

Some results on cut-elimination, provable well-orderings, induction and reflection (cites work)
cites work: Constructivism in mathematics. An introduction. Volume II

Some results on cut-elimination, provable well-orderings, induction and reflection (cites work)
cites work: Q3138826

Some results on cut-elimination, provable well-orderings, induction and reflection (cites work)
cites work: Bounding derivation lengths with functions from the slow growing hierarchy

Some results on cut-elimination, provable well-orderings, induction and reflection (cites work)
cites work: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Q3475264
Similarity Score: 0.87414837
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Intuitionistically provable recursive well-orderings
Similarity Score: 0.8703794
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Well-Ordering Principles in Proof Theory and Reverse Mathematics
Similarity Score: 0.8698853
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: A cut-elimination proof in intuitionistic predicate logic
Similarity Score: 0.8694669
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Cut-Elimination and Proof Schemata
Similarity Score: 0.86927664
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Cut Elimination in ε‐Calculi
Similarity Score: 0.8686086
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: An Addition to “Cut Elimination in ε-Calculi”
Similarity Score: 0.86789954
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: A Note on (Meta)predicative Wellordering Proofs
Similarity Score: 0.86769146
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Proof-theoretic strengths of the well-ordering principles
Similarity Score: 0.8667259
Recommender Run: Recommender Run 3

Some results on cut-elimination, provable well-orderings, induction and reflection (Recommended article)
Recommended article: Q3801546
Similarity Score: 0.8665059
Recommender Run: Recommender Run 3