Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction

DOI10.1515/9781501502620-016MaRDI QIDQ5221860zbMATH OpenOpenAlexFDO

Authors Sara Negri, Jan von Plato

Publication date 3 April 2020

Published in Concepts of Proof in Mathematics, Philosophy, and Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1515/9781501502620-016

zbMATH Keywords

contractioncut eliminationaltitude line

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) Cut-elimination and normal-form theorems (03F05) History of mathematical logic and foundations (03-03) Structure of proofs (03F07)

Recommendations

• On permuting cut with contraction
• Gentzen's consistency proof without heightlines
• A cut-elimination proof in intuitionistic predicate logic
• scientific article; zbMATH DE number 2047280
• \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs

Cited in

(13)

• From cut-free calculi to automated deduction: the case of bounded contraction
• scientific article; zbMATH DE number 1678397 (Why is no real title available?)
• Explaining the Gentzen-Takeuti reduction steps: A second-order system
• The Jacobson radical for an inconsistency predicate
• THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
• On permuting cut with contraction
• Reading conclusions conjunctively
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• On Gentzen's structural completeness proof
• Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut
• A sequent calculus with implicit term representation
• Gentzen's consistency proof without heightlines
• A proof of Gentzen's \textit{Hauptsatz} without multicut

This page was built for publication: Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction

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