Gentzen's consistency proof without heightlines
A proof of the consistency of a sequent calculus for intuitionistic arithmetic is proposed. The proof is based on the Gentzen-style assignment of ordinals to the derivations but does not use the so-called heightline argument, which means that the ordinal assigned to a sequent depends on the height of the sequent. Instead, the techniques proposed by Howard for Gödel's system \(T\) [\textit{W. A. Howard}, in: Intuitionism Proof Theory, Proc. Summer Conf. Buffalo N.Y. 1968, 443--458 (1970; Zbl 0206.28202)] is used. Namely an expression is assigned to every sequent and a vector of expressions is assigned to a derivation. Further, the first expression in the vector is interpreted as an ordinal. The author describes a procedure of transforming derivations of the empty sequent which reduces that ordinal. This provides the consistency of the system.
- A Direct Gentzen-Style Consistency Proof for Heyting Arithmetic
- Consistency of Heyting arithmetic in natural deduction
- On Gentzen's first consistency proof for arithmetic
- Extending the First Gentzen's Consistency Proof to the Intuitionistic Case
- Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
- A Direct Gentzen-Style Consistency Proof for Heyting Arithmetic
- A proof of Gentzen's \textit{Hauptsatz} without multicut
- Consistency of Heyting arithmetic in natural deduction
- Constructivism in mathematics. An introduction. Volume I
- Derivation lengths classification of Gödel's T extending Howard's assignment
- Handbook of proof theory
- scientific article; zbMATH DE number 3572133 (Why is no real title available?)
- scientific article; zbMATH DE number 949290 (Why is no real title available?)
- scientific article; zbMATH DE number 3328152 (Why is no real title available?)
- scientific article; zbMATH DE number 3333259 (Why is no real title available?)
- On permuting cut with contraction
- Proof theory. 2nd ed
- The machinery of consistency proofs
- Two measures for proving Gentzen's Hauptsatz without mix
- A negationless interpretation of intuitionistic theories. I
- A note on Gentzen's ordinal assignment
- A negationless interpretation of intuitionistic theories
- From Stenius' consistency proof to Schütte's cut elimination for -arithmetic
- Consistency of Heyting arithmetic in natural deduction
- Extending the First Gentzen's Consistency Proof to the Intuitionistic Case
- Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
- From \textit{Hauptsatz} to \textit{Hilfssatz}
- Normalization proof for Peano arithmetic
This page was built for publication: Gentzen's consistency proof without heightlines
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2377348)
