info
Google Группы больше не поддерживают новые публикации и подписки в сети Usenet. Опубликованный ранее контент останется доступен.
Dismiss
Basics of without loss of generaly not understood by DC Proof
67 просмотров
Перейти к первому непрочитанному сообщению
Mostowski Collapse
24 нояб. 2022 г., 15:48:1024.11.2022
–
So it seems that wikipedia has hidden second nugget
in his color example? Did Wonky Man never see a mathematician
use variables x,y,z,... for some colors of some objects.
Why does he insist on nonsense like using a color function.
When there is this easy theorem, for 3 objects:
22 ALL(x):ALL(y):ALL(z):P(x,y,z)
=> ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Conclusion, 2
So on a scale of 1-100 how stupid is Wonky Man.
1000 stupid? Infinitely stupid?
---------------------- begin proof --------------------------------------------
1 ALL(x):color(x) ε c
Axiom
2 ALL(x):ALL(y):ALL(z):P(x,y,z)
Premise
3 ~ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Premise
4 ~~EXIST(u):~ALL(v):ALL(w):P(color(u),color(v),color(w))
Quant, 3
5 EXIST(u):~ALL(v):ALL(w):P(color(u),color(v),color(w))
Rem DNeg, 4
6 EXIST(u):~~EXIST(v):~ALL(w):P(color(u),color(v),color(w))
Quant, 5
7 EXIST(u):EXIST(v):~ALL(w):P(color(u),color(v),color(w))
Rem DNeg, 6
8 EXIST(u):EXIST(v):~~EXIST(w):~P(color(u),color(v),color(w))
Quant, 7
9 EXIST(u):EXIST(v):EXIST(w):~P(color(u),color(v),color(w))
Rem DNeg, 8
10 EXIST(v):EXIST(w):~P(color(u),color(v),color(w))
E Spec, 9
11 EXIST(w):~P(color(u),color(v),color(w))
E Spec, 10
12 ~P(color(u),color(v),color(w))
E Spec, 11
13 color(u) ε c
U Spec, 1
14 color(v) ε c
U Spec, 1
15 color(w) ε c
U Spec, 1
16 ALL(y):ALL(z):P(color(u),y,z)
U Spec, 2, 13
17 ALL(z):P(color(u),color(v),z)
U Spec, 16, 14
18 P(color(u),color(v),color(w))
U Spec, 17, 15
19 ~P(color(u),color(v),color(w))
& P(color(u),color(v),color(w))
Join, 12, 18
20 ~~ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Conclusion, 3
21 ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Rem DNeg, 20
22 ALL(x):ALL(y):ALL(z):P(x,y,z)
=> ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Conclusion, 2
---------------------- end proof --------------------------------------------
in his color example? Did Wonky Man never see a mathematician
use variables x,y,z,... for some colors of some objects.
Why does he insist on nonsense like using a color function.
When there is this easy theorem, for 3 objects:
22 ALL(x):ALL(y):ALL(z):P(x,y,z)
=> ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Conclusion, 2
So on a scale of 1-100 how stupid is Wonky Man.
1000 stupid? Infinitely stupid?
---------------------- begin proof --------------------------------------------
1 ALL(x):color(x) ε c
Axiom
2 ALL(x):ALL(y):ALL(z):P(x,y,z)
Premise
3 ~ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Premise
4 ~~EXIST(u):~ALL(v):ALL(w):P(color(u),color(v),color(w))
Quant, 3
5 EXIST(u):~ALL(v):ALL(w):P(color(u),color(v),color(w))
Rem DNeg, 4
6 EXIST(u):~~EXIST(v):~ALL(w):P(color(u),color(v),color(w))
Quant, 5
7 EXIST(u):EXIST(v):~ALL(w):P(color(u),color(v),color(w))
Rem DNeg, 6
8 EXIST(u):EXIST(v):~~EXIST(w):~P(color(u),color(v),color(w))
Quant, 7
9 EXIST(u):EXIST(v):EXIST(w):~P(color(u),color(v),color(w))
Rem DNeg, 8
10 EXIST(v):EXIST(w):~P(color(u),color(v),color(w))
E Spec, 9
11 EXIST(w):~P(color(u),color(v),color(w))
E Spec, 10
12 ~P(color(u),color(v),color(w))
E Spec, 11
13 color(u) ε c
U Spec, 1
14 color(v) ε c
U Spec, 1
15 color(w) ε c
U Spec, 1
16 ALL(y):ALL(z):P(color(u),y,z)
U Spec, 2, 13
17 ALL(z):P(color(u),color(v),z)
U Spec, 16, 14
18 P(color(u),color(v),color(w))
U Spec, 17, 15
19 ~P(color(u),color(v),color(w))
& P(color(u),color(v),color(w))
Join, 12, 18
20 ~~ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Conclusion, 3
21 ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Rem DNeg, 20
22 ALL(x):ALL(y):ALL(z):P(x,y,z)
=> ALL(u):ALL(v):ALL(w):P(color(u),color(v),color(w))
Conclusion, 2
---------------------- end proof --------------------------------------------
Mostowski Collapse
24 нояб. 2022 г., 15:59:0624.11.2022
–
The theorem works also in Wolfgang Schwartz tree tool:
∀x∀y∀zPxyz → ∀u∀v∀wPc(u)c(v)c(w) is valid.
https://www.umsu.de/trees/#~6x~6y~6zP%28x,y,z%29~5~6u~6v~6wP%28c%28u%29,c%28v%29,c%28w%29%29
With the advantage that the ALL(x):color(x) ε c isn't needed.
∀x∀y∀zPxyz → ∀u∀v∀wPc(u)c(v)c(w) is valid.
https://www.umsu.de/trees/#~6x~6y~6zP%28x,y,z%29~5~6u~6v~6wP%28c%28u%29,c%28v%29,c%28w%29%29
With the advantage that the ALL(x):color(x) ε c isn't needed.
Mostowski Collapse
24 нояб. 2022 г., 17:02:0124.11.2022
–
Hey Wonky Man is your DC Proof tool made of chinesium?
It seems to be extremly fragile, can even not prove the simplest
things. And how do you think the Pigeonhole principle is formulate
in a SAT Solver?
Ask pehou...@gmail.com he will tell you. If you have two boxes
red and blue, and 3 pingeons. So its a Pingeon(2,3) problem,
how will it be formulate? With a function color?
LMAO!
It seems to be extremly fragile, can even not prove the simplest
things. And how do you think the Pigeonhole principle is formulate
in a SAT Solver?
Ask pehou...@gmail.com he will tell you. If you have two boxes
red and blue, and 3 pingeons. So its a Pingeon(2,3) problem,
how will it be formulate? With a function color?
LMAO!
Mostowski Collapse
25 нояб. 2022 г., 02:41:1825.11.2022
–
You are a liar, again and again. Of couse we can prove
your result, you asshole, your are only too stupid.
Its very easy, if you have 3 objects u,v,w,
and their colors color(u)=x, color(v)=y, color(w)=z.
Then if you prove a theorem P(x,y,z) about these
colors, then its also a theorem P(color(u),color(v),color(w)).
your result, you asshole, your are only too stupid.
Its very easy, if you have 3 objects u,v,w,
and their colors color(u)=x, color(v)=y, color(w)=z.
Then if you prove a theorem P(x,y,z) about these
colors, then its also a theorem P(color(u),color(v),color(w)).
Mostowski Collapse
25 нояб. 2022 г., 03:31:0525.11.2022
–
Its not so difficult to remove the color function,
indirection, just prove this theorem:
Theorem: "3 objects either red or blue" => "2 out of 3 all reds or blues"
ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] =>
x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Its then an easy corollary, from the additional assumptions:
ALL(x):[x in c <=> x=r v x=b]
color(u) in c & color(v) in c & color(w) in c
~u=v & ~u=w & ~v=w
To arrive at:
EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
indirection, just prove this theorem:
Theorem: "3 objects either red or blue" => "2 out of 3 all reds or blues"
ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] =>
x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Its then an easy corollary, from the additional assumptions:
ALL(x):[x in c <=> x=r v x=b]
color(u) in c & color(v) in c & color(w) in c
~u=v & ~u=w & ~v=w
To arrive at:
EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Mostowski Collapse
26 нояб. 2022 г., 08:34:0026.11.2022
–
Ha Ha, Wonky Many still doesn't get it. He is still clueless!
Without using color, we have progressed as follows:
We have now available, the intermediate step, specialization
to red, the following new theorem:
Mostowski Collapse schrieb am Samstag, 26. November 2022 um 14:28:04 UTC+1:
> 53 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=r =>
https://groups.google.com/g/sci.math/c/S-AyjY4rK7s/m/w-98GSofBwAJ
And the old theorem of symmetry breaking:
Mostowski Collapse schrieb am Donnerstag, 24. November 2022 um 18:35:47 UTC+1:
> Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues"
> 29 ALL(x):ALL(b):ALL(r):ALL(y):ALL(z):[[x=b | x=r] & [y=b | y=r] & [z=b | z=r] => x=b & y=b | x=r & y=r
> | [x=b & z=b | x=r & z=r]
> | [y=b & z=b | y=r & z=r]
> => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b
> https://groups.google.com/g/sci.math/c/3vtZ4jfP3Y0/m/7h0dWoWPBgAJ
It should now be easy to derive the other specialization
to blue, namely this theorem, without repeating the specialization
proof to red, but using the symmetry breaking theorem:
ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=b =>
Without using color, we have progressed as follows:
We have now available, the intermediate step, specialization
to red, the following new theorem:
Mostowski Collapse schrieb am Samstag, 26. November 2022 um 14:28:04 UTC+1:
> 53 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=r =>
> [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] =>
> x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
> Rem DNeg, 52
> x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
https://groups.google.com/g/sci.math/c/S-AyjY4rK7s/m/w-98GSofBwAJ
And the old theorem of symmetry breaking:
Mostowski Collapse schrieb am Donnerstag, 24. November 2022 um 18:35:47 UTC+1:
> Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues"
> 29 ALL(x):ALL(b):ALL(r):ALL(y):ALL(z):[[x=b | x=r] & [y=b | y=r] & [z=b | z=r] => x=b & y=b | x=r & y=r
> | [x=b & z=b | x=r & z=r]
> | [y=b & z=b | y=r & z=r]
> => [[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b
> | [x=r & z=r | x=b & z=b]
> | [y=r & z=r | y=b & z=b]]]
> Conclusion, 3
> | [y=r & z=r | y=b & z=b]]]
> https://groups.google.com/g/sci.math/c/3vtZ4jfP3Y0/m/7h0dWoWPBgAJ
It should now be easy to derive the other specialization
to blue, namely this theorem, without repeating the specialization
proof to red, but using the symmetry breaking theorem:
ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[x=b =>
[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] =>
x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]]
Mostowski Collapse
26 нояб. 2022 г., 10:50:1626.11.2022
–
The lifting doesn't even need the premis ~u=v & ~u=w & ~v=w,
its a little long, but also simpler than I though concering the
needed premisses to prove:
117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Rem DNeg, 116
Here is the full proof:
----------------------------- begin proof ----------------------------
3 objects either red ir blue => 2 out of 3 all reds or blues
1 ALL(x):ALL(y):ALL(z):ALL(r):ALL(b):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b]
2 ALL(x):[x ε c <=> x=r | x=b]
Axiom
3 color(u) ε c & color(v) ε c & color(w) ε c
Axiom
4 color(u) ε c
Split, 3
5 color(v) ε c
Split, 3
6 color(w) ε c
Split, 3
7 ALL(y):ALL(z):ALL(r):ALL(b):[[color(u)=r | color(u)=b] & [y=r | y=b] & [z=r | z=b] => color(u)=r & y=r | color(u)=b & y=b | [color(u)=r & z=r | color(u)=b & z=b]
8 ALL(z):ALL(r):ALL(b):[[color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [z=r | z=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & z=r | color(u)=b & z=b]
| [color(v)=r & z=r | color(v)=b & z=b]]
U Spec, 7, 5
9 ALL(r):ALL(b):[[color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]]
U Spec, 8, 6
10 ALL(b):[[color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]]
U Spec, 9
11 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
U Spec, 10
12 color(u) ε c <=> color(u)=r | color(u)=b
U Spec, 2, 4
13 [color(u) ε c => color(u)=r | color(u)=b]
& [color(u)=r | color(u)=b => color(u) ε c]
Iff-And, 12
14 color(u) ε c => color(u)=r | color(u)=b
Split, 13
15 color(u)=r | color(u)=b => color(u) ε c
Split, 13
16 color(u)=r | color(u)=b
Detach, 14, 4
17 color(v) ε c <=> color(v)=r | color(v)=b
U Spec, 2, 5
18 [color(v) ε c => color(v)=r | color(v)=b]
& [color(v)=r | color(v)=b => color(v) ε c]
Iff-And, 17
19 color(v) ε c => color(v)=r | color(v)=b
Split, 18
20 color(v)=r | color(v)=b => color(v) ε c
Split, 18
21 color(v)=r | color(v)=b
Detach, 19, 5
22 color(w) ε c <=> color(w)=r | color(w)=b
U Spec, 2, 6
23 [color(w) ε c => color(w)=r | color(w)=b]
& [color(w)=r | color(w)=b => color(w) ε c]
Iff-And, 22
24 color(w) ε c => color(w)=r | color(w)=b
Split, 23
25 color(w)=r | color(w)=b => color(w) ε c
Split, 23
26 color(w)=r | color(w)=b
Detach, 24, 6
27 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
Join, 16, 21
28 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
& [color(w)=r | color(w)=b]
Join, 27, 26
29 color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Detach, 11, 28
30 ~[color(u)=color(v) | color(u)=color(w) | color(v)=color(w)]
Premise
31 ~~[~[color(u)=color(v) | color(u)=color(w)] & ~color(v)=color(w)]
DeMorgan, 30
32 ~[color(u)=color(v) | color(u)=color(w)] & ~color(v)=color(w)
Rem DNeg, 31
33 ~~[~color(u)=color(v) & ~color(u)=color(w)] & ~color(v)=color(w)
DeMorgan, 32
34 ~color(u)=color(v) & ~color(u)=color(w) & ~color(v)=color(w)
Rem DNeg, 33
35 ~color(u)=color(v)
Split, 34
36 ~color(u)=color(w)
Split, 34
37 ~color(v)=color(w)
Split, 34
38 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Imply-Or, 29
39 ~~[~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
DeMorgan, 38
40 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Rem DNeg, 39
41 color(u)=r & color(v)=r | color(u)=b & color(v)=b
Premise
42 ~[color(u)=r & color(v)=r] => color(u)=b & color(v)=b
Imply-Or, 41
43 color(u)=r & color(v)=r
Premise
44 color(u)=r
Split, 43
45 color(v)=r
Split, 43
46 ~r=color(v)
Substitute, 44, 35
47 r=color(v)
Sym, 45
48 ~r=color(v) & r=color(v)
Join, 46, 47
49 ~[color(u)=r & color(v)=r]
Conclusion, 43
50 color(u)=b & color(v)=b
Detach, 42, 49
51 color(u)=b
Split, 50
52 color(v)=b
Split, 50
53 ~b=color(v)
Substitute, 51, 35
54 b=color(v)
Sym, 52
55 ~b=color(v) & b=color(v)
Join, 53, 54
56 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
Conclusion, 41
57 color(u)=r & color(w)=r | color(u)=b & color(w)=b
Premise
58 ~[color(u)=r & color(w)=r] => color(u)=b & color(w)=b
Imply-Or, 57
59 color(u)=r & color(w)=r
Premise
60 color(u)=r
Split, 59
61 color(w)=r
Split, 59
62 ~r=color(w)
Substitute, 60, 36
63 r=color(w)
Sym, 61
64 ~r=color(w) & r=color(w)
Join, 62, 63
65 ~[color(u)=r & color(w)=r]
Conclusion, 59
66 color(u)=b & color(w)=b
Detach, 58, 65
67 color(u)=b
Split, 66
68 color(w)=b
Split, 66
69 ~b=color(w)
Substitute, 67, 36
70 b=color(w)
Sym, 68
71 ~b=color(w) & b=color(w)
Join, 69, 70
72 ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Conclusion, 57
73 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
& ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Join, 56, 72
74 color(v)=r & color(w)=r | color(v)=b & color(w)=b
Detach, 40, 73
75 ~[color(v)=r & color(w)=r] => color(v)=b & color(w)=b
Imply-Or, 74
76 color(v)=r & color(w)=r
Premise
77 color(v)=r
Split, 76
78 color(w)=r
Split, 76
79 ~r=color(w)
Substitute, 77, 37
80 r=color(w)
Sym, 78
81 ~r=color(w) & r=color(w)
Join, 79, 80
82 ~[color(v)=r & color(w)=r]
Conclusion, 76
83 color(v)=b & color(w)=b
Detach, 75, 82
84 color(v)=b
Split, 83
85 color(w)=b
Split, 83
86 ~b=color(w)
Substitute, 84, 37
87 b=color(w)
Sym, 85
88 ~b=color(w) & b=color(w)
Join, 86, 87
89 ~~[color(u)=color(v) | color(u)=color(w) | color(v)=color(w)]
Conclusion, 30
90 color(u)=color(v) | color(u)=color(w) | color(v)=color(w)
Rem DNeg, 89
91 ~EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Premise
92 ~~ALL(p):~EXIST(q):[~p=q => color(p)=color(q)]
Quant, 91
93 ALL(p):~EXIST(q):[~p=q => color(p)=color(q)]
Rem DNeg, 92
94 ALL(p):~~ALL(q):~[~p=q => color(p)=color(q)]
Quant, 93
95 ALL(p):ALL(q):~[~p=q => color(p)=color(q)]
Rem DNeg, 94
96 ALL(p):ALL(q):~~[~p=q & ~color(p)=color(q)]
Imply-And, 95
97 ALL(p):ALL(q):[~p=q & ~color(p)=color(q)]
Rem DNeg, 96
98 ~[color(u)=color(v) | color(u)=color(w)] => color(v)=color(w)
Imply-Or, 90
99 ~~[~color(u)=color(v) & ~color(u)=color(w)] => color(v)=color(w)
DeMorgan, 98
100 ~color(u)=color(v) & ~color(u)=color(w) => color(v)=color(w)
Rem DNeg, 99
101 ALL(q):[~u=q & ~color(u)=color(q)]
U Spec, 97
102 ~u=v & ~color(u)=color(v)
U Spec, 101
103 ~u=v
Split, 102
104 ~color(u)=color(v)
Split, 102
105 ALL(q):[~u=q & ~color(u)=color(q)]
U Spec, 97
106 ~u=w & ~color(u)=color(w)
U Spec, 105
107 ~u=w
Split, 106
108 ~color(u)=color(w)
Split, 106
109 ~color(u)=color(v) & ~color(u)=color(w)
Join, 104, 108
110 color(v)=color(w)
Detach, 100, 109
111 ALL(q):[~v=q & ~color(v)=color(q)]
U Spec, 97
112 ~v=w & ~color(v)=color(w)
U Spec, 111
113 ~v=w
Split, 112
114 ~color(v)=color(w)
Split, 112
115 color(v)=color(w) & ~color(v)=color(w)
Join, 110, 114
116 ~~EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Conclusion, 91
117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Rem DNeg, 116
----------------------------- end proof -------------------------------
its a little long, but also simpler than I though concering the
needed premisses to prove:
117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Rem DNeg, 116
Here is the full proof:
----------------------------- begin proof ----------------------------
3 objects either red ir blue => 2 out of 3 all reds or blues
1 ALL(x):ALL(y):ALL(z):ALL(r):ALL(b):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b] => x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b]
| [y=r & z=r | y=b & z=b]]
Axiom
2 ALL(x):[x ε c <=> x=r | x=b]
Axiom
3 color(u) ε c & color(v) ε c & color(w) ε c
Axiom
4 color(u) ε c
Split, 3
5 color(v) ε c
Split, 3
6 color(w) ε c
Split, 3
7 ALL(y):ALL(z):ALL(r):ALL(b):[[color(u)=r | color(u)=b] & [y=r | y=b] & [z=r | z=b] => color(u)=r & y=r | color(u)=b & y=b | [color(u)=r & z=r | color(u)=b & z=b]
| [y=r & z=r | y=b & z=b]]
U Spec, 1, 4
8 ALL(z):ALL(r):ALL(b):[[color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [z=r | z=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & z=r | color(u)=b & z=b]
| [color(v)=r & z=r | color(v)=b & z=b]]
U Spec, 7, 5
9 ALL(r):ALL(b):[[color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]]
U Spec, 8, 6
10 ALL(b):[[color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]]
U Spec, 9
11 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
U Spec, 10
12 color(u) ε c <=> color(u)=r | color(u)=b
U Spec, 2, 4
13 [color(u) ε c => color(u)=r | color(u)=b]
& [color(u)=r | color(u)=b => color(u) ε c]
Iff-And, 12
14 color(u) ε c => color(u)=r | color(u)=b
Split, 13
15 color(u)=r | color(u)=b => color(u) ε c
Split, 13
16 color(u)=r | color(u)=b
Detach, 14, 4
17 color(v) ε c <=> color(v)=r | color(v)=b
U Spec, 2, 5
18 [color(v) ε c => color(v)=r | color(v)=b]
& [color(v)=r | color(v)=b => color(v) ε c]
Iff-And, 17
19 color(v) ε c => color(v)=r | color(v)=b
Split, 18
20 color(v)=r | color(v)=b => color(v) ε c
Split, 18
21 color(v)=r | color(v)=b
Detach, 19, 5
22 color(w) ε c <=> color(w)=r | color(w)=b
U Spec, 2, 6
23 [color(w) ε c => color(w)=r | color(w)=b]
& [color(w)=r | color(w)=b => color(w) ε c]
Iff-And, 22
24 color(w) ε c => color(w)=r | color(w)=b
Split, 23
25 color(w)=r | color(w)=b => color(w) ε c
Split, 23
26 color(w)=r | color(w)=b
Detach, 24, 6
27 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
Join, 16, 21
28 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
& [color(w)=r | color(w)=b]
Join, 27, 26
29 color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Detach, 11, 28
30 ~[color(u)=color(v) | color(u)=color(w) | color(v)=color(w)]
Premise
31 ~~[~[color(u)=color(v) | color(u)=color(w)] & ~color(v)=color(w)]
DeMorgan, 30
32 ~[color(u)=color(v) | color(u)=color(w)] & ~color(v)=color(w)
Rem DNeg, 31
33 ~~[~color(u)=color(v) & ~color(u)=color(w)] & ~color(v)=color(w)
DeMorgan, 32
34 ~color(u)=color(v) & ~color(u)=color(w) & ~color(v)=color(w)
Rem DNeg, 33
35 ~color(u)=color(v)
Split, 34
36 ~color(u)=color(w)
Split, 34
37 ~color(v)=color(w)
Split, 34
38 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Imply-Or, 29
39 ~~[~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
DeMorgan, 38
40 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Rem DNeg, 39
41 color(u)=r & color(v)=r | color(u)=b & color(v)=b
Premise
42 ~[color(u)=r & color(v)=r] => color(u)=b & color(v)=b
Imply-Or, 41
43 color(u)=r & color(v)=r
Premise
44 color(u)=r
Split, 43
45 color(v)=r
Split, 43
46 ~r=color(v)
Substitute, 44, 35
47 r=color(v)
Sym, 45
48 ~r=color(v) & r=color(v)
Join, 46, 47
49 ~[color(u)=r & color(v)=r]
Conclusion, 43
50 color(u)=b & color(v)=b
Detach, 42, 49
51 color(u)=b
Split, 50
52 color(v)=b
Split, 50
53 ~b=color(v)
Substitute, 51, 35
54 b=color(v)
Sym, 52
55 ~b=color(v) & b=color(v)
Join, 53, 54
56 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
Conclusion, 41
57 color(u)=r & color(w)=r | color(u)=b & color(w)=b
Premise
58 ~[color(u)=r & color(w)=r] => color(u)=b & color(w)=b
Imply-Or, 57
59 color(u)=r & color(w)=r
Premise
60 color(u)=r
Split, 59
61 color(w)=r
Split, 59
62 ~r=color(w)
Substitute, 60, 36
63 r=color(w)
Sym, 61
64 ~r=color(w) & r=color(w)
Join, 62, 63
65 ~[color(u)=r & color(w)=r]
Conclusion, 59
66 color(u)=b & color(w)=b
Detach, 58, 65
67 color(u)=b
Split, 66
68 color(w)=b
Split, 66
69 ~b=color(w)
Substitute, 67, 36
70 b=color(w)
Sym, 68
71 ~b=color(w) & b=color(w)
Join, 69, 70
72 ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Conclusion, 57
73 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
& ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Join, 56, 72
74 color(v)=r & color(w)=r | color(v)=b & color(w)=b
Detach, 40, 73
75 ~[color(v)=r & color(w)=r] => color(v)=b & color(w)=b
Imply-Or, 74
76 color(v)=r & color(w)=r
Premise
77 color(v)=r
Split, 76
78 color(w)=r
Split, 76
79 ~r=color(w)
Substitute, 77, 37
80 r=color(w)
Sym, 78
81 ~r=color(w) & r=color(w)
Join, 79, 80
82 ~[color(v)=r & color(w)=r]
Conclusion, 76
83 color(v)=b & color(w)=b
Detach, 75, 82
84 color(v)=b
Split, 83
85 color(w)=b
Split, 83
86 ~b=color(w)
Substitute, 84, 37
87 b=color(w)
Sym, 85
88 ~b=color(w) & b=color(w)
Join, 86, 87
89 ~~[color(u)=color(v) | color(u)=color(w) | color(v)=color(w)]
Conclusion, 30
90 color(u)=color(v) | color(u)=color(w) | color(v)=color(w)
Rem DNeg, 89
91 ~EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Premise
92 ~~ALL(p):~EXIST(q):[~p=q => color(p)=color(q)]
Quant, 91
93 ALL(p):~EXIST(q):[~p=q => color(p)=color(q)]
Rem DNeg, 92
94 ALL(p):~~ALL(q):~[~p=q => color(p)=color(q)]
Quant, 93
95 ALL(p):ALL(q):~[~p=q => color(p)=color(q)]
Rem DNeg, 94
96 ALL(p):ALL(q):~~[~p=q & ~color(p)=color(q)]
Imply-And, 95
97 ALL(p):ALL(q):[~p=q & ~color(p)=color(q)]
Rem DNeg, 96
98 ~[color(u)=color(v) | color(u)=color(w)] => color(v)=color(w)
Imply-Or, 90
99 ~~[~color(u)=color(v) & ~color(u)=color(w)] => color(v)=color(w)
DeMorgan, 98
100 ~color(u)=color(v) & ~color(u)=color(w) => color(v)=color(w)
Rem DNeg, 99
101 ALL(q):[~u=q & ~color(u)=color(q)]
U Spec, 97
102 ~u=v & ~color(u)=color(v)
U Spec, 101
103 ~u=v
Split, 102
104 ~color(u)=color(v)
Split, 102
105 ALL(q):[~u=q & ~color(u)=color(q)]
U Spec, 97
106 ~u=w & ~color(u)=color(w)
U Spec, 105
107 ~u=w
Split, 106
108 ~color(u)=color(w)
Split, 106
109 ~color(u)=color(v) & ~color(u)=color(w)
Join, 104, 108
110 color(v)=color(w)
Detach, 100, 109
111 ALL(q):[~v=q & ~color(v)=color(q)]
U Spec, 97
112 ~v=w & ~color(v)=color(w)
U Spec, 111
113 ~v=w
Split, 112
114 ~color(v)=color(w)
Split, 112
115 color(v)=color(w) & ~color(v)=color(w)
Join, 110, 114
116 ~~EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Conclusion, 91
117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
Rem DNeg, 116
----------------------------- end proof -------------------------------
Dan Christensen
26 нояб. 2022 г., 16:12:4926.11.2022
–
On Saturday, November 26, 2022 at 10:50:16 AM UTC-5, Mostowski Collapse wrote:
> The lifting doesn't even need the premis ~u=v & ~u=w & ~v=w,
> its a little long, but also simpler than I though concering the
> needed premisses to prove:
>
> 117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
> Rem DNeg, 116
>
[snip]
> The lifting doesn't even need the premis ~u=v & ~u=w & ~v=w,
> its a little long, but also simpler than I though concering the
> needed premisses to prove:
>
> 117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
> Rem DNeg, 116
>
In what way does this make use of the WLOG method of proof as you promised?
See my reply to you just now to your similar posting just now in the thread, "'Without loss of generality' may not be formalizable."
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Mostowski Collapse
27 нояб. 2022 г., 05:33:1127.11.2022
–
You are definitively a moron. Cognitive science tells us
that a human being can typically hold 7 (seven) items in
short term memory. In your case its 0 (zero) items.
Still clueless how the proof works? Right?
Coke Alfero
27 нояб. 2022 г., 11:51:1527.11.2022
–
Mostowski Collapse wrote:
> You are definitively a moron. Cognitive science tells us that a human
> being can typically hold 7 (seven) items in short term memory. In your
> case its 0 (zero) items.
>
> Still clueless how the proof works? Right?
>
> Dan Christensen schrieb am Samstag, 26. November 2022 um 22:12:49 UTC+1:
read about these modrefakers here. They already said Dr. Stalin kill them
> You are definitively a moron. Cognitive science tells us that a human
> being can typically hold 7 (seven) items in short term memory. In your
> case its 0 (zero) items.
>
> Still clueless how the proof works? Right?
>
> Dan Christensen schrieb am Samstag, 26. November 2022 um 22:12:49 UTC+1:
with famine in their country.
EU country faces drastic food inflation
Swedish households are struggling with rising costs for basic goods and
energy, the latest report shows
https://%72%74.com/business/567129-sweden-food-energy-inflation/
“In our calculations we are taking into account only basic needs and not
some luxurious consumption,” a manager from the Swedish Consumer Agency,
Kristina Difs, said in a statement. She noted that usually an increase in
annual expenses is insignificant, while this year “we have seen numbers
quickly lose relevance.”
Dan Christensen
27 нояб. 2022 г., 12:49:2327.11.2022
–
Speaking of wars, how is your genocidal war of conquest and terror in Ukraine going, Nazi Boy? Let's just say that your Red Army ain't what it used to be!
Do you at least have plan for going into hiding? You will likely be hunted as a war criminal in the not too distant future.
Coke Alfero
27 нояб. 2022 г., 14:19:4827.11.2022
–
Dan Christensen wrote:
>> > Dan Christensen schrieb am Samstag, 26. November 2022 um 22:12:49
>> > UTC+1:
>> read about these modrefakers here. They already said Dr. Stalin kill
>> them with famine in their country.
>>
>> EU country faces drastic food inflation Swedish households are
>> struggling with rising costs for basic goods and energy, the latest
>> report shows
>> https://%72%74.com/business/567129-sweden-food-energy-inflation/
>>
>> “In our calculations we are taking into account only basic needs and
>> not some luxurious consumption,” a manager from the Swedish Consumer
>> Agency,
>> Kristina Difs, said in a statement. She noted that usually an increase
>> in annual expenses is insignificant, while this year “we have seen
>> numbers quickly lose relevance.”
>
> Times of pandemics and war are rarely times of plenty.
I beg to differ. You get what you fucking deserve. It's your lie, not Dr.
>> > Dan Christensen schrieb am Samstag, 26. November 2022 um 22:12:49
>> > UTC+1:
>> read about these modrefakers here. They already said Dr. Stalin kill
>> them with famine in their country.
>>
>> EU country faces drastic food inflation Swedish households are
>> struggling with rising costs for basic goods and energy, the latest
>> report shows
>> https://%72%74.com/business/567129-sweden-food-energy-inflation/
>>
>> “In our calculations we are taking into account only basic needs and
>> not some luxurious consumption,” a manager from the Swedish Consumer
>> Agency,
>> Kristina Difs, said in a statement. She noted that usually an increase
>> in annual expenses is insignificant, while this year “we have seen
>> numbers quickly lose relevance.”
>
> Times of pandemics and war are rarely times of plenty.
Stalin. Dr. Stalin was a wonderful human being, putting to real work all
these cacapitalist modrefakar around here. What we need is Dr. Stalin
today.
more you lie, more you suffer, you stupid capitalist bitch. And if you
don't suffer enough, the justing castro trudeau and bill gaytes comes with
serum to kill you faster, as they say, is more "human" than the capitalist
*death_panels*. You fucking nazi idiots. Just continue lying.
Coke Alfero
27 нояб. 2022 г., 14:21:5027.11.2022
–
Dan Christensen wrote:
>> read about these modrefakers here. They already said Dr. Stalin kill
>> them with famine in their country.
>>
>> EU country faces drastic food inflation Swedish households are
>> struggling with rising costs for basic goods and energy, the latest
>> report shows
>> https://%72%74.com/business/567129-sweden-food-energy-inflation/
>>
>> “In our calculations we are taking into account only basic needs and
>> not some luxurious consumption,” a manager from the Swedish Consumer
>> Agency,
>> Kristina Difs, said in a statement. She noted that usually an increase
>> in annual expenses is insignificant, while this year “we have seen
>> numbers quickly lose relevance.”
>
> Times of pandemics and war are rarely times of plenty.
amazing, having eight years (8) a man as *first_lady* they called
>> read about these modrefakers here. They already said Dr. Stalin kill
>> them with famine in their country.
>>
>> EU country faces drastic food inflation Swedish households are
>> struggling with rising costs for basic goods and energy, the latest
>> report shows
>> https://%72%74.com/business/567129-sweden-food-energy-inflation/
>>
>> “In our calculations we are taking into account only basic needs and
>> not some luxurious consumption,” a manager from the Swedish Consumer
>> Agency,
>> Kristina Difs, said in a statement. She noted that usually an increase
>> in annual expenses is insignificant, while this year “we have seen
>> numbers quickly lose relevance.”
>
> Times of pandemics and war are rarely times of plenty.
*Michael* by mistake. Just continue lying, you depraved sondre bitches. Go
bomb a country, for whatever reason, Iraq, and so on.
Mostowski Collapse
27 нояб. 2022 г., 16:14:1827.11.2022
–
Maybe a dramatic simplification of the WLOG problem,
so that dumbo Wonky Man understands it, would be to
view the coloring as a subset C ⊆ {0,1,2}. With the meaning:
k ∈ C <=> object k is colored red
k ∉ C <=> object k is colored blue
The desired theorem then says, for arbitary C, there are k,j such that
{k,j} ⊆ C v {k,j} ⊆ C' where C' = {0,1,2} \ C
A proof fixing k=0 and k ∈ C, and then fixing and doing
the other case k ∉ C can be done on C', with k ∈ C' again,
which is obviously essentially the same theorem to prove:
{k,j} ⊆ C' v {k,j} ⊆ C where C = {0,1,2} \ C'
So the theorem has to be only proved once, k ∈ C,
and k ∉ C follows from some symmetry breaking.
so that dumbo Wonky Man understands it, would be to
view the coloring as a subset C ⊆ {0,1,2}. With the meaning:
k ∈ C <=> object k is colored red
k ∉ C <=> object k is colored blue
The desired theorem then says, for arbitary C, there are k,j such that
{k,j} ⊆ C v {k,j} ⊆ C' where C' = {0,1,2} \ C
A proof fixing k=0 and k ∈ C, and then fixing and doing
the other case k ∉ C can be done on C', with k ∈ C' again,
which is obviously essentially the same theorem to prove:
{k,j} ⊆ C' v {k,j} ⊆ C where C = {0,1,2} \ C'
So the theorem has to be only proved once, k ∈ C,
and k ∉ C follows from some symmetry breaking.
Mostowski Collapse
27 нояб. 2022 г., 16:23:2527.11.2022
–
This could relieve dumbo Wonky Man from his baggage
of color function, and finally allow him to quantify
over the problem space, like for example
ALL(C): ....
Where C is the set that models the problem. This
is necessary for the without loss of generality argument,
because it is an argument that disects the problem
space, basically you would show that for every
problem C there is a dual problem C'. Thats maybe
easier to do for dumbo Wonky Man, with a set C,
than with a color function.
of color function, and finally allow him to quantify
over the problem space, like for example
ALL(C): ....
Where C is the set that models the problem. This
is necessary for the without loss of generality argument,
because it is an argument that disects the problem
space, basically you would show that for every
problem C there is a dual problem C'. Thats maybe
easier to do for dumbo Wonky Man, with a set C,
than with a color function.
Dan Christensen
27 нояб. 2022 г., 23:02:5327.11.2022
–
See my reply to you just now in the thread "'Without loss of generality' may not be formalizable."
On Sunday, November 27, 2022 at 4:23:25 PM UTC-5, Mostowski Collapse wrote:
> [snip childish abuse]
On Sunday, November 27, 2022 at 4:23:25 PM UTC-5, Mostowski Collapse wrote:
> [snip childish abuse]
Mostowski Collapse
28 нояб. 2022 г., 07:50:0728.11.2022
–
Ok, there is a typo somewhere, I should redo this
annoying proof, and then show instead:
EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Maybe will nevertheless need ~u=v & ~u=w & ~v=w?
Who knows? Dickhead Wonky Man?
A useful lemma could be, interestingly DC Poop
wants me to quantify over the function symbol f:
Lemma 4: Some equality swizzling
38 ALL(f):ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Rem DNeg, 37
------------------------------------ begin proof ----------------------------------------
1 ~ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Premise
2 ~~EXIST(x):~ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 1
3 EXIST(x):~ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 2
4 EXIST(x):~~EXIST(y):~ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 3
5 EXIST(x):EXIST(y):~ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 4
6 EXIST(x):EXIST(y):~~EXIST(s):~ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 5
7 EXIST(x):EXIST(y):EXIST(s):~ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 6
8 EXIST(x):EXIST(y):EXIST(s):~~EXIST(t):~[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 7
9 EXIST(x):EXIST(y):EXIST(s):EXIST(t):~[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 8
10 EXIST(x):EXIST(y):EXIST(s):EXIST(t):~~[~color(x)=color(y) & ~~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Imply-And, 9
11 EXIST(x):EXIST(y):EXIST(s):EXIST(t):[~color(x)=color(y) & ~~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 10
12 EXIST(x):EXIST(y):EXIST(s):EXIST(t):[~color(x)=color(y) & [color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 11
13 EXIST(y):EXIST(s):EXIST(t):[~color(u)=color(y) & [color(u)=s & color(y)=s | color(u)=t & color(y)=t]]
E Spec, 12
14 EXIST(s):EXIST(t):[~color(u)=color(v) & [color(u)=s & color(v)=s | color(u)=t & color(v)=t]]
E Spec, 13
15 EXIST(t):[~color(u)=color(v) & [color(u)=r & color(v)=r | color(u)=t & color(v)=t]]
E Spec, 14
16 ~color(u)=color(v) & [color(u)=r & color(v)=r | color(u)=b & color(v)=b]
E Spec, 15
17 ~color(u)=color(v)
Split, 16
18 color(u)=r & color(v)=r | color(u)=b & color(v)=b
Split, 16
19 ~[color(u)=r & color(v)=r] => color(u)=b & color(v)=b
Imply-Or, 18
20 color(u)=r & color(v)=r
Premise
21 color(u)=r
Split, 20
22 color(v)=r
Split, 20
23 ~r=color(v)
Substitute, 21, 17
24 ~r=r
Substitute, 22, 23
25 r=r
Reflex
26 ~r=r & r=r
Join, 24, 25
27 ~[color(u)=r & color(v)=r]
Conclusion, 20
28 color(u)=b & color(v)=b
Detach, 19, 27
29 color(u)=b
Split, 28
30 color(v)=b
Split, 28
31 ~b=color(v)
Substitute, 29, 17
32 ~b=b
Substitute, 30, 31
33 b=b
Reflex
34 ~b=b & b=b
Join, 32, 33
35 ~EXIST(f):~ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Conclusion, 1
36 ~~ALL(f):~~ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Quant, 35
37 ALL(f):~~ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Rem DNeg, 36
38 ALL(f):ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Rem DNeg, 37
------------------------------------ end proof ----------------------------------------
annoying proof, and then show instead:
EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Maybe will nevertheless need ~u=v & ~u=w & ~v=w?
Who knows? Dickhead Wonky Man?
A useful lemma could be, interestingly DC Poop
wants me to quantify over the function symbol f:
Lemma 4: Some equality swizzling
38 ALL(f):ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Rem DNeg, 37
------------------------------------ begin proof ----------------------------------------
1 ~ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Premise
2 ~~EXIST(x):~ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 1
3 EXIST(x):~ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 2
4 EXIST(x):~~EXIST(y):~ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 3
5 EXIST(x):EXIST(y):~ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 4
6 EXIST(x):EXIST(y):~~EXIST(s):~ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 5
7 EXIST(x):EXIST(y):EXIST(s):~ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 6
8 EXIST(x):EXIST(y):EXIST(s):~~EXIST(t):~[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Quant, 7
9 EXIST(x):EXIST(y):EXIST(s):EXIST(t):~[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 8
10 EXIST(x):EXIST(y):EXIST(s):EXIST(t):~~[~color(x)=color(y) & ~~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Imply-And, 9
11 EXIST(x):EXIST(y):EXIST(s):EXIST(t):[~color(x)=color(y) & ~~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 10
12 EXIST(x):EXIST(y):EXIST(s):EXIST(t):[~color(x)=color(y) & [color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
Rem DNeg, 11
13 EXIST(y):EXIST(s):EXIST(t):[~color(u)=color(y) & [color(u)=s & color(y)=s | color(u)=t & color(y)=t]]
E Spec, 12
14 EXIST(s):EXIST(t):[~color(u)=color(v) & [color(u)=s & color(v)=s | color(u)=t & color(v)=t]]
E Spec, 13
15 EXIST(t):[~color(u)=color(v) & [color(u)=r & color(v)=r | color(u)=t & color(v)=t]]
E Spec, 14
16 ~color(u)=color(v) & [color(u)=r & color(v)=r | color(u)=b & color(v)=b]
E Spec, 15
17 ~color(u)=color(v)
Split, 16
18 color(u)=r & color(v)=r | color(u)=b & color(v)=b
Split, 16
19 ~[color(u)=r & color(v)=r] => color(u)=b & color(v)=b
Imply-Or, 18
20 color(u)=r & color(v)=r
Premise
21 color(u)=r
Split, 20
22 color(v)=r
Split, 20
23 ~r=color(v)
Substitute, 21, 17
24 ~r=r
Substitute, 22, 23
25 r=r
Reflex
26 ~r=r & r=r
Join, 24, 25
27 ~[color(u)=r & color(v)=r]
Conclusion, 20
28 color(u)=b & color(v)=b
Detach, 19, 27
29 color(u)=b
Split, 28
30 color(v)=b
Split, 28
31 ~b=color(v)
Substitute, 29, 17
32 ~b=b
Substitute, 30, 31
33 b=b
Reflex
34 ~b=b & b=b
Join, 32, 33
35 ~EXIST(f):~ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Conclusion, 1
36 ~~ALL(f):~~ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Quant, 35
37 ALL(f):~~ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Rem DNeg, 36
38 ALL(f):ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Rem DNeg, 37
------------------------------------ end proof ----------------------------------------
Mostowski Collapse
28 нояб. 2022 г., 08:03:0128.11.2022
–
Ok, that ~u=v & ~u=w & ~v=w wasn´t needed was
a kind of proof smell, so needed to revise the proof,
in particular a different theorem is now proved.
Using the lemma, we can prove, now ~u=v & ~u=w & ~v=w
was used. We find the following conclusion:
76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Rem DNeg, 75
---------------------------- begin proof -----------------------------
3 objects either red or blue => 2 out of 3 all reds or blues
1 ALL(x):ALL(y):ALL(z):ALL(s):ALL(t):[[x=s | x=t] & [y=s | y=t] & [z=s | z=t] => x=s & y=s | x=t & y=t | [x=s & z=s | x=t & z=t]
| [y=s & z=s | y=t & z=t]]
Axiom
Lemma 4: Some equality swizzling
2 ALL(f):ALL(x):ALL(y):ALL(s):ALL(t):[~f(x)=f(y) => ~[f(x)=s & f(y)=s | f(x)=t & f(y)=t]]
Axiom
3 ALL(x):[x ε c <=> x=r | x=b]
Axiom
4 color(u) ε c & color(v) ε c & color(w) ε c
Axiom
5 ~u=v & ~u=w & ~v=w
Axiom
6 ~EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Premise
7 ~~ALL(p):~EXIST(q):[~p=q & color(p)=color(q)]
Quant, 6
8 ALL(p):~EXIST(q):[~p=q & color(p)=color(q)]
Rem DNeg, 7
9 ALL(p):~~ALL(q):~[~p=q & color(p)=color(q)]
Quant, 8
10 ALL(p):ALL(q):~[~p=q & color(p)=color(q)]
Rem DNeg, 9
11 ALL(p):ALL(q):~~[~p=q => ~color(p)=color(q)]
Imply-And, 10
12 ALL(p):ALL(q):[~p=q => ~color(p)=color(q)]
Rem DNeg, 11
13 color(u) ε c
Split, 4
14 color(v) ε c
Split, 4
15 color(w) ε c
Split, 4
16 color(u) ε c <=> color(u)=r | color(u)=b
U Spec, 3, 13
17 [color(u) ε c => color(u)=r | color(u)=b]
18 color(u) ε c => color(u)=r | color(u)=b
Split, 17
19 color(u)=r | color(u)=b => color(u) ε c
Split, 17
20 color(u)=r | color(u)=b
Detach, 18, 13
21 color(v) ε c <=> color(v)=r | color(v)=b
U Spec, 3, 14
22 [color(v) ε c => color(v)=r | color(v)=b]
23 color(v) ε c => color(v)=r | color(v)=b
Split, 22
24 color(v)=r | color(v)=b => color(v) ε c
Split, 22
25 color(v)=r | color(v)=b
Detach, 23, 14
26 color(w) ε c <=> color(w)=r | color(w)=b
U Spec, 3, 15
27 [color(w) ε c => color(w)=r | color(w)=b]
28 color(w) ε c => color(w)=r | color(w)=b
Split, 27
29 color(w)=r | color(w)=b => color(w) ε c
Split, 27
30 color(w)=r | color(w)=b
Detach, 28, 15
31 ALL(y):ALL(z):ALL(s):ALL(t):[[color(u)=s | color(u)=t] & [y=s | y=t] & [z=s | z=t] => color(u)=s & y=s | color(u)=t & y=t | [color(u)=s & z=s | color(u)=t & z=t]
| [y=s & z=s | y=t & z=t]]
U Spec, 1, 13
32 ALL(z):ALL(s):ALL(t):[[color(u)=s | color(u)=t] & [color(v)=s | color(v)=t] & [z=s | z=t] => color(u)=s & color(v)=s | color(u)=t & color(v)=t | [color(u)=s & z=s | color(u)=t & z=t]
| [color(v)=s & z=s | color(v)=t & z=t]]
U Spec, 31, 14
33 ALL(s):ALL(t):[[color(u)=s | color(u)=t] & [color(v)=s | color(v)=t] & [color(w)=s | color(w)=t] => color(u)=s & color(v)=s | color(u)=t & color(v)=t | [color(u)=s & color(w)=s | color(u)=t & color(w)=t]
| [color(v)=s & color(w)=s | color(v)=t & color(w)=t]]
U Spec, 32, 15
34 ALL(t):[[color(u)=r | color(u)=t] & [color(v)=r | color(v)=t] & [color(w)=r | color(w)=t] => color(u)=r & color(v)=r | color(u)=t & color(v)=t | [color(u)=r & color(w)=r | color(u)=t & color(w)=t]
| [color(v)=r & color(w)=r | color(v)=t & color(w)=t]]
U Spec, 33
35 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
36 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
Join, 20, 25
37 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
& [color(w)=r | color(w)=b]
Join, 36, 30
38 color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
39 ~u=v
Split, 5
40 ~u=w
Split, 5
41 ~v=w
Split, 5
42 ALL(q):[~u=q => ~color(u)=color(q)]
U Spec, 12
43 ~u=v => ~color(u)=color(v)
U Spec, 42
44 ~color(u)=color(v)
Detach, 43, 39
45 ALL(q):[~u=q => ~color(u)=color(q)]
U Spec, 12
46 ~u=w => ~color(u)=color(w)
U Spec, 45
47 ~color(u)=color(w)
Detach, 46, 40
48 ALL(q):[~v=q => ~color(v)=color(q)]
U Spec, 12
49 ~v=w => ~color(v)=color(w)
U Spec, 48
50 ~color(v)=color(w)
Detach, 49, 41
51 ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
U Spec, 2
52 ALL(y):ALL(s):ALL(t):[~color(u)=color(y) => ~[color(u)=s & color(y)=s | color(u)=t & color(y)=t]]
U Spec, 51
53 ALL(s):ALL(t):[~color(u)=color(v) => ~[color(u)=s & color(v)=s | color(u)=t & color(v)=t]]
U Spec, 52
54 ALL(t):[~color(u)=color(v) => ~[color(u)=r & color(v)=r | color(u)=t & color(v)=t]]
U Spec, 53
55 ~color(u)=color(v) => ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
U Spec, 54
56 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
Detach, 55, 44
57 ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
U Spec, 2
58 ALL(y):ALL(s):ALL(t):[~color(u)=color(y) => ~[color(u)=s & color(y)=s | color(u)=t & color(y)=t]]
U Spec, 57
59 ALL(s):ALL(t):[~color(u)=color(w) => ~[color(u)=s & color(w)=s | color(u)=t & color(w)=t]]
U Spec, 58
60 ALL(t):[~color(u)=color(w) => ~[color(u)=r & color(w)=r | color(u)=t & color(w)=t]]
U Spec, 59
61 ~color(u)=color(w) => ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
U Spec, 60
62 ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Detach, 61, 47
63 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
64 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Imply-Or, 38
65 ~~[~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
DeMorgan, 64
66 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Rem DNeg, 65
67 color(v)=r & color(w)=r | color(v)=b & color(w)=b
Detach, 66, 63
68 ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
U Spec, 2
69 ALL(y):ALL(s):ALL(t):[~color(v)=color(y) => ~[color(v)=s & color(y)=s | color(v)=t & color(y)=t]]
U Spec, 68
70 ALL(s):ALL(t):[~color(v)=color(w) => ~[color(v)=s & color(w)=s | color(v)=t & color(w)=t]]
U Spec, 69
71 ALL(t):[~color(v)=color(w) => ~[color(v)=r & color(w)=r | color(v)=t & color(w)=t]]
U Spec, 70
72 ~color(v)=color(w) => ~[color(v)=r & color(w)=r | color(v)=b & color(w)=b]
U Spec, 71
73 ~[color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Detach, 72, 50
74 [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
& ~[color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Join, 67, 73
75 ~~EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Conclusion, 6
76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Rem DNeg, 75
---------------------------- end proof -----------------------------
a kind of proof smell, so needed to revise the proof,
in particular a different theorem is now proved.
Using the lemma, we can prove, now ~u=v & ~u=w & ~v=w
was used. We find the following conclusion:
76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Rem DNeg, 75
---------------------------- begin proof -----------------------------
3 objects either red or blue => 2 out of 3 all reds or blues
| [y=s & z=s | y=t & z=t]]
Axiom
Lemma 4: Some equality swizzling
Axiom
3 ALL(x):[x ε c <=> x=r | x=b]
Axiom
4 color(u) ε c & color(v) ε c & color(w) ε c
Axiom
5 ~u=v & ~u=w & ~v=w
Axiom
6 ~EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Premise
7 ~~ALL(p):~EXIST(q):[~p=q & color(p)=color(q)]
Quant, 6
8 ALL(p):~EXIST(q):[~p=q & color(p)=color(q)]
Rem DNeg, 7
9 ALL(p):~~ALL(q):~[~p=q & color(p)=color(q)]
Quant, 8
10 ALL(p):ALL(q):~[~p=q & color(p)=color(q)]
Rem DNeg, 9
11 ALL(p):ALL(q):~~[~p=q => ~color(p)=color(q)]
Imply-And, 10
12 ALL(p):ALL(q):[~p=q => ~color(p)=color(q)]
Rem DNeg, 11
13 color(u) ε c
Split, 4
14 color(v) ε c
Split, 4
15 color(w) ε c
Split, 4
16 color(u) ε c <=> color(u)=r | color(u)=b
U Spec, 3, 13
17 [color(u) ε c => color(u)=r | color(u)=b]
& [color(u)=r | color(u)=b => color(u) ε c]
Iff-And, 16
18 color(u) ε c => color(u)=r | color(u)=b
Split, 17
19 color(u)=r | color(u)=b => color(u) ε c
Split, 17
20 color(u)=r | color(u)=b
Detach, 18, 13
21 color(v) ε c <=> color(v)=r | color(v)=b
U Spec, 3, 14
22 [color(v) ε c => color(v)=r | color(v)=b]
& [color(v)=r | color(v)=b => color(v) ε c]
Iff-And, 21
23 color(v) ε c => color(v)=r | color(v)=b
Split, 22
24 color(v)=r | color(v)=b => color(v) ε c
Split, 22
25 color(v)=r | color(v)=b
Detach, 23, 14
26 color(w) ε c <=> color(w)=r | color(w)=b
U Spec, 3, 15
27 [color(w) ε c => color(w)=r | color(w)=b]
& [color(w)=r | color(w)=b => color(w) ε c]
Iff-And, 26
28 color(w) ε c => color(w)=r | color(w)=b
Split, 27
29 color(w)=r | color(w)=b => color(w) ε c
Split, 27
30 color(w)=r | color(w)=b
Detach, 28, 15
31 ALL(y):ALL(z):ALL(s):ALL(t):[[color(u)=s | color(u)=t] & [y=s | y=t] & [z=s | z=t] => color(u)=s & y=s | color(u)=t & y=t | [color(u)=s & z=s | color(u)=t & z=t]
| [y=s & z=s | y=t & z=t]]
U Spec, 1, 13
32 ALL(z):ALL(s):ALL(t):[[color(u)=s | color(u)=t] & [color(v)=s | color(v)=t] & [z=s | z=t] => color(u)=s & color(v)=s | color(u)=t & color(v)=t | [color(u)=s & z=s | color(u)=t & z=t]
| [color(v)=s & z=s | color(v)=t & z=t]]
U Spec, 31, 14
33 ALL(s):ALL(t):[[color(u)=s | color(u)=t] & [color(v)=s | color(v)=t] & [color(w)=s | color(w)=t] => color(u)=s & color(v)=s | color(u)=t & color(v)=t | [color(u)=s & color(w)=s | color(u)=t & color(w)=t]
| [color(v)=s & color(w)=s | color(v)=t & color(w)=t]]
U Spec, 32, 15
34 ALL(t):[[color(u)=r | color(u)=t] & [color(v)=r | color(v)=t] & [color(w)=r | color(w)=t] => color(u)=r & color(v)=r | color(u)=t & color(v)=t | [color(u)=r & color(w)=r | color(u)=t & color(w)=t]
| [color(v)=r & color(w)=r | color(v)=t & color(w)=t]]
U Spec, 33
35 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b] & [color(w)=r | color(w)=b] => color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
U Spec, 34
36 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
Join, 20, 25
37 [color(u)=r | color(u)=b] & [color(v)=r | color(v)=b]
& [color(w)=r | color(w)=b]
Join, 36, 30
38 color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]
| [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Detach, 35, 37
39 ~u=v
Split, 5
40 ~u=w
Split, 5
41 ~v=w
Split, 5
42 ALL(q):[~u=q => ~color(u)=color(q)]
U Spec, 12
43 ~u=v => ~color(u)=color(v)
U Spec, 42
44 ~color(u)=color(v)
Detach, 43, 39
45 ALL(q):[~u=q => ~color(u)=color(q)]
U Spec, 12
46 ~u=w => ~color(u)=color(w)
U Spec, 45
47 ~color(u)=color(w)
Detach, 46, 40
48 ALL(q):[~v=q => ~color(v)=color(q)]
U Spec, 12
49 ~v=w => ~color(v)=color(w)
U Spec, 48
50 ~color(v)=color(w)
Detach, 49, 41
51 ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
U Spec, 2
52 ALL(y):ALL(s):ALL(t):[~color(u)=color(y) => ~[color(u)=s & color(y)=s | color(u)=t & color(y)=t]]
U Spec, 51
53 ALL(s):ALL(t):[~color(u)=color(v) => ~[color(u)=s & color(v)=s | color(u)=t & color(v)=t]]
U Spec, 52
54 ALL(t):[~color(u)=color(v) => ~[color(u)=r & color(v)=r | color(u)=t & color(v)=t]]
U Spec, 53
55 ~color(u)=color(v) => ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
U Spec, 54
56 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
Detach, 55, 44
57 ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
U Spec, 2
58 ALL(y):ALL(s):ALL(t):[~color(u)=color(y) => ~[color(u)=s & color(y)=s | color(u)=t & color(y)=t]]
U Spec, 57
59 ALL(s):ALL(t):[~color(u)=color(w) => ~[color(u)=s & color(w)=s | color(u)=t & color(w)=t]]
U Spec, 58
60 ALL(t):[~color(u)=color(w) => ~[color(u)=r & color(w)=r | color(u)=t & color(w)=t]]
U Spec, 59
61 ~color(u)=color(w) => ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
U Spec, 60
62 ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Detach, 61, 47
63 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b]
& ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]
Join, 56, 62
64 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b | [color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Imply-Or, 38
65 ~~[~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b]] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
DeMorgan, 64
66 ~[color(u)=r & color(v)=r | color(u)=b & color(v)=b] & ~[color(u)=r & color(w)=r | color(u)=b & color(w)=b] => color(v)=r & color(w)=r | color(v)=b & color(w)=b
Rem DNeg, 65
67 color(v)=r & color(w)=r | color(v)=b & color(w)=b
Detach, 66, 63
68 ALL(x):ALL(y):ALL(s):ALL(t):[~color(x)=color(y) => ~[color(x)=s & color(y)=s | color(x)=t & color(y)=t]]
U Spec, 2
69 ALL(y):ALL(s):ALL(t):[~color(v)=color(y) => ~[color(v)=s & color(y)=s | color(v)=t & color(y)=t]]
U Spec, 68
70 ALL(s):ALL(t):[~color(v)=color(w) => ~[color(v)=s & color(w)=s | color(v)=t & color(w)=t]]
U Spec, 69
71 ALL(t):[~color(v)=color(w) => ~[color(v)=r & color(w)=r | color(v)=t & color(w)=t]]
U Spec, 70
72 ~color(v)=color(w) => ~[color(v)=r & color(w)=r | color(v)=b & color(w)=b]
U Spec, 71
73 ~[color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Detach, 72, 50
74 [color(v)=r & color(w)=r | color(v)=b & color(w)=b]
& ~[color(v)=r & color(w)=r | color(v)=b & color(w)=b]
Join, 67, 73
75 ~~EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Conclusion, 6
76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
Rem DNeg, 75
---------------------------- end proof -----------------------------
Mild Shock
4 июн. 2023 г., 15:44:0004.06.2023
–
Except in the case of Generalized Drinker Paradox.
LoL
LoL
Mild Shock
5 июн. 2023 г., 06:09:4905.06.2023
–
I have a new theory about the Generalized Drinker Paradox.
Maybe its only a change in letter, from small to capital letter:
WLOG = Without Loss of Generality
wLOG = With Loss of Generality
BTW: Here is a 2OGeneralizedGeneralizedGeneralizedDrinkerParadox,
we went down from the real line, to yet something smaller, the
boolean domain:
/* propositional second order generalized generalized generalized drinker paradox,
abbreviated 2OGeneralizedGeneralizedGeneralizedDrinkerParadox */
EXIST(x):[[x <=> s] => Q(x,s)]]
Maybe its only a change in letter, from small to capital letter:
WLOG = Without Loss of Generality
wLOG = With Loss of Generality
BTW: Here is a 2OGeneralizedGeneralizedGeneralizedDrinkerParadox,
we went down from the real line, to yet something smaller, the
boolean domain:
/* propositional second order generalized generalized generalized drinker paradox,
abbreviated 2OGeneralizedGeneralizedGeneralizedDrinkerParadox */
EXIST(x):[[x <=> s] => Q(x,s)]]
Mild Shock
5 июн. 2023 г., 06:13:4305.06.2023
–
In the 2OGeneralizedGeneralizedGeneralizedDrinkerParadox
we directly aim for "jim" the variable s. So the statement
x <=> s says that x is "jim". There is only "jim" and "not jim".
0 новых сообщений