Gentzen's consistency proof without heightlines

DOI10.1007/S00153-013-0324-0MaRDI QIDQ2377348zbMATH OpenOpenAlexFDO

Authors Annika Siders

Publication date 28 June 2013

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00153-013-0324-0

zbMATH Keywords

consistencysequent calculusintuitionistic arithmeticordinal assignment

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Intuitionistic mathematics (03F55)

Recommendations

• 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

Cites work

• 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?)
• 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
• On permuting cut with contraction
• Proof theory. 2nd ed

Cited in

(11)

• A negationless interpretation of intuitionistic theories
• Consistency of Heyting arithmetic in natural deduction
• Two measures for proving Gentzen's Hauptsatz without mix
• A note on Gentzen's ordinal assignment
• 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
• The machinery of consistency proofs
• Normalization proof for Peano arithmetic
• A negationless interpretation of intuitionistic theories. I
• From \textit{Hauptsatz} to \textit{Hilfssatz}
• From Stenius' consistency proof to Schütte's cut elimination for \(\omega\)-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)