Classical logic, intuitionistic logic, and the Peirce rule (Q1203786)

In Gentzen's sequent formalization of first-order logic, the essential difference between the classical system LK and the intuitionistic system LJ is that sequents \(A_ 1,\dots,A_ m\to B_ 1,\dots,B_ n\) are restricted to \(n\leq 1\) for the intuitionistic system LJ. Adjoining the Peirce rule \[ {A\Longrightarrow B, \Gamma\longrightarrow A\over\Gamma\longrightarrow A} \] to the system LJ makes it as strong as LK. Therefore it is possible to translate all LK proofs into the system \(\text{LJ}+\text{Peirce}\) rule. A simple algorithm for this purpose, translating an LK proof into the system \(\text{LJ}+\text{Peirce}\) rule, is presented in the paper. A consequence of this result is a primitive recursive cut-elimination operator for \(\text{LJ}+\text{Peirce}\) rule, which exploits the cut- elimination theorem for LK.