Prove $(\lnot p \to p) \to p$ in 19 steps 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:


*

*$p \to (q \to p)$ (L1)

*$(p \to (q \to r)) \to ((p \to q) \to (p \to r))$ (L2)

*$(p \to q) \to (\lnot q \to \lnot p)$ (L3)

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

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

 A: 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

A: 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?
