Contraction-elimination for implicational logics (Q676308)

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.