Like in Dan Christensens famous Generalized Drinker
Paradox, we can prove, with Q an arbitrary formula:
60 ALL(s):ALL(t):ALL(f):ALL(m):[ALL(a):[a @ s => [a @ t | a @ f | a @ m]
& ~[a @ t & a @ f]
& ~[a @ t & a @ m]
& ~[a @ f & a @ m]]
=> ALL(a):[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]]
4 Conclusion, 1
Proof was done by first proving. I guess something went
exploding, I hope its not Dan Christensens brain!
42 ALL(a):[a @ s => ~[a @ t <=> a @ t => a @ f]]
Rem DNeg, 41
Maybe a short proof is possible?
----------------------------- begin proof ---------------------------
1 ALL(a):[a @ s => [a @ t | a @ f | a @ m]
& ~[a @ t & a @ f]
& ~[a @ t & a @ m]
& ~[a @ f & a @ m]]
Premise
2 ~ALL(a):[a @ s => ~[a @ t <=> a @ t => a @ f]]
Premise
3 ~~EXIST(a):~[a @ s => ~[a @ t <=> a @ t => a @ f]]
Quant, 2
4 EXIST(a):~[a @ s => ~[a @ t <=> a @ t => a @ f]]
Rem DNeg, 3
5 EXIST(a):~~[a @ s & ~~[a @ t <=> a @ t => a @ f]]
Imply-And, 4
6 EXIST(a):[a @ s & ~~[a @ t <=> a @ t => a @ f]]
Rem DNeg, 5
7 EXIST(a):[a @ s & [a @ t <=> a @ t => a @ f]]
Rem DNeg, 6
8 u @ s & [u @ t <=> u @ t => u @ f]
E Spec, 7
9 u @ s
Split, 8
10 u @ t <=> u @ t => u @ f
Split, 8
11 u @ s => [u @ t | u @ f | u @ m]
& ~[u @ t & u @ f]
& ~[u @ t & u @ m]
& ~[u @ f & u @ m]
U Spec, 1
12 [u @ t | u @ f | u @ m]
& ~[u @ t & u @ f]
& ~[u @ t & u @ m]
& ~[u @ f & u @ m]
Detach, 11, 9
13 u @ t | u @ f | u @ m
Split, 12
14 ~[u @ t & u @ f]
Split, 12
15 ~[u @ t & u @ m]
Split, 12
16 ~[u @ f & u @ m]
Split, 12
17 [u @ t => [u @ t => u @ f]] & [u @ t => u @ f => u @ t]
Iff-And, 10
18 u @ t => [u @ t => u @ f]
Split, 17
19 u @ t => u @ f => u @ t
Split, 17
20 u @ f
Premise
21 ~u @ t | u @ f
Arb Or, 20
22 ~~u @ t => u @ f
Imply-Or, 21
23 u @ t => u @ f
Rem DNeg, 22
24 u @ t
Detach, 19, 23
25 u @ t & u @ f
Join, 24, 20
26 ~[u @ t & u @ f] & [u @ t & u @ f]
Join, 14, 25
27 ~u @ f
4 Conclusion, 20
28 ~[u @ t => u @ f] => ~u @ t
Contra, 18
29 ~~[u @ t & ~u @ f] => ~u @ t
Imply-And, 28
30 u @ t & ~u @ f => ~u @ t
Rem DNeg, 29
31 u @ t
Premise
32 u @ t & ~u @ f
Join, 31, 27
33 ~u @ t
Detach, 30, 32
34 u @ t & ~u @ t
Join, 31, 33
35 ~u @ t
4 Conclusion, 31
36 ~u @ t | u @ f
Arb Or, 35
37 ~~u @ t => u @ f
Imply-Or, 36
38 u @ t => u @ f
Rem DNeg, 37
39 u @ t
Detach, 19, 38
40 ~u @ t & u @ t
Join, 35, 39
41 ~~ALL(a):[a @ s => ~[a @ t <=> a @ t => a @ f]]
4 Conclusion, 2
42 ALL(a):[a @ s => ~[a @ t <=> a @ t => a @ f]]
Rem DNeg, 41
43 ~ALL(a):[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]
Premise
44 ~~EXIST(a):~[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]
Quant, 43
45 EXIST(a):~[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]
Rem DNeg, 44
46 EXIST(a):~~[a @ s & ~[[a @ t <=> a @ t => a @ f] => Q]]
Imply-And, 45
47 EXIST(a):[a @ s & ~[[a @ t <=> a @ t => a @ f] => Q]]
Rem DNeg, 46
48 v @ s & ~[[v @ t <=> v @ t => v @ f] => Q]
E Spec, 47
49 v @ s
Split, 48
50 ~[[v @ t <=> v @ t => v @ f] => Q]
Split, 48
51 v @ s => ~[v @ t <=> v @ t => v @ f]
U Spec, 42
52 ~[v @ t <=> v @ t => v @ f]
Detach, 51, 49
53 ~~[[v @ t <=> v @ t => v @ f] & ~Q]
Imply-And, 50
54 [v @ t <=> v @ t => v @ f] & ~Q
Rem DNeg, 53
55 v @ t <=> v @ t => v @ f
Split, 54
56 ~Q
Split, 54
57 [v @ t <=> v @ t => v @ f]
& ~[v @ t <=> v @ t => v @ f]
Join, 55, 52
58 ~~ALL(a):[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]
4 Conclusion, 43
59 ALL(a):[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]
Rem DNeg, 58
60 ALL(s):ALL(t):ALL(f):ALL(m):[ALL(a):[a @ s => [a @ t | a @ f | a @ m]
& ~[a @ t & a @ f]
& ~[a @ t & a @ m]
& ~[a @ f & a @ m]]
=> ALL(a):[a @ s => [[a @ t <=> a @ t => a @ f] => Q]]]
4 Conclusion, 1
----------------------------- end proof ---------------------------