Contraction-elimination for implicational logics (Q676308)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Contraction-elimination for implicational logics |
scientific article |
Statements
Contraction-elimination for implicational logics (English)
0 references
6 October 1997
0 references
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.
0 references
implicational fragments
0 references
contraction rules
0 references
Gentzen-type formulations
0 references
classical logic
0 references
intuitionistic logic
0 references
BCK-logic
0 references