# Is this a correct derivation of Peirce's law?

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

– user876009
Sep 3, 2021 at 6:31
• Are you sue this is how it is supposed to be written? It's a tad bit hard to read.
– user956717
Sep 3, 2021 at 6:34
• No; the "lower" assumption of $Q$ is not correctly discharged. Sep 3, 2021 at 6:39
• I've just edited. mathjax doesn't support proof tree, so i can't choose another way to proof except the method to use cfrac. Sep 3, 2021 at 6:40
• See this post: you need Double Negation. Sep 3, 2021 at 6:40

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