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 $$
$\begingroup$
$\endgroup$
7
-
$\begingroup$ Please review your use of MathJax $\endgroup$– user876009Sep 3, 2021 at 6:31
-
$\begingroup$ Are you sue this is how it is supposed to be written? It's a tad bit hard to read. $\endgroup$– user956717Sep 3, 2021 at 6:34
-
2$\begingroup$ No; the "lower" assumption of $Q$ is not correctly discharged. $\endgroup$– Mauro ALLEGRANZASep 3, 2021 at 6:39
-
1$\begingroup$ 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. $\endgroup$– blahblahSep 3, 2021 at 6:40
-
1$\begingroup$ See this post: you need Double Negation. $\endgroup$– Mauro ALLEGRANZASep 3, 2021 at 6:40
|
Show 2 more comments
2 Answers
$\begingroup$
$\endgroup$
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 $$
answered Sep 3, 2021 at 19:27
$\begingroup$
$\endgroup$
Using a form of natural deduction (screen print from my proof checker):
answered Sep 4, 2021 at 4:11