Contraction-elimination for implicational logics

DOI10.1016/S0168-0072(97)81394-2MaRDI QIDQ676308zbMATH OpenOpenAlexFDO

Authors Ryo Kashima

Publication date 6 October 1997

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(97)81394-2

zbMATH Keywords

BCK-logicclassical logiccontraction rulesGentzen-type formulationsimplicational fragmentsintuitionistic logic

Mathematics Subject Classification ID

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

Review text

The author considers the implicational fragments of the classical and intuitionistic logics and obtains a quite interesting syntactical result regarding the role of contraction rules in the corresponding Gentzen-type formulations of these fragments. A propositional letter \(p\) is said to be PNN (respectively PPN) in a sequent \(\Gamma\lvdash A\) if \(p\) occurs at least once (resp. twice) positively and at least twice (resp. once) negatively in \(\Gamma\lvdash A\). The following ``contraction-elimination theorem is proved: if a sequent \(\Gamma\lvdash A\) is provable in the implicational fragment of \({\mathbf L}{\mathbf K}\) (resp. \({\mathbf L}{\mathbf J}\)) and if no propositional letter is PNN (resp. PPN) in \(\Gamma\lvdash A\), then \(\Gamma\lvdash A\) is provable without the right (resp. left) contraction rule. An immediate consequence of this theorem is the following one: if an implicational formula \(A\) is a theorem of classical logic (resp. of intuitionistic logic) and is not a theorem of intuitionistic logic (resp. BCK-logic), then there is a propositional letter which is PNN (resp. PPN) in \(A\). The methods used in proofs are purely syntactical.

Recommendations

• Contraction-free sequent calculi for intuitionistic logic
• The proof-theoretical analysis of contraction-less relevant logics
• scientific article; zbMATH DE number 823590
• Contraction in propositional logic
• Contraction in propositional logic
• Note on deduction theorems in contraction-free logics
• Deduction theorems for weak implicational logics
• The contraction rule and decision problems for logics without structural rules
• On a contraction-less intuitionistic propositional logic with conjunction and fusion
• Algorithmic proof methods and cut elimination for implicational logics. I: Modal implication

Cites work

• Logics without the contraction rule
• Proof theory. 2nd ed
• Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt

Cited in

(13)

• Investigations into a left-structural right-substructural sequent calculus
• Contraction in propositional logic
• Contraction-free proofs and finitary games for linear logic
• Logics without the contraction rule
• Contraction-free sequent calculi for intuitionistic logic
• scientific article; zbMATH DE number 1222495 (Why is no real title available?)
• scientific article; zbMATH DE number 2024615 (Why is no real title available?)
• On permuting cut with contraction
• Belief Contraction, Anti-formulae and Resource Overdraft: Part I Deletion in Resource Bounded Logics
• scientific article; zbMATH DE number 823590 (Why is no real title available?)
• Contraction contracted
• scientific article; zbMATH DE number 2236612 (Why is no real title available?)
• Rule-elimination theorems

This page was built for publication: Contraction-elimination for implicational logics

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