# 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
Commented 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
Commented Sep 3, 2021 at 6:34
• No; the "lower" assumption of $Q$ is not correctly discharged. Commented 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. Commented Sep 3, 2021 at 6:40
• See this post: you need Double Negation. Commented 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$$