Some results on cut-elimination, provable well-orderings, induction and reflection
From MaRDI portal
Publication:1295413
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
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)
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
Cites work
- scientific article; zbMATH DE number 432699 (Why is no real title available?)
- scientific article; zbMATH DE number 432700 (Why is no real title available?)
- scientific article; zbMATH DE number 432704 (Why is no real title available?)
- scientific article; zbMATH DE number 440487 (Why is no real title available?)
- scientific article; zbMATH DE number 3825796 (Why is no real title available?)
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- scientific article; zbMATH DE number 4059391 (Why is no real title available?)
- scientific article; zbMATH DE number 3668596 (Why is no real title available?)
- scientific article; zbMATH DE number 3777480 (Why is no real title available?)
- scientific article; zbMATH DE number 3782997 (Why is no real title available?)
- scientific article; zbMATH DE number 48365 (Why is no real title available?)
- scientific article; zbMATH DE number 3572133 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 806747 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 1420857 (Why is no real title available?)
- scientific article; zbMATH DE number 3248030 (Why is no real title available?)
- scientific article; zbMATH DE number 963569 (Why is no real title available?)
- A Remark on Gentzen's paper “Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten induktionin der reinen zahlentheorie”, I
- A note on sharply bounded arithmetic
- About the proof-theoretic ordinals of weak fixed point theories
- An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
- An intuitionistic fixed point theory
- Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
- Bounding derivation lengths with functions from the slow growing hierarchy
- Bounds for cut elimination in intuitionistic propositional logic
- Constructivism in mathematics. An introduction. Volume II
- Elementary descent recursion and proof theory
- Elementary induction on abstract structures
- Fixed point theories and dependent choice
- Induction rules, reflection principles, and provably recursive functions
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Proof theory. 2nd ed
- Proof-theoretic analysis of termination proofs
- Provable equality in primitive recursive arithmetic with and without induction
- Recursive models for constructive set theories
- Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
- Relativized realizability in intuitionistic arithmetic of all finite types
- Separations of theories in weak bounded arithmetic
- Term rewriting theory for the primitive recursive functions
- Termination proofs by multiset path orderings imply primitive recursive derivation lengths
- Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The proof-theoretic analysis of transfinitely iterated fixed point theories
- Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
- Transfinite induction within Peano arithmetic
- Variations on a theme by Weiermann
Cited in
(12)- Quick cut-elimination for strictly positive cuts
- Derivation lengths and order types of Knuth--Bendix orders
- Intuitionistic fixed point theories over set theories
- Derivatives of normal functions and \(\omega \)-models
- On Relating Theories: Proof-Theoretical Reduction
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
- On the Computational Content of Termination Proofs
- Revisiting the conservativity of fixpoints over intuitionistic arithmetic
- GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION
- Some interesting connections between the slow growing hierarchy and the Ackermann function
- Proof-theoretic strengths of the well-ordering principles
- The omega-rule interpretation of transfinite provability logic
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)
