Prove $(\lnot p \to p) \to p$ in 19 steps

Question

While revisiting "Mathematical Logic", I noticed a quiz that I had never worked out. It requires to prove

$$\{\} \vdash (\lnot p \to p) \to p$$

in 19 steps.

To be clear, each "step" should be in one of the following forms:

1. $p \to (q \to p)$ (L1)
2. $(p \to (q \to r)) \to ((p \to q) \to (p \to r))$ (L2)
3. $(p \to q) \to (\lnot q \to \lnot p)$ (L3)
4. $q$, provided that both $p$ and $p \to q$ have appeared in previous steps (Modus Ponens, MP)

(According to the book, using MP twice in an expression counts as 2 steps, and similar counting method holds for other expressions)

I still can't work this out, any one point out a way?

---

For example, here's a valid proof of $\{p \to q, q \to r\} \vdash p \to r$ in 7 steps:

1. $(q \to r) \to (p \to (q \to r))$ (L1)
2. $q \to r$ (Assumption)
3. $p \to (q \to r)$ (1, 2, MP)
4. $(p \to (q \to r)) \to ((p \to q) \to (p \to r))$ (L2)
5. $(p \to q) \to (p \to r)$ (3, 4, MP)
6. $p \to q$ (Assumption)
7. $p \to r$ (5, 6, MP)

Answer 1

Sketch of the proof.

I'll use the following axiom in place of (L3) :

(L3') $\vdash (¬p→¬q) → (q→p)$.

The axiom system (L1), (L2) and (L3') is complete for classical propositional logic.

With it we can prove (L3) as well as Double Negation laws and

(A) $\vdash A \to A$.

---

1) $\vdash \lnot A \to (\lnot B \to \lnot A)$ --- (L1)

2) $\vdash (¬B→¬A) → (A→B)$ --- (L3')

(B) $\vdash \lnot A \to (A→B)$ --- from 1) and 2) by Trans (you have proved it)

1) $\vdash (\lnot A \to (A \to \lnot B)) \to ((\lnot A \to A) \to (\lnot A \to \lnot B))$ --- (L2)

2) $\vdash \lnot A \to (A \to \lnot B)$ --- from (B) with $\lnot B$ in place of $B$

3) $\vdash (\lnot A \to A) \to (\lnot A \to \lnot B)$ --- from 1) and 2) by MP

(C) $\vdash (\lnot A \to A) \to (B \to A)$ --- from 3) and (L3') by Trans

---

1) $\vdash (\lnot p \to p) \to ((\lnot p \to p) \to p)$ --- from (C) with $(\lnot p \to p)$ in place of $B$

2) suitable version of (L2)

3) $\vdash ((\lnot p \to p) \to (\lnot p \to p)) \to ((\lnot p \to p) \to p)$ --- from 1) and 2) by MP

4) $\vdash (\lnot p \to p) \to (\lnot p \to p)$ --- from (A)

5) $\vdash (\lnot p \to p) \to p$ --- from 3) and 4) by MP

Answer 2

First, Mauro is right to question your third axiom, for your L1,L2,L3, okus Modus Ponens is not complete ... and in fact with those you cannot prove $(\neg p \to p) \to p$

To see why, take the following non-standard semantics for the variables and their operators:

All statements still take a value of $T$ or $F$, and the $\to$ is defined as normal, but $\neg p$ will always return $F$

Then L1 and L2 are of course still tautologies, since they do not involve any $\neg$, but L3 is a tautology as well. And, using Modus Ponens, you can only infer further tautologies from tautologies.

However, $(\neg p \to p) \to p$ is no longer a tautology. With $p=F$, you get $(\neg F \to F) \to F = (F \to F) \to F = T \to F = F$

Therefore, $(\neg p \to p) \to p$ cannot be derived using your axioms and inference rule as stated.

(note that a similar argument can be used to show that $\neg \neg p \to p$ can also not be proven: this time, define $\neg$ such that it always evaluates to $T$. Then L1,L2,L3 are still tautologies, and MP can only derie tautologies from tautologies, but $\neg \neg p \to p$ is not a tautology, since with $P=F$, you get $\neg \neg p \to p = \neg \neg F \to F = \neg T \to F = T \to F = F$)

