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)$