On permuting cut with contraction

DOI10.1017/S0960129599003011MaRDI QIDQ4487267zbMATH OpenFDO

Authors Mirjana Borisavljević, Kosta Došen, Zoran Petrić

Publication date 24 July 2000

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/9911065

zbMATH Keywords

cut eliminationpropositional intuitionistic logicsequential formalizationstructural rule of contraction

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05)

Abstract: The paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction steps. The presentation of this procedure is preceded by an analysis of Gentzen's mix-elimination procedure, made in the perspective of permuting cut with contraction. It is also shown that in the absence of implication, pushing cut above contraction doesn't pose problems for directly eliminating cut.

Recommendations

• scientific article; zbMATH DE number 2047280
• A cut-elimination proof in intuitionistic predicate logic
• Contraction-elimination for implicational logics
• Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
• Contraction contracted

Cited in

(14)

• A cut-elimination proof in intuitionistic predicate logic
• Gentzen's consistency proof without heightlines
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• Valentini's cut-elimination for provability logic resolved
• A note on the cut-elimination proof in ``Truth without contra(di)ction
• A contraction algorithm for finding small cycle cutsets
• Contraction-free sequent calculi for intuitionistic logic
• scientific article; zbMATH DE number 1086658 (Why is no real title available?)
• scientific article; zbMATH DE number 2047280 (Why is no real title available?)
• Contraction contracted
• Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
• A proof of Gentzen's \textit{Hauptsatz} without multicut
• The elimination of maximum cuts in linear logic and BCK logic
• A connection between cut elimination and normalization

This page was built for publication: On permuting cut with contraction

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