Some results on cut-elimination, provable well-orderings, induction and reflection

DOI10.1016/S0168-0072(98)00020-7zbMath0936.03054MaRDI QIDQ1295413

Toshiyasu Arai

Publication date: 17 May 2000

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

decidabilityproof theorypruningbounded arithmetictransfinite inductioninterpretationbar inductionPAcut-free proofselementary analysisclassical fixed point theoriescomputation of proof-theoretic ordinalsderivation lengths of finite rewriting systemsdirect computationsequational calculusintuitionistic iterated fixed point theoriesiterated reflection schemaprovably well-founded relation

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Grammars and rewriting systems (68Q42) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)

Related Items

On the Computational Content of Termination Proofs, Derivatives of normal functions and \(\omega \)-models, The omega-rule interpretation of transfinite provability logic, Revisiting the conservativity of fixpoints over intuitionistic arithmetic, Quick cut-elimination for strictly positive cuts, Intuitionistic fixed point theories over set theories, On Relating Theories: Proof-Theoretical Reduction, Some interesting connections between the slow growing hierarchy and the Ackermann function, Derivation lengths and order types of Knuth--Bendix orders, GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION, Proof-theoretic strengths of the well-ordering principles

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Term rewriting theory for the primitive recursive functions
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Proof theory. 2nd ed
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Constructivism in mathematics. An introduction. Volume II
• Bounds for cut elimination in intuitionistic propositional logic
• Elementary induction on abstract structures
• Provable equality in primitive recursive arithmetic with and without induction
• Bounding derivation lengths with functions from the slow growing hierarchy
• A note on sharply bounded arithmetic
• Elementary descent recursion and proof theory
• Separations of theories in weak bounded arithmetic
• Induction rules, reflection principles, and provably recursive functions
• An intuitionistic fixed point theory
• Fixed point theories and dependent choice
• Proof-theoretic analysis of termination proofs
• Transfinite induction within Peano arithmetic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
• Recursive models for constructive set theories
• About the proof-theoretic ordinals of weak fixed point theories
• Relativized realizability in intuitionistic arithmetic of all finite types
• Variations on a theme by Weiermann
• The proof-theoretic analysis of transfinitely iterated fixed point theories
• An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• A Remark on Gentzen's paper “Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten induktionin der reinen zahlentheorie”, I
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems