A question about Implicational Propositional Calculus
I think I sorted out the outline, I still need to fill in the gaps but here something to start with: (f = $ \bot $)
1 |- ( A -> (B->C)) -> ((A -> B)-> (A->C))) A2
2 |- ( A -> (B->f)) -> ((A -> B)-> (A->f))) 1 C := f
3 |- ( (A->f) -> (B->f) )-> (((A->f) -> B)-> ((A->f)->f))) 2 A := (A->f)
4 |- ((A -> B) -> A) -> A A3 Peirce
5 |- ((A->f) -> A) -> A 4 B := f
6 |- ((A->f) -> f) -> ((A->f) -> f) theorem (A -> A)
7 |- f -> A axiom
8 |- ((A -> f) -> f) -> ((A -> f) -> A) hyp syll 6,7
9 |- ((A -> f) -> f) -> A hyp syll 8,5
10 |- ((A -> f) -> (B-> f)) -> (((A ->f) -> B)-> A ) hyp syll 3,9
And 10 is $ ( \lnot A \to \lnot B) \to (( \lnot A \to B) \to A ) $
good exercise
Combining the subformula strategy, weighting of the axioms and the goal, and a (partial) level saturation search, I've found a 15 step (excluding the axioms), level 5 proof using OTTER [1]. Actually, instead of proving
CCCp0Cq0CCCp0qp. OTTER proved the more general
CCCpqCr0CCCpqrp. (we can substitute q/0, r/q in CCCpqCr0CCCpqrp to get CCCp0Cq0CCCp0qp, but we can't obtain CCCpqCr0CCCpqrp from CCCp0Cq0CCCp0qp by substitution alone).
Note that this does not imply that
CCNpNqCCNpqp could get replaced by
CCCpqNrCCCpqrp without the definition Np := Cp0.
Here's the proof:
axiom 3 CxCyx. Level of formula is 0.
axiom 4 CCxCyzCCxyCxz. 0
axiom 5 CCCxyxx. 0
axiom 6 C0x. 0
D3.3 7 CxCyCzy. 1
D4.4 8 CCCxCyzCxyCCxCyzCxz. 1
D3.4 9 CxCCyCzuCCyzCyu. 1
D3.5 11 CxCCCyzyy. 1
D3.6 13 CxC0y. 1
DD4.4.7 17 CCxCCyxzCxz. 2
D3.9 20 CxCyCCzCuvCCzuCzv. 2
D4.11 25 CCxCCyzyCxy. 2
D4.13 27 CCx0Cxy. 2
D17.9 42 CCxyCCzxCzy. 3
DD4.4.20 51 CCxCCCyCzuCCyzCyuvCxv. 3
DD4.11.27 71 CCCxy0x. 3
D51.42 224 CCCCxyCxzuCCxCyzu. 4
D42.71 300 CCxCCyz0Cxy. 4
D224.300 2474 CCCxyCz0CCCxyzx. 5
[1]- W. McCune, "OTTER and Mace2", http://www.mcs.anl.gov/research/projects/AR/otter/, 1988-2014.
The solution is motivated by Alonzo Church, Introduction to Mathematical Logic (1956), Ex 12.7 [page 86].
We need $\bot$ and $\rightarrow$ as primitives and the definition of $\lnot A$ as : $A \rightarrow \bot$.
We need also as additional axiom, Ex Falso Quodlibet [see Church, para.$122, page 84] :
$\vdash \bot \rightarrow A$.
With EFQ and Peirce's law, we can have Double Negation :
$\vdash \lnot \lnot A \rightarrow A$.
Proof
1) $\lnot \lnot A$ --- assumed
2) $\lnot A \rightarrow \bot$ --- by def of $\lnot$
3) $\lnot A$ --- assumed
4) $\bot$ --- from 2) and 3) by modus ponens
5) $\vdash \bot \rightarrow A$ --- EFQ
6) $A$ --- from 4) and 5) by mp
7) $\lnot A \rightarrow A$ --- from 3) and 6) by Deduction Theorem
8) $\vdash (\lnot A \rightarrow A) \rightarrow A$ --- from Peirce's law
9) $A$ --- from 7) and 8) by mp
10) $\vdash \lnot \lnot A \rightarrow A$ --- from 1) and 9) by DT.
Note
See Joel W. Robbin, Mathematical Logic : A First Course (1969 - Dover reprint), page 22 : axiom schema (A3) of Mendelson's system can be replaced by : $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ or equivalently by $\vdash (\lnot A \rightarrow B) \rightarrow (\lnot B \rightarrow A)$.
Or we can replace it with EFQ and Peirce's law.
Now for the proof of Mendelson's (A3) :
1) $\lnot C \rightarrow \lnot B$ --- assumed
2) $\lnot C \rightarrow B$ --- assumed
3) $\lnot C$ --- assumed
4) $\lnot B$ --- from 1) and 3) by modus ponens
5) $B$ --- from 2) and 3) by modus ponens
6) $\bot$ --- from 4) and 5) and definition of $\lnot$, by mp
7) $\lnot \lnot C$ --- from 3) and 6) by DT
8) $C$ --- from 7) and Double Negation, by mp.
Finally, apply Deduction Theorem twice :
$\vdash (\lnot C \rightarrow \lnot B) \rightarrow ((\lnot C \rightarrow B) \rightarrow C)$.
We have used the Deduction Theorem, which is provable with (A1) and (A2) only.