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

DOI10.1016/S0168-0072(98)00020-7zbMATH Open0936.03054MaRDI QIDQ1295413FDOQ1295413

Authors: Toshiyasu Arai 

Publication date: 17 May 2000

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

Recommendations

• Publication:3475264
• Intuitionistically provable recursive well-orderings
• Well-Ordering Principles in Proof Theory and Reverse Mathematics
• A cut-elimination proof in intuitionistic predicate logic
• Cut-elimination and proof schemata
• Cut Elimination in ε‐Calculi
• An Addition to “Cut Elimination in ε-Calculi”
• A Note on (Meta)predicative Wellordering Proofs
• Proof-theoretic strengths of the well-ordering principles
• scientific article; zbMATH DE number 4068863

zbMATH Keywords

pruninginterpretationproof theorybounded arithmeticdecidabilitybar inductiontransfinite inductioncut-free proofsPAelementary 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

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

Cites Work

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

Cited In (12)

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

This page was built for publication: Some results on cut-elimination, provable well-orderings, induction and reflection

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