Why Peirce's law implies law of excluded middle?

Why if in a formal system the Peirce's law $((P\rightarrow Q)\rightarrow P) \rightarrow P$ is true, the law of excluded middle $P \lor \neg P$ is true too?

Intuition:

Peirce's law is of the form $$\big((A \to B) \to A\big) \quad \to \quad A,$$ that is, given $(A \to B) \to A$ we could deduce $A$. Therefore, we will try to construct $$((P \lor \neg P) \to \bot) \to (P \lor \neg P).$$ The trick is that for any $A \to B$ we can strengthen $A$ or relax $B$, for example:

\begin{align} P\lor \neg P &\to \bot &\text{implies}&& P &\to \bot,\\ P &\to P &\text{implies}&& P &\to P \lor \neg P. \end{align} So we could start with a tautology (I assume that negation is just a shorthand for $\to \bot$) \begin{align} \neg P &\to \neg P \\ (P \to \bot) &\to \neg P \end{align} strengthen left side $$(P \lor \neg P \to \bot) \to \neg P$$ and relax right side $$(P \lor \neg P \to \bot) \to P \lor \neg P.$$

Now we apply Peirce's law, and we are done ;-)

Things used:

• negation $\neg P$ is a shorthand for $P \to \bot$,
• identity: $\dfrac{\quad}{\Gamma, A \vdash A}[\alpha]$
• application: $\dfrac{\Gamma \vdash A, A \to B}{\Gamma \vdash B}[\beta]$
• finite composition $\dfrac{\Gamma \vdash A_1 \to A_2, A_2 \to A_3, \ldots, A_{n-1} \to A_n}{ \Gamma \vdash A_1 \to A_n}[\gamma]$,
• disjunction introduction: $\dfrac{}{\Gamma, A \vdash A \lor B}[\delta]$,
• implication: $\dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}[\iota]$,
• Peirce's law $\dfrac{}{\Gamma \vdash ((A\to B) \to A) \to A}[\pi]$.

The proof:

The premise

$$ \dfrac{ \dfrac{ \dfrac{ \frac{}{P \to P \lor \neg P}{[\delta,\iota]}, \quad \frac{}{P \lor \neg P \to \bot \vdash P \lor \neg P \to \bot}[\alpha] }{P\lor\neg P \to \bot \vdash P \to \bot}[\gamma] }{(P\lor\neg P\to \bot) \to \neg P}[\iota], \quad \dfrac{\quad}{\neg P \to P \lor \neg P}[\delta, \iota] }{(P \lor \neg P \to \bot) \to P \lor \neg P}[\gamma] $$

and final derivation

$$ \dfrac{ \dfrac{\text{from above} }{(P \lor \neg P \to \bot) \to P \lor \neg P}, \ \dfrac{}{((P \lor \neg P \to \bot) \to P \lor \neg P) \to P \lor \neg P}[\pi] }{P \lor \neg P}[\beta] $$

There are various shortcuts, and implicit assumptions, most notably negation $\neg P$ is a shorthand for $P \to \bot$, be careful! Nevertheless, I hope it still helps $\ddot\smile$

This is probably what you're looking for: Peirce's Law Equivalent to Law of Excluded Middle. Note, however, that this proof depends on a few assumptions which are not embodied in every logic. For instance, in relevance logic, the move from $\neg p$ to $p \rightarrow q$ is invalid, since $p$ may not be relevant to $q$.