Contraction-elimination for implicational logics Original Research Article

We establish the “contraction-elimination theorem” which means that if a sequent Γ ⇒ A is provable in the implicational fragment of the Gentzenʹs sequent calculus LK (resp. of LJ) and if it satisfies a certain condition on the number of the occurrences of propositional variables, then it is provable without the right (resp. left) contraction rule. By this theorem, we get the following. 1. (1) If an implicational formula A is a theorem of classical logic and is not a theorem of intuitionistic logic, then there is a propositional variable which occurs at least once positively and at least twice negatively in A (e.g., A = ((a → b) → a) → a). 2. (2) If an implicational formula A is a theorem of intuitionistic logic and is not a theorem of BCK-logic, then there is a propositional variable which occurs at least twice positively and at least once negatively in A (e.g., A = (a → a → b) → a → b). We prove the contraction-elimination theorem by a fully syntactical method, which has some analogy with Gentzenʹs cut-elimination.