Is this a correct derivation of Peirce's law?

Question

I've used the rules of Chapter 2 of van Dalen's Logic and Structure, which allows only $\{ \wedge I, \wedge E, \to I, \to E, \bot E, RAA.\}$ $$ \newcommand{\bfrac}[2]{\displaystyle\genfrac{}{}{0pt}{}{#1}{#2}} \cfrac{ \cfrac{ \cfrac{{\bfrac{}{[( P\to Q)\to P]^3}} \quad\quad\quad \cfrac{[Q]^1}{P\to Q}}{P} \quad\quad\quad \bfrac{}{ {[\neg P]^2} }} {{\cfrac{\cfrac{\bot}{ \neg Q}1 \quad\quad\quad\quad\quad \bfrac{}{[ Q] ^1}} {\cfrac{\bot}{P}}}}} {(P\to Q)\to P)\to P}3 $$

Answer 1

I think below is the most natural way for me to derive Peirce's law in classic logic per Dalen's natural deduction rules and style. Another style is Fitch which I found an old post here deriving the same Peirce's law in Fitch style, and the steps are essentially same as mine below.

Please note that in your derivation you need to assume Q (your assumption #1) which is not needed at all in the whole proof. Actually if you transform your own proof to Fitch, then you'll see you cannot arrive at your first $\bot$ above at all within a same subproof. IMHO, Dalen's style is error prone and not suitable for new students just beginning their logic study. You seem to be able to do the job with discharging all assumptions, but you also intuitively feel you're not confident at all.

$$ \cfrac{[(P \to Q) \to P]^1 \quad \quad \cfrac{\cfrac{\cfrac{[\neg P]^2 \quad \quad [P]^3}{\bot} \to E}{Q} \bot}{(P \to Q)} \to I_3}{\cfrac{\cfrac{\cfrac{P}{\bot} \to E}{P} \quad RAA_2} {((P \to Q) \to P) \to P} \to I_1} \to E $$

Answer 2

Using a form of natural deduction (screen print from my proof checker):