Proof of Peirce's Law in Propositional Calculus

Question

Is it possible to derive Peirce's Law:

⊢∗ [(α → β) → α] → α

in a calculus that has modus ponens, the Deduction Theorem, Cut rule, Inconsistency effect and Principle of Indirect Proof?

Thanks a lot in advance!

Answer 1

We refer to: Moshe Machover, Set Theory, Logic and Their Limitations Cambridge UP (1996), page 116-on for the definitions and some results about propositional calculus.

Proof

1) $(ϕ → ψ) → ϕ$ --- premise

2) $\lnot \phi$ --- premise

3) $\vdash^* \lnot \phi \to (\phi \to \psi)$ --- Problem 8.8 [page 125]

4) $\phi \to \psi$ --- from 2) and 3) by mp

5) $\phi$ --- from 1) and 4) by mp.

Up to now we have: $(ϕ → ψ) → ϕ, \lnot \phi \vdash^* \phi$.

Obviously: $(ϕ → ψ) → ϕ, \lnot \phi \vdash^* \lnot \phi$.

Thus, we can use Indirect proof to get:

6) $(ϕ → ψ) → ϕ, \vdash^* \phi$.

7) $\vdash^* ((ϕ → ψ ) → ϕ) → ϕ$ --- from 6) by Deduction Theorem.