One more last lemma:

Lemma 4: Swap "2 out of 3 all reds or blues"

37 ALL(x):ALL(r):ALL(y):ALL(b):ALL(z):[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=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]]
Conclusion, 2

---------------------------------- begin proof ---------------------------------------------

Lemma 2: Swap "two reds or two blues"

1 ALL(s):ALL(p):ALL(t):ALL(q):[s=p & t=p | s=q & t=q => s=q & t=q | s=p & t=p]
Axiom

2 x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]
Premise

3 ~[x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]]
Premise

4 ~~[~[x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r]] & ~[y=b & z=b | y=r & z=r]]
DeMorgan, 3

5 ~[x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r]] & ~[y=b & z=b | y=r & z=r]
Rem DNeg, 4

6 ~~[~[x=b & y=b | x=r & y=r] & ~[x=b & z=b | x=r & z=r]] & ~[y=b & z=b | y=r & z=r]
DeMorgan, 5

7 ~[x=b & y=b | x=r & y=r] & ~[x=b & z=b | x=r & z=r] & ~[y=b & z=b | y=r & z=r]
Rem DNeg, 6

8 ~[x=b & y=b | x=r & y=r]
Split, 7

9 ~[x=b & z=b | x=r & z=r]
Split, 7

10 ~[y=b & z=b | y=r & z=r]
Split, 7

11 ~[x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b]] => y=r & z=r | y=b & z=b
Imply-Or, 2

12 ~[y=r & z=r | y=b & z=b] => ~~[x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b]]
Contra, 11

13 ALL(p):ALL(t):ALL(q):[y=p & t=p | y=q & t=q => y=q & t=q | y=p & t=p]
U Spec, 1

14 ALL(t):ALL(q):[y=r & t=r | y=q & t=q => y=q & t=q | y=r & t=r]
U Spec, 13

15 ALL(q):[y=r & z=r | y=q & z=q => y=q & z=q | y=r & z=r]
U Spec, 14

16 y=r & z=r | y=b & z=b => y=b & z=b | y=r & z=r
U Spec, 15

17 ~[y=b & z=b | y=r & z=r] => ~[y=r & z=r | y=b & z=b]
Contra, 16

18 ~[y=r & z=r | y=b & z=b]
Detach, 17, 10

19 ~~[x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b]]
Detach, 12, 18

20 x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b]
Rem DNeg, 19

21 ~[x=r & y=r | x=b & y=b] => x=r & z=r | x=b & z=b
Imply-Or, 20

22 ALL(p):ALL(t):ALL(q):[x=p & t=p | x=q & t=q => x=q & t=q | x=p & t=p]
U Spec, 1

23 ALL(t):ALL(q):[x=r & t=r | x=q & t=q => x=q & t=q | x=r & t=r]
U Spec, 22

24 ALL(q):[x=r & y=r | x=q & y=q => x=q & y=q | x=r & y=r]
U Spec, 23

25 x=r & y=r | x=b & y=b => x=b & y=b | x=r & y=r
U Spec, 24

26 ~[x=b & y=b | x=r & y=r] => ~[x=r & y=r | x=b & y=b]
Contra, 25

27 ~[x=r & y=r | x=b & y=b]
Detach, 26, 8

28 x=r & z=r | x=b & z=b
Detach, 21, 27

29 ALL(p):ALL(t):ALL(q):[x=p & t=p | x=q & t=q => x=q & t=q | x=p & t=p]
U Spec, 1

30 ALL(t):ALL(q):[x=r & t=r | x=q & t=q => x=q & t=q | x=r & t=r]
U Spec, 29

31 ALL(q):[x=r & z=r | x=q & z=q => x=q & z=q | x=r & z=r]
U Spec, 30

32 x=r & z=r | x=b & z=b => x=b & z=b | x=r & z=r
U Spec, 31

33 x=b & z=b | x=r & z=r
Detach, 32, 28

34 ~[x=b & z=b | x=r & z=r] & [x=b & z=b | x=r & z=r]
Join, 9, 33

35 ~~[x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]]
Conclusion, 3

36 x=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]
Rem DNeg, 35

37 ALL(x):ALL(r):ALL(y):ALL(b):ALL(z):[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=b & y=b | x=r & y=r | [x=b & z=b | x=r & z=r] | [y=b & z=b | y=r & z=r]]
Conclusion, 2

Mostowski Collapse schrieb am Donnerstag, 24. November 2022 um 17:59:38 UTC+1:
> One more lemma:
>
> Lemma 3: Swap "3 objects either red or blue"
>
> 26 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
> => [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
> Conclusion, 2
>
> ---------------------------- begin proof ------------------------------------
> Lemma 1: Swap "either red or blue"
> 1 ALL(x):ALL(r):ALL(b):[x=r | x=b => x=b | x=r]
> Axiom
>
> 2 [x=r | x=b] & [y=r | y=b] & [z=r | z=b]
> Premise
>
> 3 ~[[x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
> Premise
>
> 4 x=r | x=b
> Split, 2
>
> 5 y=r | y=b
> Split, 2
>
> 6 z=r | z=b
> Split, 2
>
> 7 ~~[[x=b | x=r] & [y=b | y=r] => ~[z=b | z=r]]
> Imply-And, 3
>
> 8 [x=b | x=r] & [y=b | y=r] => ~[z=b | z=r]
> Rem DNeg, 7
>
> 9 ALL(r):ALL(b):[x=r | x=b => x=b | x=r]
> U Spec, 1
>
> 10 ALL(b):[x=r | x=b => x=b | x=r]
> U Spec, 9
>
> 11 x=r | x=b => x=b | x=r
> U Spec, 10
>
> 12 x=b | x=r
> Detach, 11, 4
>
> 13 ALL(r):ALL(b):[y=r | y=b => y=b | y=r]
> U Spec, 1
>
> 14 ALL(b):[y=r | y=b => y=b | y=r]
> U Spec, 13
>
> 15 y=r | y=b => y=b | y=r
> U Spec, 14
>
> 16 y=b | y=r
> Detach, 15, 5
>
> 17 [x=b | x=r] & [y=b | y=r]
> Join, 12, 16
>
> 18 ~[z=b | z=r]
> Detach, 8, 17
>
> 19 ALL(r):ALL(b):[z=r | z=b => z=b | z=r]
> U Spec, 1
>
> 20 ALL(b):[z=r | z=b => z=b | z=r]
> U Spec, 19
>
> 21 z=r | z=b => z=b | z=r
> U Spec, 20
>
> 22 z=b | z=r
> Detach, 21, 6
>
> 23 ~[z=b | z=r] & [z=b | z=r]
> Join, 18, 22
>
> 24 ~~[[x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
> Conclusion, 3
>
> 25 [x=b | x=r] & [y=b | y=r] & [z=b | z=r]
> Rem DNeg, 24
>
> 26 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
> => [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
> Conclusion, 2
> Dan Christensen schrieb am Donnerstag, 24. November 2022 um 17:54:05 UTC+1:
> > On Thursday, November 24, 2022 at 11:36:38 AM UTC-5, Forest Vaccaro wrote:
> >
> > > nobody is talking with you, eating the burger, the french fries and
> > > getting the vaccine. [snip]
> >
> > Hey, Nazi Boy, you seem to have your work cut out for you promoting your boyfriend Putin's interests and his genocidal war of conquest and terror in Ukraine. Sadly for both of you, your Red Army ain't what it used to be.

On Thursday, November 24, 2022 at 12:20:20 PM UTC-5, Mostowski Collapse (Jan Burse) wrote:
> One more last lemma:
>
> Lemma 4: Swap "2 out of 3 all reds or blues" [snip]

Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."

Dan

Finally the symmetry breaking theorem:

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

---------------------------- begin proof --------------------------------------

Lemma 3: Swap "3 objects either red or blue"

1 ALL(x):ALL(r):ALL(b):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
=> [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
Axiom

Lemma 4: Swap "2 out of 3 all reds or blues"

2 ALL(x):ALL(p):ALL(y):ALL(q):ALL(z):[x=p & y=p | x=q & y=q | [x=p & z=p | x=q & z=q] | [y=p & z=p | y=q & z=q]
=> x=q & y=q | x=p & y=p | [x=q & z=q | x=p & z=p] | [y=q & z=q | y=p & z=p]]
Axiom

3 [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]
Premise

4 ~[[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]]
Premise

5 ~~[[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]]]
Imply-And, 4

6 [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, 5

7 x=r | x=b
Split, 6

8 y=r | y=b
Split, 6

9 z=r | z=b
Split, 6

10 ~[x=r & y=r | x=b & y=b
| [x=r & z=r | x=b & z=b]
| [y=r & z=r | y=b & z=b]]
Split, 6

11 [x=r | x=b] & [y=r | y=b]
Join, 7, 8

12 [x=r | x=b] & [y=r | y=b] & [z=r | z=b]
Join, 11, 9

13 ALL(r):ALL(b):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
=> [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
U Spec, 1

14 ALL(b):ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
=> [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
U Spec, 13

15 ALL(y):ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
=> [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
U Spec, 14

16 ALL(z):[[x=r | x=b] & [y=r | y=b] & [z=r | z=b]
=> [x=b | x=r] & [y=b | y=r] & [z=b | z=r]]
U Spec, 15

17 [x=r | x=b] & [y=r | y=b] & [z=r | z=b]
=> [x=b | x=r] & [y=b | y=r] & [z=b | z=r]
U Spec, 16

18 [x=b | x=r] & [y=b | y=r] & [z=b | z=r]
Detach, 17, 12

19 x=b & y=b | x=r & y=r
| [x=b & z=b | x=r & z=r]
| [y=b & z=b | y=r & z=r]
Detach, 3, 18

20 ALL(p):ALL(y):ALL(q):ALL(z):[x=p & y=p | x=q & y=q | [x=p & z=p | x=q & z=q] | [y=p & z=p | y=q & z=q]
=> x=q & y=q | x=p & y=p | [x=q & z=q | x=p & z=p] | [y=q & z=q | y=p & z=p]]
U Spec, 2

21 ALL(y):ALL(q):ALL(z):[x=b & y=b | x=q & y=q | [x=b & z=b | x=q & z=q] | [y=b & z=b | y=q & z=q]
=> x=q & y=q | x=b & y=b | [x=q & z=q | x=b & z=b] | [y=q & z=q | y=b & z=b]]
U Spec, 20

22 ALL(q):ALL(z):[x=b & y=b | x=q & y=q | [x=b & z=b | x=q & z=q] | [y=b & z=b | y=q & z=q]
=> x=q & y=q | x=b & y=b | [x=q & z=q | x=b & z=b] | [y=q & z=q | y=b & z=b]]
U Spec, 21

23 ALL(z):[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 & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]]
U Spec, 22

24 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 & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]
U Spec, 23

25 x=r & y=r | x=b & y=b | [x=r & z=r | x=b & z=b] | [y=r & z=r | y=b & z=b]
Detach, 24, 19

26 [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]]
Join, 25, 10

27 ~~[[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, 4

28 [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, 27

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

---------------------------- end proof --------------------------------------

Dan Christensen schrieb am Donnerstag, 24. November 2022 um 01:27:56 UTC+1:
> On Wednesday, November 23, 2022 at 5:53:21 PM UTC-5, Mostowski Collapse wrote:
> > Come on, you can quantify over function symbols in DC Proof.
> > It should not be so difficult to prove for red blue colorings:
> >
> > ALL(color):EXIST(color2):ALL(x):[
> > (color(x)=red => color2(x)=blue) &
> > (color(x)=blue => color2(x)=red
> [snip]
>
> We are STILL waiting for even the first line of the formal proof of your claim that there exists some kind of formal mathematical shortcut. Will it be a premise? Or an axiom? What then will be the 2nd or 3rd line? Poor Jan Burse doesn't have clue. Oh, well...
>
> Dan

Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."

Dan

On Thursday, November 24, 2022 at 12:35:47 PM UTC-5, Mostowski Collapse wrote:
> Finally the symmetry breaking theorem:
>
> Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues"
>
[snip]

Yeah, very interesting nonsense topic.

LoL

Dan Christensen schrieb am Donnerstag, 24. November 2022 um 18:42:41 UTC+1:
> Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."
>
> Dan
> On Thursday, November 24, 2022 at 12:35:47 PM UTC-5, Mostowski Collapse wrote:
> > Finally the symmetry breaking theorem:
> >
> > Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues"
> >
> [snip]

Did you sit in a brain vacuum wormhole while posting?

Or did simply the usual Wonky Man drugs kick in?

LMAO!

Mostowski Collapse schrieb:
> Yeah, very interesting nonsense topic.
>
> LoL
>
> Dan Christensen schrieb am Donnerstag, 24. November 2022 um 18:42:41 UTC+1:
>> Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."
>>
>> Dan
>> On Thursday, November 24, 2022 at 12:35:47 PM UTC-5, Mostowski Collapse wrote:
>>> Finally the symmetry breaking theorem:
>>>
>>> Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues"
>>>
>> [snip]

Mostowski Collapse wrote:

> Yeah, very interesting nonsense topic. LoL
>
> Dan Christensen schrieb am Donnerstag, 24. November 2022 um 18:42:41
> UTC+1:
>> Please stay on topic, Jan Burse. See the thread, "'Without loss of

nice to meet you. Here you have some khazars, from khazaria, stealing
*_$4_billions_* from people, on an deeply illegal pyramid game / ponzi
scheme. NOT *judged_and_executed*. But talking freely in "seminars" for
stealing. You just can't make this shit up. This is america. Driven gay
comedians on cocaine as *_"president"_*. Blowing up energy pipeline of
other countries and continents as *_tremendous_opportunity_*.

https://cms.zerohedge.com/s3/files/inline-images/NYT%20speakers.jpg

Howls Of Outrage After New York Times Confirms SBF To Speak Alongside
Zelenskyy, Yellen
https://www.zerohedge.com/markets/howls-outrage-after-new-york-times-
confirms-sbf-speak-alongside-zelenskyy-yellen-dealbook

https://assets.zerohedge.com/s3fs-public/styles/inline_image_mobile/
public/inline-images/sbf%20and%20bill%20clinton_1.png

Mostowski Collapse wrote:

> Did you sit in a brain vacuum wormhole while posting?
> Or did simply the usual Wonky Man drugs kick in? LMAO!
>
> Mostowski Collapse schrieb:
>> Yeah, very interesting nonsense topic.

how's the weather in Khakholekistan? Here you have some khazars, from khazaria, stealing *_$4_billions_* from people, along a deeply illegal pyramid game / ponzi scheme. NOT *judged_and_executed*. But speaking freely in "seminars" for stealing. You can't make this shit up. This is america. Driven *gay_comedians* on cocaine as *_"president"s_*. Blowing up energy pipelines of other countries and continents, as *_tremendous_opportunity_*.

https://cms.zerohedge.com/s3/files/inline-images/NYT%20speakers.jpg

Howls Of Outrage After New York Times Confirms SBF To Speak Alongside
Zelenskyy, Yellen
https://www.zerohedge.com/markets/howls-outrage-after-new-york-times-confirms-sbf-speak-alongside-zelenskyy-yellen-dealbook

https://assets.zerohedge.com/s3fs-public/styles/inline_image_mobile/public/inline-images/sbf%20and%20bill%20clinton_1.png

The swapping works also with SAT Solver version
of Pigeon principle, that is related to the WLOG example:

If we try to place 3 pigeons in 2 boxes, we get this
conjunctive normal form (CNF_1):

X11 v X12
X21 v X22
X31 v X32
~X11 v ~X21
~X11 v ~X31
~X21 v ~X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32

Now if we swap indices of the two boxes, we
get another conjunctive normal form (CNF_2):

X12 v X11
X22 v X21
X32 v X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32
~X11 v ~X21
~X11 v ~X31
~X21 v ~X31

But obviously CNF_1 => CNF_2, and of course
also CNF_1 => CNF_2, they are logically equivalent.

But I agree with Fritz that Wikipedia is a little nonsensical.
Since they write the following:

"Assume, without loss of generality, that the first object is red."
https://en.wikipedia.org/wiki/Without_loss_of_generality

This could be read as not only a choice of a color, but also a
choice of a pigeon. Its basically a DPLL step: Set x11 to true,
and see what happens, via unit propagation we get a reduced formula:

X21 v X22
X31 v X32
~X21
~X31
~X21 v ~X31
~X12 v ~X22
~X12 v ~X32
~X22 v ~X32

But we could also start with any other variable, an other color
or another pigeon, or another color and another pigeon. The
problem is now that DPLL is not based on symmetry breaking,

as a next step it would try to set X11 to false. So there could
be indeed a problem, in that another reading of Wikipedia doesn't
show without loss of generality as we would wish.

It would only give an example of a kind of order independence,
which is a common phenomenon for many algorithms, even
if there is no symmetry breaking:

Davis–Putnam–Logemann–Loveland (DPLL) algorithm
https://en.wikipedia.org/wiki/DPLL_algorithm

Mostowski Collapse schrieb am Donnerstag, 24. November 2022 um 23:32:38 UTC+1:
> The swapping works also with SAT Solver version
> of Pigeon principle, that is related to the WLOG example:
>
> If we try to place 3 pigeons in 2 boxes, we get this
> conjunctive normal form (CNF_1):
>
> X11 v X12
> X21 v X22
> X31 v X32
> ~X11 v ~X21
> ~X11 v ~X31
> ~X21 v ~X31
> ~X12 v ~X22
> ~X12 v ~X32
> ~X22 v ~X32
>
> Now if we swap indices of the two boxes, we
> get another conjunctive normal form (CNF_2):
>
> X12 v X11
> X22 v X21
> X32 v X31
> ~X12 v ~X22
> ~X12 v ~X32
> ~X22 v ~X32
> ~X11 v ~X21
> ~X11 v ~X31
> ~X21 v ~X31
>
> But obviously CNF_1 => CNF_2, and of course
> also CNF_1 => CNF_2, they are logically equivalent.

Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."

Dan

On Thursday, November 24, 2022 at 5:33:46 PM UTC-5, Mostowski Collapse wrote:
> But I agree with Fritz that Wikipedia is a little nonsensical.
> Since they write the following:
>
> "Assume, without loss of generality, that the first object is red."
> https://en.wikipedia.org/wiki/Without_loss_of_generality
>
> This could be read as not only a choice of a color, but also a
> choice of a pigeon. Its basically a DPLL step: Set x11 to true,
> and see what happens, via unit propagation we get a reduced formula:
> X21 v X22
[snip]

Hurry clueless Wonky Man. I am very close to completing
a prove that uses "Without loss of generality" reasoning.
Your prove here is stupid as usual, repeating speczialization

to red and blue twice? Pretty pointless to illustrate
"Without loss of generality" as you noticed yourself:

I have been unable to formally justify the without-loss-of-generality claim.
https://www.dcproof.com/WithoutLossOfGenerality.htm (new version)

On the other hand I already got that far. So I am a blink
away from justifying without-loss-of-generality:

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
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
> https://groups.google.com/g/sci.math/c/3vtZ4jfP3Y0/m/7h0dWoWPBgAJ

Hurry Wonky Man, or it gets quite awkward for DC Poop.
Its already extremly awkward for DC Poop, its getting more nasty now.

Dan Christensen schrieb am Freitag, 25. November 2022 um 00:23:51 UTC+1:
> Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."
>
> Dan
> On Thursday, November 24, 2022 at 5:33:46 PM UTC-5, Mostowski Collapse wrote:
> > But I agree with Fritz that Wikipedia is a little nonsensical.
> > Since they write the following:
> >
> > "Assume, without loss of generality, that the first object is red."
> > https://en.wikipedia.org/wiki/Without_loss_of_generality
> >
> > This could be read as not only a choice of a color, but also a
> > choice of a pigeon. Its basically a DPLL step: Set x11 to true,
> > and see what happens, via unit propagation we get a reduced formula:
> > X21 v X22
> [snip]

Please stay on topic, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."

Dan

On Saturday, November 26, 2022 at 8:41:42 AM UTC-5, Mostowski Collapse wrote:
[snip childish abuse]

> I am very close to completing
> a prove that uses "Without loss of generality" reasoning.
> Your prove here is stupid as usual, repeating speczialization
>
[snip]

So Dan Christensen is absolutely clueless why
A v ~A, the law of excluded middle, is so problematic
in constructive mathematics.

Here is a hint: Assume I give you an infinite sequence
a1, a2, a3, ... and I ask you is there some aj < 0. Lets
say this question is A.

You can answer A if you find an index j with aj < 0. A
procedure for that would be to inspect one after the
other a1, a2, a3, ... until you find aj < 0.

What is the procedure to answer ~A ? Do we really
have constructively A v ~A ?

On Saturday, December 24, 2022 at 8:37:20 PM UTC-5, Mostowski Collapse wrote:
> So Dan Christensen is absolutely clueless why
> A v ~A, the law of excluded middle, is so problematic
> in constructive mathematics.
>

Because it makes math too easy for students?

> Here is a hint: Assume I give you an infinite sequence
> a1, a2, a3, ... and I ask you is there some aj < 0. Lets
> say this question is A.
>
> You can answer A if you find an index j with aj < 0. A
> procedure for that would be to inspect one after the
> other a1, a2, a3, ... until you find aj < 0.
>
> What is the procedure to answer ~A ?

I am not aware of any such general procedure.

Dan

Can you make an example? What do you mean by "it"
and what you you mean by "easy" when you write "Because
it makes math too easy for students?"?

Isn't your 2nd statement "I am not aware of any such
general procedure." evidence that nothing is easy, that
there is some difficulty somewhere?

Whats wrong with you?

Don't they have libraries where you can rent books at the place
you live? I guess there are at least 10 books that explain the
subset intuitionstic logic of classical logic,

other names for the subset are constructive mathematic, there
is a close relationship. Get an eduction sick boy.

Dan Christensen schrieb am Sonntag, 25. Dezember 2022 um 15:31:24 UTC+11:
> On Saturday, December 24, 2022 at 8:37:20 PM UTC-5, Mostowski Collapse wrote:
> > So Dan Christensen is absolutely clueless why
> > A v ~A, the law of excluded middle, is so problematic
> > in constructive mathematics.
> >
> Because it makes math too easy for students?
> > Here is a hint: Assume I give you an infinite sequence
> > a1, a2, a3, ... and I ask you is there some aj < 0. Lets
> > say this question is A.
> >
> > You can answer A if you find an index j with aj < 0. A
> > procedure for that would be to inspect one after the
> > other a1, a2, a3, ... until you find aj < 0.
> >
> > What is the procedure to answer ~A ?
> I am not aware of any such general procedure.
>
> Dan

This is funny: DISPUTATION between "Class" and "Int"

CLASS. How do you do, Mr. Int? Did you not flee
the town on this fine summer day?
INT. I had some ideas and worked them out at the library.
CLASS. Industrious bee! How are you getting along?
INT. Quite weil. Shall we have a drink?
CLASS. Thank you. I bet you worked on that hobby
of yours, rejection of the excluded middle, and the rest.
I never understood why logic should be reliable everywhere
else, but not in mathematics.

INTUITIONISM - AN INTRODUCTION - A. HEYTING
http://www.sciacchitano.it/Tempo/Intuizionismo/Heyting%20Intuizionism.pdf

Mostowski Collapse schrieb am Sonntag, 25. Dezember 2022 um 21:20:25 UTC+11:
> Can you make an example? What do you mean by "it"
> and what you you mean by "easy" when you write "Because
> it makes math too easy for students?"?
>
> Isn't your 2nd statement "I am not aware of any such
> general procedure." evidence that nothing is easy, that
> there is some difficulty somewhere?
>
> Whats wrong with you?
>
> Don't they have libraries where you can rent books at the place
> you live? I guess there are at least 10 books that explain the
> subset intuitionstic logic of classical logic,
>
> other names for the subset are constructive mathematic, there
> is a close relationship. Get an eduction sick boy.
> Dan Christensen schrieb am Sonntag, 25. Dezember 2022 um 15:31:24 UTC+11:
> > On Saturday, December 24, 2022 at 8:37:20 PM UTC-5, Mostowski Collapse wrote:
> > > So Dan Christensen is absolutely clueless why
> > > A v ~A, the law of excluded middle, is so problematic
> > > in constructive mathematics.
> > >
> > Because it makes math too easy for students?
> > > Here is a hint: Assume I give you an infinite sequence
> > > a1, a2, a3, ... and I ask you is there some aj < 0. Lets
> > > say this question is A.
> > >
> > > You can answer A if you find an index j with aj < 0. A
> > > procedure for that would be to inspect one after the
> > > other a1, a2, a3, ... until you find aj < 0.
> > >
> > > What is the procedure to answer ~A ?
> > I am not aware of any such general procedure.
> >
> > Dan

On Sunday, December 25, 2022 at 5:20:25 AM UTC-5, Mostowski Collapse (Jan Burse) wrote:

> Dan Christensen schrieb am Sonntag, 25. Dezember 2022 um 15:31:24 UTC+11:
> > On Saturday, December 24, 2022 at 8:37:20 PM UTC-5, Mostowski Collapse wrote:
> > > So Dan Christensen is absolutely clueless why
> > > A v ~A, the law of excluded middle, is so problematic
> > > in constructive mathematics.
> > >

> > Because it makes math too easy for students?

[snip]

> Can you make an example? What do you mean by "it"
> and what you you mean by "easy" when you write "Because
> it makes math too easy for students?"?
>
[snip]

I was being a bit facetious. Get a life, Jan Burse.

If, as you seem to be suggesting, users want a real challenge (doing math with "one arm tied behind their back"), they can forego the use of one or more options on the Logic Menu in DC Proof. Not some something that, I think, would interest most of my intended audience--those learning the basic methods of mathematical proof. They probably think math is challenging enough without any such seemingly bizarre, self-imposed restrictions.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

One more deficiency, counterfactuals are out of reach for DC Proof!

Sheldon & Amy's Game Counter-Factuals
https://www.youtube.com/watch?v=0lpY0Kt4bn8

Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 10:15:39 UTC+1:
> DC Proof creator Dan-O-Matik suffers from some major
> didactic deficiencies:

Challenge translate this Tic Tac Toe Game Search
from Prolog back to First Order Logic (FOL):

best(X, P, Y) :-
move(X, P, Y),
(win(Y, P) -> true;
other(P, Q),
\+ tie(Y, Q),
\+ best(Y, Q, _)).

Mostowski Collapse schrieb am Montag, 30. Januar 2023 um 09:22:37 UTC+1:
> One more deficiency, counterfactuals are out of reach for DC Proof!
>
> Sheldon & Amy's Game Counter-Factuals
> https://www.youtube.com/watch?v=0lpY0Kt4bn8
>
> Mostowski Collapse schrieb am Donnerstag, 25. November 2021 um 10:15:39 UTC+1:
> > DC Proof creator Dan-O-Matik suffers from some major
> > didactic deficiencies:

On Monday, January 30, 2023 at 3:22:37 AM UTC-5, Mostowski Collapse wrote:
> One more deficiency, counterfactuals are out of reach for DC Proof!
>

It is true that DC Proof doesn't do very well with what might have been if unicorns had actually existed. I will leave such weighty questions to Mr. Collapse and company.

Dan

Dan Christensen wrote:
> In my development, I start with a thought experiment to develop
the notion of a Dedekind FINITE set. It avoids a lot of the supernatural
silliness of Hilbert's Hotel.

Hell No! A thought experiment. Please stick to Historical Facts,
and not some Mathematical Fiction. Similarly I recommend retracting
the induction axiom schema from your Peano Axioms. It cannot be

that we form theorems like:

n + m = m + n

In the light of dark numbers. This is surely humbug predicting
the future of ones calculation, this way, that is impossibru!

Dan Christensen schrieb am Montag, 30. Januar 2023 um 16:54:19 UTC+1:
> On Monday, January 30, 2023 at 3:22:37 AM UTC-5, Mostowski Collapse wrote:
> > One more deficiency, counterfactuals are out of reach for DC Proof!
> >
> It is true that DC Proof doesn't do very well with what might have been if unicorns had actually existed. I will leave such weighty questions to Mr. Collapse and company.
>
> Dan

And could you solve the riddle why counterfactual conditional
differs from material implication? Not only they are different
names, they also refer to different inference rules.

One inference rule found in strict implication when modelling
A > B as the modal formula [](A => B), is the rule of necessity:

|- C
--------
|- []C

Lets say this is the only inference rule for our counterfactual
conditional. I guess its evident that A > ( ~A > B) isn't provable,

isn't it? Usually Provability logics based on modal operator,
have one more axiom, but this additional axiom will also

not allow derivation of A > ( ~A > B) right?

See also:

Basic Concepts in Modal Logic - Edward N. Zalta
https://www.cs.brandeis.edu/~cs112/cs112-2004/newReadings/ConceptsModalLogic.pdf

Wiki Article - Provability logic
https://en.wikipedia.org/wiki/Provability_logic

This author suggests some Prolog code for modal
logic propositional theorem prover:

6 A Modal Calculus for K
leanTAP Revisited - Melvin Fitting, 1997
http://melvinfitting.org/bookspapers/pdf/papers/LeanTaP.pdf

Could try to provide a theorem prover with A => B and
A > B, and model A > B by [](A => B).

Could be fun!

Mostowski Collapse schrieb am Mittwoch, 1. Februar 2023 um 01:56:58 UTC+1:
> And could you solve the riddle why counterfactual conditional
> differs from material implication? Not only they are different
> names, they also refer to different inference rules.
>
> One inference rule found in strict implication when modelling
> A > B as the modal formula [](A => B), is the rule of necessity:
>
> |- C
> --------
> |- []C
>
> Lets say this is the only inference rule for our counterfactual
> conditional. I guess its evident that A > ( ~A > B) isn't provable,
>
> isn't it? Usually Provability logics based on modal operator,
> have one more axiom, but this additional axiom will also
>
> not allow derivation of A > ( ~A > B) right?
>
> See also:
>
> Basic Concepts in Modal Logic - Edward N. Zalta
> https://www.cs.brandeis.edu/~cs112/cs112-2004/newReadings/ConceptsModalLogic.pdf
>
> Wiki Article - Provability logic
> https://en.wikipedia.org/wiki/Provability_logic

See my reply just now to your identical posting at sci.logic

Dan

On Tuesday, January 31, 2023 at 7:56:58 PM UTC-5, Mostowski Collapse wrote:
> And could you solve the riddle why counterfactual conditional
> differs from material implication? Not only they are different
> names, they also refer to different inference rules.
>
[snip]