Equivalence between Peirce's law and Excluded Middle in Intuitionistic logic

Question

I'm searching for a intuitionistically valid proof of the formula :

$[((P→Q)→P)→P] ↔ (P \lor \lnot P)$

using the "standard" Hilbert-style axiom system from Kleene [1952], for intuitionistic propositional calculus (with modus ponens).

Following Wiki's proof, I've rewritten the first part :

$\vdash (P \lor \lnot P) → [((P→Q)→P)→P]$

as follows :

1) $P$ --- assumed

2) $((P→Q)→P)→P$ --- from axiom $A → (B → A)$, with $P$ in place of $A$ and $((P→Q)→P)$ as $B$, and 1), by modus ponens

3) $P → [((P→Q)→P)→P]$ --- from 1) and 2) by Deduction Theorem, "discharging" assumption 1)

4) $\lnot P$ --- assumed

5) $(P→Q)$ --- from axiom $\lnot A → (A → B)$ (ex falso quodlibet) and 4), by modus ponens

6) $(P→Q)→P$ --- assumed

7) $P$ --- from 5) and 6), by mp

8) $((P→Q)→P)→P$ --- from 6) and 7), by Deduction Theorem, "discharging" assumption 6)

9) $\lnot P → [((P→Q)→P)→P]$ --- from 4) and 8) by Deduction Theorem, "discharging" assumption 4)

Now that we have derived : $P → [((P→Q)→P)→P]$ (3) and $\lnot P → [((P→Q)→P)→P]$ (9), we use the axiom $(A → C) → ((B → C) → (A ∨ B → C))$ with $P$ in place of $A$, $\lnot P$ in place of $B$ and $((P→Q)→P)→P$ as $C$ to derive, by modus ponens twice :

10) $(P \lor \lnot P) → [((P→Q)→P)→P]$.

---

---

I'm not able to manege Wiki's proof of the other part in order to prove the conditional :

$\vdash [((P→Q)→P)→P] → (P \lor \lnot P)$.

In Wiki's proof, as well as in the answer to this post we can find the proof of :

if $\vdash ((P→Q)→P)→P$, then $\vdash P \lor \lnot P$.

The proof use a "substitution instance" of Peirce's law : $(((P \lor \lnot P) \rightarrow \bot) \rightarrow (P \lor \lnot P)) \rightarrow (P \lor \lnot P)$, and this is allowed only if the formula is an axiom or a theorem, which is not in intuitionistic logic.

---

For a similar situation, see Jan von Plato, Elements of Logical Reasoning (2013), page 82 :

Given $A \lor \lnot A$, if $\lnot \lnot A$ is assumed, $A$ follows and therefore the implication $\lnot \lnot A \supset A$ follows from $A \lor \lnot A$. An easy proof search in intuitionistic sequent calculus gives a formal derivation for :

$A \lor \lnot A \supset (\lnot \lnot A \supset A)$.

A similar proof search for the converse fails, for there is no derivation of :

$(\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.

[...]

The overall situation is that if $\vdash \lnot \lnot A \supset A$, then $\vdash A \lor \lnot A$, but not $\vdash (\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.

---

Thus, the Question is : is it possible that

if $\vdash ((P→Q)→P)→P$, then $\vdash P \lor \lnot P$,

but $\nvdash [((P→Q)→P)→P] → (P \lor \lnot P)$

Answer 1

The implication $$ [((P\rightarrow Q)\rightarrow P)\rightarrow P ] \rightarrow P\lor\neg P \quad\quad\quad\quad (1) $$ is in fact not a theorem of intuitionistic propositional logic. You can check this semantically, with a Kripke frame with two worlds $w_1\le w_2$, with $P, Q$ both satisfied in $w_2$ and none of them satisfied in $w_1$. See here for background. Or you could try to prove (1) in a sequent calculus and discover that you get stuck.

What is true is that if you make Peirce's law an additional axiom, then $P\lor\neg P$ becomes a theorem. In symbols: $$ \{((A\rightarrow B)\rightarrow A )\rightarrow A\} \vdash P\lor\neg P $$ Here the curly brackets are supposed to refer to the collection of all substitution instances. This is discussed in the answer you linked. (So Peirce's law and LEM are equivalent in the sense that adding either of them will give you classical logic.)

By the deduction theorem, you then also obtain an implication similar to (1) as a theorem, but if you check what (substitution) instance of Peirce's was actually used, you'll find that $A=P\lor\neg P$, $B=\bot$. So $$ \vdash [((P\lor\neg P\rightarrow \bot)\rightarrow P\lor\neg P )\rightarrow P\lor\neg P] \rightarrow P\lor\neg P , $$ which of course is not the same as (1).

As for your last question, taken in an abstract sense, it is definitely possible to have "$\vdash A$ implies $\vdash B$" satisfied, but $A\rightarrow B$ is not a formal theorem: the hypothesis holds whenever $\not\vdash A$, and there is of course no reason why this would make $A\rightarrow B$ a theorem.

Answer 2

The equivalence between Peirce's formula and the excluded middle is sometimes claimed but because $$(((A \to B) \to A) \to A) \to (\lnot A \lor A)$$ is not an intuitionistic theorem, this equivalence fails in intuitionistic logic. But this instance of Peirce's formula: $$((A \to \bot) \to A) \to A$$ i.e. $$(\lnot A \to A) \to A$$ is intuitionistically equivalent to the classical double negation elimination; i.e. $$\lnot \lnot A \to A$$