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

Solution 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.

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