Following Mauro's suggestion to replace your third axiom with $(\neg p \to \neg q) \to (q \to p)$ (which is the 'standard' third axiom of the Lukasciewicz system .. which is complete), and working out his proof schema, you get:

\begin{array}{lll} 1&\neg p \to (\neg \neg (\neg p \to p) \to \neg p) & L1\\ 2&(\neg \neg (\neg p \to p) \to \neg p) \to (p \to \neg (\neg p \to p))&L3'\\ 3&((\neg \neg (\neg p \to p) \to \neg p) \to (p \to \neg (\neg p \to p)))\to (\neg p \to ((\neg \neg (\neg p \to p) \to \neg p) \to (p \to \neg (\neg p \to p))))&L1\\ 4&\neg p \to ((\neg \neg (\neg p \to p) \to \neg p) \to (p \to \neg (\neg p \to p)))&MP \ 3,2\\ 5&(\neg p \to ((\neg \neg (\neg p \to p) \to \neg p) \to (p \to \neg (\neg p \to p))))\to( (\neg p \to (\neg \neg (\neg p \to p) \to \neg p))\to (\neg p \to (p \to \neg (\neg p \to p))))&L2\\ 6& (\neg p \to (\neg \neg (\neg p \to p) \to \neg p))\to (\neg p \to (p \to \neg (\neg p \to p)))&MP \ 5,4\\ 7&\neg p \to (p \to \neg (\neg p \to p))&MP \ 6,1\\ 8&(\neg p \to (p \to \neg (\neg p \to p)))\to ((\neg p \to p) \to (\neg p \to \neg (\neg p \to p)))&L2\\ 9&(\neg p \to p) \to (\neg p \to \neg (\neg p \to p))&MP \ 8,7\\ 10&(\neg p \to \neg (\neg p \to p)) \to ((\neg p \to p) \to p)& L3\\ 11&((\neg p \to \neg (\neg p \to p)) \to ((\neg p \to p) \to p)) \to ((\neg p \to p) \to ((\neg p \to \neg (\neg p \to p)) \to ((\neg p \to p) \to p)))&L1\\ 12&(\neg p \to p) \to ((\neg p \to \neg (\neg p \to p)) \to ((\neg p \to p) \to p))&MP \ 11, 10\\ 13&((\neg p \to p) \to ((\neg p \to \neg (\neg p \to p)) \to ((\neg p \to p) \to p)))\to (((\neg p \to p) \to (\neg p \to \neg (\neg p \to p))) \to ((\neg p \to p) \to ((\neg p \to p) \to p)))&L2\\ 14&((\neg p \to p) \to (\neg p \to \neg (\neg p \to p))) \to ((\neg p \to p) \to ((\neg p \to p) \to p))&MP \ 13, 12\\ 15&(\neg p \to p) \to ((\neg p \to p) \to p)&MP \ 14, 9\\ 16&(\neg p \to p) \to ((p \to (\neg p \to p)) \to (\neg p \to p))&L1\\ 17&((\neg p \to p) \to ((p \to (\neg p \to p)) \to (\neg p \to p)))\to (((\neg p \to p) \to (p \to (\neg p \to p))) \to ((\neg p \to p) \to (\neg p \to p)))&L2\\ 18&((\neg p \to p) \to (p \to (\neg p \to p))) \to ((\neg p \to p) \to (\neg p \to p))&MP \ 17, 16\\ 19& (\neg p \to p) \to (p \to (\neg p \to p))& L1\\ 20&(\neg p \to p) \to (\neg p \to p)&MP \ 18, 19\\ 21&((\neg p \to p) \to ((\neg p \to p) \to p)) \to (((\neg p \to p) \to (\neg p \to p)) \to ((\neg p \to p) \to p))&L2\\ 22&((\neg p \to p) \to (\neg p \to p)) \to ((\neg p \to p) \to p)&MP \ 21,15\\ 23&(\neg p \to p) \to p&MP \ 22,20\\ \end{array}

So .... that's 23 lines, rather than 19 ... pretty good ... but not quite short enough... or maybe we are still using the wrong axiom for axiom 3?