I tried to find a small natural deduction proof for Meredith's single axiom
| Infix notation | Polish notation |
|---|---|
| ((((ψ→φ)→(¬χ→¬ξ))→χ)→τ)→((τ→ψ)→(ξ→ψ)) | CCCCCpqCNrNsrtCCtpCsp |
but I failed. My proof (shown below) has a whooping 72 steps. Am I missing something? Can it be reduced further, or are natural deduction proofs just that big over only basic rules? For example, the semantic tableau proof (linked above) is much smaller.
So, essentially, I am looking for three things:
- A smaller proof for Meredith's single axiom.
- Methods to find optimal proofs in natural deduction systems.
- Ways to show that such a given proof is optimal.
Inference Rules
I'm looking for the smallest possible natural deduction proof, based only on the rules of {¬,→,∨,∧,↔}-{elimination,introduction} and ⊥-introduction, i.e. no derived rules:
My Attempt
The proof can be imported into https://mrieppel.github.io/fitchjs/ for automated validation and a prettier view.
Problem: |- (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A)))
1 |_ ((((A > B) > (~C > ~D)) > C) > E) Assumption
2 | |_ (E > A) Assumption
3 | | |_ D Assumption
4 | | | |_ ~(~(((A > B) > (~C > ~D)) > C) v E) Assumption
5 | | | | |_ E Assumption
6 | | | | | (~(((A > B) > (~C > ~D)) > C) v E) 5 vI
7 | | | | | # 4,6 #I
8 | | | | ~E 5-7 ~I
9 | | | | |_ ~(((A > B) > (~C > ~D)) > C) Assumption
10 | | | | | (~(((A > B) > (~C > ~D)) > C) v E) 9 vI
11 | | | | | # 4,10 #I
12 | | | | ~~(((A > B) > (~C > ~D)) > C) 9-11 ~I
13 | | | | (((A > B) > (~C > ~D)) > C) 12 ~E
14 | | | | E 1,13 >E
15 | | | | # 8,14 #I
16 | | | ~~(~(((A > B) > (~C > ~D)) > C) v E) 4-15 ~I
17 | | | (~(((A > B) > (~C > ~D)) > C) v E) 16 ~E
18 | | | |_ ~(((A > B) > (~C > ~D)) > C) Assumption
19 | | | | |_ ~((A > B) > (~C > ~D)) Assumption
20 | | | | | |_ ((A > B) > (~C > ~D)) Assumption
21 | | | | | | |_ ~C Assumption
22 | | | | | | | # 19,20 #I
23 | | | | | | ~~C 21-22 ~I
24 | | | | | | C 23 ~E
25 | | | | | (((A > B) > (~C > ~D)) > C) 20-24 >I
26 | | | | | # 18,25 #I
27 | | | | ~~((A > B) > (~C > ~D)) 19-26 ~I
28 | | | | ((A > B) > (~C > ~D)) 27 ~E
29 | | | | |_ C Assumption
30 | | | | | |_ ((A > B) > (~C > ~D)) Assumption
31 | | | | | | C 29 Reit
32 | | | | | (((A > B) > (~C > ~D)) > C) 30-31 >I
33 | | | | | # 18,32 #I
34 | | | | ~C 29-33 ~I
35 | | | | |_ ~(~(A > B) v (~C > ~D)) Assumption
36 | | | | | |_ ~(A > B) Assumption
37 | | | | | | (~(A > B) v (~C > ~D)) 36 vI
38 | | | | | | # 35,37 #I
39 | | | | | ~~(A > B) 36-38 ~I
40 | | | | | (A > B) 39 ~E
41 | | | | | |_ (~C > ~D) Assumption
42 | | | | | | (~(A > B) v (~C > ~D)) 41 vI
43 | | | | | | # 35,42 #I
44 | | | | | ~(~C > ~D) 41-43 ~I
45 | | | | | (~C > ~D) 28,40 >E
46 | | | | | # 44,45 #I
47 | | | | ~~(~(A > B) v (~C > ~D)) 35-46 ~I
48 | | | | (~(A > B) v (~C > ~D)) 47 ~E
49 | | | | |_ ~(A > B) Assumption
50 | | | | | |_ ~A Assumption
51 | | | | | | |_ A Assumption
52 | | | | | | | |_ ~B Assumption
53 | | | | | | | | # 50,51 #I
54 | | | | | | | ~~B 52-53 ~I
55 | | | | | | | B 54 ~E
56 | | | | | | (A > B) 51-55 >I
57 | | | | | | # 49,56 #I
58 | | | | | ~~A 50-57 ~I
59 | | | | | A 58 ~E
60 | | | | |_ (~C > ~D) Assumption
61 | | | | | ~D 60,34 >E
62 | | | | | |_ ~A Assumption
63 | | | | | | # 3,61 #I
64 | | | | | ~~A 62-63 ~I
65 | | | | | A 64 ~E
66 | | | | A 48,49-59,60-65 vE
67 | | | |_ E Assumption
68 | | | | A 2,67 >E
69 | | | A 17,18-66,67-68 vE
70 | | (D > A) 3-69 >I
71 | ((E > A) > (D > A)) 2-70 >I
72 (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A))) 1-71 >I
Proofs in Answers
For proofs in answers that do not provide a method for machine-based validation, this section is meant to provide plain text variants compatible with the fitchjs project.
Bram28's proof (26 steps)
Problem: |- (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A))) 1 |_ ((((A > B) > (~C > ~D)) > C) > E) Assumption 2 | |_ (E > A) Assumption 3 | | |_ D Assumption 4 | | | |_ ~A Assumption 5 | | | | |_ A Assumption 6 | | | | | |_ ~B Assumption 7 | | | | | | # 4,5 #I 8 | | | | | ~~B 6-7 ~I 9 | | | | | B 8 ~E 10 | | | | (A > B) 5-9 >I 11 | | | | |_ ((A > B) > (~C > ~D)) Assumption 12 | | | | | (~C > ~D) 11,10 >E 13 | | | | | |_ ~C Assumption 14 | | | | | | ~D 12,13 >E 15 | | | | | | # 3,14 #I 16 | | | | | ~~C 13-15 ~I 17 | | | | | C 16 ~E 18 | | | | (((A > B) > (~C > ~D)) > C) 11-17 >I 19 | | | | E 1,18 >E 20 | | | | A 2,19 >E 21 | | | | # 4,20 #I 22 | | | ~~A 4-21 ~I 23 | | | A 22 ~E 24 | | (D > A) 3-23 >I 25 | ((E > A) > (D > A)) 2-24 >I 26 (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A))) 1-25 >I
Here is a 26 line proof (if you don't count line 1):