"Without loss of generality" may not be formalizable

[Dan Christensen]

What is meant by "without loss of generality" in a mathematical proof?

"In giving a mathematical proof, if we say that 'without loss of generality' we may assume that some condition X holds, this means that if we can establish the result in the case where X holds, we can deduce from this that it holds in general. After saying this, one usually assumes that X holds for the rest of the proof. [...]

"Of course, whether it is 'clear' that knowing a result in one case implies that it is true in other cases depends on the situation, and on the mathematical background of one's readership."
--George Bergman
https://math.berkeley.edu/~gbergman/ug.hndts/sets_etc,t=1.pdf

Here I formally prove the following theorem from Wikipedia:

"If three objects are each painted either red or blue, then there must be at least two objects of the same color."

Wikipeda provides the following INFORMAL proof:

"A proof: Assume, without loss of generality, that the first object is red. If either of the other two objects is red, then we are finished; if not, then the other two objects must both be blue and we are still finished."

https://en.wikipedia.org/wiki/Without_loss_of_generality#Example

Formally, I prove (link below):

EXIST(a):EXIST(b):[a e s & b e s & [~a=b & color(a)=color(b)]]

Where

s = a set of 3 distinct elements: {x, y, z}

colors = a set of 2 distinct elements: {red, blue}

color(n) = the color of object n

I have been unable to formally justify the without-loss-of-generality claim. Instead, I first prove the case of the first object being red (lines 33-64), then, the case of it being blue (lines 65-96). The two sub-proofs are only superficially alike (both are 31 lines).

It seems unlikely that the without-loss-of-generality claim can be justified using the ordinary rules of logic found in most math textbooks as has been used here.

https://www.dcproof.com/WithoutLossOfGenerality.htm

Dan

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

[Jeffrey Rubard]

"This is a hoax, right?"

[Mostowski Collapse]

Why sets?

"If three objects are each painted either red or blue,
then there must be at least two objects of the same color."

Make P(x) = "x is red", make ~P(x) = "x is blue".

Then it says:

(P(x) & P(y) & P(z)) v (~P(x) & ~P(y) & ~P(z)) =>
(P(x) & P(y)) v (~P(x) & ~P(x)) v
(P(y) & P(z)) v (~P(y) & ~P(z)) v
(P(x) & P(z)) v (~P(x) & ~P(z)).

Proof by cases P(x) | ~P(x), but the case ~P(x) is symmetric,
need not really be proved. Just replace P(x) by ~P(x).

[Mostowski Collapse]

Yeah, this is not some "without loss" heuristic applied,
you proof two theorems, and then join them:

96 [color(x)=red
=> EXIST(a):EXIST(b):[a e s & b e s & [~a=b & color(a)=color(b)]]]
& [color(x)=blue
=> EXIST(a):EXIST(b):[a e s & b e s & [~a=b & color(a)=color(b)]]]
Join, 63, 95
https://www.dcproof.com/WithoutLossOfGenerality.htm

The proof SUB-PROOF 1 and the proof SUB-PROOF 2 are
the same proof twice. If you need to prove:

a v b -> c

And if thee is a Galois connection (F,G), such that
F(a)<->b and G(c)<->c, its enought to prove:
https://en.wikipedia.org/wiki/Galois_connection

a -> c

LoL

Proof: a -> c, is the same as a -> c, since G(c) <-> c.
Therefore we have also a proof a -> G(c). Now by
definition of Galois connection, there is also a proof

F(a) -> c, but we have F(a) <-> b, so there is a proof
b -> c, and now we can use v introduction rule:

a -> c
b -> c
----------------- (v-Intro)
a v b -> c

[Mostowski Collapse]

Because a Galois connection goes both ways,
back and forth, you could also start with:

b -> c

Giving it the arbitraryness feeling of the choice in the
"without loss" heuristic. But you need to proof the
Galois connection as well. And historically Galois
connection was rather used to establish a connection

between quite different objects, so F(c) <-> c is not
the usual usecase for Galois connection.
https://en.wikipedia.org/wiki/Fundamental_theorem_of_Galois_theory

[Dan Christensen]

On Wednesday, November 23, 2022 at 6:39:44 AM UTC-5, Mostowski Collapse wrote:
> Why sets?
> "If three objects are each painted either red or blue,
> then there must be at least two objects of the same color."
> Make P(x) = "x is red", make ~P(x) = "x is blue".
>
> Then it says:
>
> (P(x) & P(y) & P(z)) v (~P(x) & ~P(y) & ~P(z)) =>
> (P(x) & P(y)) v (~P(x) & ~P(x)) v
> (P(y) & P(z)) v (~P(y) & ~P(z)) v
> (P(x) & P(z)) v (~P(x) & ~P(z)).
>
> Proof by cases P(x) | ~P(x), but the case ~P(x) is symmetric,
> need not really be proved. Just replace P(x) by ~P(x).

[snip]

It may be "intuitively obvious" in an informal proof, but in formal proofs, there is no "intuitively obvious." Every statement must be either be an axiom or derived from such using a fixed list of rules of inference. In this case, it seemed to me that it is easier and quicker to simply handle each case separately. Maybe I gave up too quickly, but if you can formally prove the "symmetry" in this case using only the given rules of inference, please do so, Jan Burse. I won't hold my breath.

[Mostowski Collapse]

See Galois connection. To make it explicit.

[Mostowski Collapse]

But you need a fixpoint:

G(c) <-> c

[Ross A. Finlayson]

Why sets?

It's any theory with only one kind of element and only one relation.

It's called "fundamental".

The effort to establish theory in it called "pure mathematics" is quite underway.

[Ross A. Finlayson]

How about v <-> V\v ?

[Mostowski Collapse]

Ha Ha, Rossy Boy, whats up with Foundation?
Need a new foundation? Category Theorists would

not agree about sets, they like to play with arrows:

ADJOINTNESS IN FOUNDATIONS
F. WILLIAM LAWVERE
http://www.tac.mta.ca/tac/reprints/articles/16/tr16.pdf

[Mostowski Collapse]

Every Galois connection is an idempotent adjunction
https://ncatlab.org/nlab/show/idempotent+adjunction

[Ross A. Finlayson]

That's there's "Kunen consistency in a theory with a universe, and also V=L, Feferman".

The arrow functor, is about the theory of functions in category theory.

It's a big boy now.

[Dan Christensen]

See my reply just now to your similar posting at sci.math.

Dan

[Ross A. Finlayson]

No.

[Mostowski Collapse]

Thats rather easy, the Galois connection is a permutation, of the colors.
The only non-identity permutation of two colors is swapping them.

So lets write the desired theorem with the colors as additional
parameters, namely:

C(red, blue,x,y,z) <=> ((x=red & y=red & z=red) v (x=blue & y=blue & z=blue)
=> ((x=red & y=red) v (x=blue & y=blue) v
(y=red & z=red) v (y=blue & z=blue) v
(x=red & z=red) v (x=blue & z=blue)))

Now you prove:

ALL(red):ALL(blue):(x=red => C(red,blue,x,y,z))
ALL(red):ALL(blue):(C(red,blue,x,y,z) => C(blue,red,x,y,z))

Then you can conclude:

ALL(red):ALL(blue):(x=blue => C(red,blue))

Here my claim verified by Wolfgang Schwartz tool:

(∀r∀b(x=r → Crbxyz) ∧ ∀r∀b(Crbxyz → Cbrxyz)) → ∀r∀b(x=b → Crbxyz) is valid.
https://www.umsu.de/trees/#~6r~6b%28x=r~5C%28r,b,x,y,z%29%29~1~6r~6b%28C%28r,b,x,y,z%29~5C%28b,r,x,y,z%29%29~5~6r~6b%28x=b~5C%28r,b,x,y,z%29%29

[Mostowski Collapse]

Credits for using this Galois Connection go to:

Dudley Brooks schrieb am Dienstag, 22. November 2022 um 22:25:43 UTC+1:
> [...] It has to do with the rules of logic pertaining to
> the naming of variables. In a nutshell, the name of a variable is
> arbitrary, and can be changed at will, as long as it is done
> consistently throughout the entire proof and is not the same as the name
> of some other variable in the proof. (IIRC, that's a corollary of a
> theorem in Proof Theory, about substitution.) [...]
> Dudley Brooks, Artistic Director
https://groups.google.com/g/sci.math/c/S-AyjY4rK7s/m/nw6dfej-BQAJ

Lets make the Galois Connection (F,G) transparent. If
we swap red and blue, then lets says that is the F functor.
The G functor is the same functor again, since swapping

is its own inverse permutation. Now first verify the
fixpoint, G(c) <-> c, we assume that we can show:

ALL(red):ALL(blue):(C(red,blue,x,y,z) => C(blue,red,x,y,z))

From it, it follows:

ALL(red):ALL(blue):(C(blue,red,x,y,z) => C(red,blue,x,y,z))

Verifiable with Wolfgang Schwartz tool:

∀r∀b(Crbxyz → Cbrxyz) → ∀r∀b(Cbrxyz → Crbxyz) is valid.
https://www.umsu.de/trees/#~6r~6b%28C%28r,b,x,y,z%29~5C%28b,r,x,y,z%29%29~5~6r~6b%28C%28b,r,x,y,z%29~5C%28r,b,x,y,z%29%29

So that we have indeed:

ALL(red):ALL(blue):(C(blue,red,x,y,z) <=> C(red,blue,x,y,z))

The rest is also as in the Galois Connection criterias,
namely F(a) <-> b. We did already F(a) -> b, using c -> G(c),
now that we also have G(c) -> c, we will be able to show b -> F(a).

Whats a little messy here the quantifiers are sometimes
outside of -> and sometimes inside the arguments of ->.
But don't worry, we can show:

∀r∀bC(r,b,x,y,z) → ∀r∀b(C(r,b,x,y,z) → C(b,r,x,y,z))
https://www.umsu.de/trees/#~6r~6bC%28r,b,x,y,z%29~5~6r~6b%28C%28r,b,x,y,z%29~5C%28b,r,x,y,z%29%29

So maybe should rework everything to arrive at a less
sloppy presentation.

Mostowski Collapse schrieb am Mittwoch, 23. November 2022 um 21:32:16 UTC+1:
> Thats rather easy, the Galois connection is a permutation, of the colors.
> The only non-identity permutation of two colors is swapping them.
>
> So lets write the desired theorem with the colors as additional
> parameters, namely:
>
> C(red, blue,x,y,z) <=> ((x=red & y=red & z=red) v (x=blue & y=blue & z=blue)
> => ((x=red & y=red) v (x=blue & y=blue) v
> (y=red & z=red) v (y=blue & z=blue) v
> (x=red & z=red) v (x=blue & z=blue)))
>
> Now you prove:
>
> ALL(red):ALL(blue):(x=red => C(red,blue,x,y,z))
> ALL(red):ALL(blue):(C(red,blue,x,y,z) => C(blue,red,x,y,z))
>
> Then you can conclude:
>

> ALL(red):ALL(blue):(x=blue => C(red,blue,x,y,z))

[Dan Christensen]

On Wednesday, November 23, 2022 at 3:32:16 PM UTC-5, Mostowski Collapse wrote:
> Thats rather easy, the Galois connection is a permutation, of the colors.
> The only non-identity permutation of two colors is swapping them.
>
> So lets write the desired theorem with the colors as additional
> parameters, namely:
>
> C(red, blue,x,y,z) <=> ((x=red & y=red & z=red) v (x=blue & y=blue & z=blue)
> => ((x=red & y=red) v (x=blue & y=blue) v
> (y=red & z=red) v (y=blue & z=blue) v
> (x=red & z=red) v (x=blue & z=blue)))
>
> Now you prove:
>
> ALL(red):ALL(blue):(x=red => C(red,blue,x,y,z))
> ALL(red):ALL(blue):(C(red,blue,x,y,z) => C(blue,red,x,y,z))
>
> Then you can conclude:
>
> ALL(red):ALL(blue):(x=blue => C(red,blue))
>

Hint: What part of FORMAL PROOF don't you understand, Jan Burse. OK let's take one line at at time.

Hint: Your first 63 lines will be the same as mine. Then what? What is your line 64? What about 65 and 66? Get back to us when you have at least that much.

[Mostowski Collapse]

Well we only prove SUB-PROOF 1 , but we don't prove SUB-PROOF 2.
Its a consequence:

Mostowski Collapse schrieb am Mittwoch, 23. November 2022 um 21:30:37 UTC+1:
> Now you prove:
>
> ALL(red):ALL(blue):(x=red => C(red,blue,x,y,z))
> ALL(red):ALL(blue):(C(red,blue,x,y,z) => C(blue,red,x,y,z))
>
> Then you can conclude:
>

> ALL(red):ALL(blue):(x=blue => C(red,blue,x,y,z))
https://groups.google.com/g/sci.math/c/S-AyjY4rK7s/m/P_feO3tKBgAJ

Too hard to understand what WLOG means for Wonky Man?

[Dan Christensen]

On Wednesday, November 23, 2022 at 4:32:50 PM UTC-5, Mostowski Collapse wrote:

> Too hard to understand what WLOG means for Wonky Man?
> Dan Christensen schrieb am Mittwoch, 23. November 2022 um 22:17:42 UTC+1:
> > On Wednesday, November 23, 2022 at 3:32:16 PM UTC-5, Mostowski Collapse wrote:
> > > Thats rather easy, the Galois connection is a permutation, of the colors.
> > > The only non-identity permutation of two colors is swapping them.
> > >
> > > So lets write the desired theorem with the colors as additional
> > > parameters, namely:
> > >
> > > C(red, blue,x,y,z) <=> ((x=red & y=red & z=red) v (x=blue & y=blue & z=blue)
> > > => ((x=red & y=red) v (x=blue & y=blue) v
> > > (y=red & z=red) v (y=blue & z=blue) v
> > > (x=red & z=red) v (x=blue & z=blue)))
> > >
> > > Now you prove:
> > >
> > > ALL(red):ALL(blue):(x=red => C(red,blue,x,y,z))
> > > ALL(red):ALL(blue):(C(red,blue,x,y,z) => C(blue,red,x,y,z))
> > >
> > > Then you can conclude:
> > >
> > > ALL(red):ALL(blue):(x=blue => C(red,blue))
> > >
> > Hint: What part of FORMAL PROOF don't you understand, Jan Burse. OK let's take one line at at time.
> >
> > Hint: Your first 63 lines will be the same as mine. Then what? What is your line 64? What about 65 and 66? Get back to us when you have at least that much.

> Well we only prove SUB-PROOF 1 , but we don't prove SUB-PROOF 2.

So, you have no clue of what to actually do next, Jan Burse. Oh, well...

Dan

[Mostowski Collapse]

But I made an error, I didn't quantify x, so this is better:

∀x∀y∀z∀r∀b(x=r → Crbxyz) →
(∀x∀y∀z∀r∀b(Crbxyz → Cbrxyz) →
∀x∀y∀z∀b∀r(x=b → Cbrxyz)) is valid.
https://www.umsu.de/trees/#~6x~6y~6z~6r~6b%28x=r~5C%28r,b,x,y,z%29%29~5~6x~6y~6z~6r~6b%28C%28r,b,x,y,z%29~5C%28b,r,x,y,z%29%29~5~6x~6y~6z~6b~6r%28x=b~5C%28b,r,x,y,z%29%29

But this is only to illustrate why x=b case is redundant,
when we know something about permutation. We can now prove:

∀x∀y∀z∀r∀b(x=r → Crbxyz) →
(∀x∀y∀z∀r∀b(Crbxyz → Cbrxyz) →
∀x∀y∀z∀b∀r((x=r ∨ x=b) → Crbxyz)) is valid.
https://www.umsu.de/trees/#~6x~6y~6z~6r~6b%28x=r~5C%28r,b,x,y,z%29%29~5~6x~6y~6z~6r~6b%28C%28r,b,x,y,z%29~5C%28b,r,x,y,z%29%29~5~6x~6y~6z~6b~6r%28x=r~2x=b~5C%28r,b,x,y,z%29%29

[Mostowski Collapse]

Corr.: Actually we can formulate the redundancy,
only based on alpha-conversion of bounded quantifers:

∀x∀y∀z∀r∀b(x=r → Crbxyz) → ∀x∀y∀z∀b∀r(x=b → Cbrxyz) is valid.

Now its clear that we need something to connect
Crbxyz and Cbrxyz. But obviously this Crbxyz here:

C(red, blue,x,y,z) <=> ((x=red & y=red & z=red) v (x=blue & y=blue & z=blue)
=> ((x=red & y=red) v (x=blue & y=blue) v
(y=red & z=red) v (y=blue & z=blue) v
(x=red & z=red) v (x=blue & z=blue)))

Has this property:

∀x∀y∀z∀r∀b(Crbxyz → Cbrxyz)

A formal proof might be quite long. We humans on
the other hand somehow see this "obviously" in kind
of a holistic fashion through our visual pattern matching.

Our visual pattern matching seems to be quite
good what concerns commutativity and associativity.

LMAO!

[Mostowski Collapse]

You can also use another reading of "each", like for example:

C2(red, blue,x,y,z) <=> ((x=red v x=blue) & (y=red v y=blue) & (z=red v z=blue)

=> ((x=red & y=red) v (x=blue & y=blue) v
(y=red & z=red) v (y=blue & z=blue) v
(x=red & z=red) v (x=blue & z=blue)))

C2 also "obviously" satisfies:

∀x∀y∀z∀r∀b(Crbxyz → Cbrxyz)

[Dan Christensen]

On Wednesday, November 23, 2022 at 5:36:46 PM UTC-5, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Mittwoch, 23. November 2022 um 23:04:45 UTC+1:

> > A formal proof might be quite long.

[snip]

No kidding! So much for your "formal SHORTCUT," eh, Jan Burse? HA, HA, HA!!!

But the longest proof begins with a single statement. Get busy, Jan Burse! Maybe you can salvage some of your reputation here by finishing it even if it might be 100 lines longer than the original. (Hee, hee!)

Dan

[Mostowski Collapse]

Ha Ha, if we were to ask Dan Christense to prove the
theorem "Every Planar Map is Four-Colorable", and if

we would give him that the colors are:

{red, green, blue, yellow}

He would possibly produce 4! = 24 proofs, depending
how the crayons are layed out on the table, for the

poor hypothetical guy who needs to color all the
infinitely many possible planar graph. LoL

[Mostowski Collapse]

Ok, we will help Wonky Man, to solve his homework.
Here is are two lemmas, towards proving Crbxyz => Cbrxyz:

Lemma 1: Swap "either red or blue"

12 ALL(x):ALL(r):ALL(b):[x=r | x=b => x=b | x=r]
Conclusion, 1

Lemma 2: Swap "two reds or two blues"

12 ALL(x):ALL(r):ALL(y):ALL(b):[x=r & y=r | x=b & y=b => x=b & y=b | x=r & y=r]
Conclusion, 1

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

Lemma 1: Swap "either red or blue"

1 x=r | x=b
Premise

2 ~[x=b | x=r]
Premise

3 ~~[~x=b & ~x=r]
DeMorgan, 2

4 ~x=b & ~x=r
Rem DNeg, 3

5 ~x=b
Split, 4

6 ~x=r
Split, 4

7 ~x=r => x=b
Imply-Or, 1

8 x=b
Detach, 7, 6

9 ~x=b & x=b
Join, 5, 8

10 ~~[x=b | x=r]
Conclusion, 2

11 x=b | x=r
Rem DNeg, 10

12 ALL(x):ALL(r):ALL(b):[x=r | x=b => x=b | x=r]
Conclusion, 1

Lemma 2: Swap "two reds or two blues"

1 x=r & y=r | x=b & y=b
Premise

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

3 ~~[~[x=b & y=b] & ~[x=r & y=r]]
DeMorgan, 2

4 ~[x=b & y=b] & ~[x=r & y=r]
Rem DNeg, 3

5 ~[x=b & y=b]
Split, 4

6 ~[x=r & y=r]
Split, 4

7 ~[x=r & y=r] => x=b & y=b
Imply-Or, 1

8 x=b & y=b
Detach, 7, 6

9 ~[x=b & y=b] & [x=b & y=b]
Join, 5, 8

10 ~~[x=b & y=b | x=r & y=r]
Conclusion, 2

11 x=b & y=b | x=r & y=r
Rem DNeg, 10

12 ALL(x):ALL(r):ALL(y):ALL(b):[x=r & y=r | x=b & y=b => x=b & y=b | x=r & y=r]
Conclusion, 1

[Dan Christensen]

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

Dan

On Thursday, November 24, 2022 at 11:45:03 AM UTC-5, Mostowski Collapse wrote:
> Ok, we will help Wonky Man, to solve his homework.
> Here is are two lemmas, towards proving Crbxyz => Cbrxyz:
>
> Lemma 1: Swap "either red or blue"
>
> 12 ALL(x):ALL(r):ALL(b):[x=r | x=b => x=b | x=r]
> Conclusion, 1
>
> Lemma 2: Swap "two reds or two blues"
>
> 12 ALL(x):ALL(r):ALL(y):ALL(b):[x=r & y=r | x=b & y=b => x=b & y=b | x=r & y=r]
> Conclusion, 1
>

[snip]

[Mostowski Collapse]

See symmetry breaking theorem below. We can now make
some "without loss of generality" reasoning. Now you can prove:

/* Spezialize on red */
ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):(x=r=> C(r,b,x,y,z))

This was already proved:

/* Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues" */
ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):(C(r,b,x,y,z) => C(b,r,x,y,z))

Then you may automatically conclude:

/* Spezialize on blue */
ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):(x=b=> C(r,b,x,y,z))

Yeah, its done! Even with clumsy tool like DC Poop.

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

[Dan Christensen]

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

Dan

On Thursday, November 24, 2022 at 12:52:58 PM UTC-5, Mostowski Collapse wrote:
> See symmetry breaking theorem below. We can now make
> some "without loss of generality" reasoning. Now you can prove:
>
> /* Spezialize on red */
> ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):(x=r=> C(r,b,x,y,z))
>
> This was already proved:
>
> /* Theorem: Swap "3 objects either red or blue" => "2 out of 3 all reds or blues" */
> ALL(x):ALL(y):ALL(y):ALL(r):ALL(b):(C(r,b,x,y,z) => C(b,r,x,y,z))
>

[snip]

[Mostowski Collapse]

No I don't need. Wikipedia says nowhere that there is
a function color. When you have 3 objects, you can
use variables x,y,z for their colors. Just read Wikipedia:

"If three objects are each painted either red or blue, then
there must be at least two objects of the same color."

https://en.wikipedia.org/wiki/Without_loss_of_generality#Example

Whats wrong with you Wonky Man? Did your brain get evacuated?

[Dan Christensen]

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

[Mostowski Collapse]

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!

[Mostowski Collapse]

You will even have more variables if we would do the Pigeonhole principle:

> State of affair is represented as:
> Xij <=> pigeon i is placed in hole j i in 0..n-1, j in 0..m-1
> Clause for each pigeon that it is placed in at least one hole:
> Xi0 v .. v Xim-1 i in 0..n-1
> Clauses for each hole that it carries maximally one pigeon:
> ~Xij v ~Xkj i in 0..n-1, k in i+1..n-1, j in 0..m-1.
> Should work correctly for n>=m.

The outcome for two boxes red and blue, will be basically
that you cannot place 3 pigeons each in its own box.

So we have n=3, m=2. This gives a matrice of 3x2 variables:

X11 X12
X21 X22
X31 X32

And the boolean conditions are:

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

So using a SAT solvere for example from SWI-Prolog we get:

?- use_module(library(clpb)).
true.

?- sat((X11+X12)*
(X21+X22)*
(X31+X32)*
(~X11+ ~X21)*
(~X11+ ~X31)*
(~X21+ ~X31)*
(~X12+ ~X22)*
(~X12+ ~X32)*
(~X22+ ~X32)).
false.

[Mostowski Collapse]

So lets sum up why DC Proof is made of chinesium:

- Failure 1: Wonky Man cannot use his own take
with a color function, to show a WLOG inference.

- Failure 2: Wonky Man is not able to understand
the 3 variables x,y,z solution that shows a WLOG inference.

- Failure 3: Given Failure 1 and Failure 2, I guess
a SAT solver Pigeon principle is also out of reach for Wonky Man.

[Dan Christensen]

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

Dan

On Thursday, November 24, 2022 at 5:15:16 PM UTC-5, Mostowski Collapse wrote:
> So lets sum up why DC Proof is made of chinesium:
>

[snip]

[Mostowski Collapse]

You are a liar, again and again. Of course 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)).

Whats wrong with you? See here:

Mostowski Collapse schrieb am Donnerstag, 24. November 2022 um 21:59:06 UTC+1:
> 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.
https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/IOpQr52aBgAJ

[Dan Christensen]

See my reply just now to your identical posting at sci.math (your homework assignment)

Dan

On Friday, November 25, 2022 at 2:37:18 AM UTC-5, Mostowski Collapse wrote:

[snip childish abuse]

[Mostowski Collapse]

Whats your prolololoblem Wonky Man? Still level 1000 stupid?
Thats your assignment. Moron. Its relatively trivial with x,y,z colors.
so we prove towards ultimately proving: First recall what is

our goal, what we want to prove, call the logical matrice of it by the
name C(r,b,x,y,z), the logical matrice is what is inside the quantifier block:

Theorem: "3 objects either red or blue" => "2 out of 3 all reds or blues"
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]]]

And intermediate step, that you seem to have requested, is to prove a
different logical matrice, namely x=r => C(r,b,x,y,z). Quite trivial:

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

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

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

2 ~~[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]]]
Imply-And, 1

3 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, 2

4 x=r
Split, 3

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]]
Split, 3

6 ~[[r=r | r=b] & [y=r | y=b] & [z=r | z=b] => r=r & y=r | r=b & y=b | [r=r & z=r | r=b & z=b] | [y=r & z=r | y=b & z=b]]
Substitute, 4, 5

7 ~~[[r=r | r=b] & [y=r | y=b] & [z=r | z=b] & ~[r=r & y=r | r=b & y=b | [r=r & z=r | r=b & z=b] | [y=r & z=r | y=b & z=b]]]
Imply-And, 6

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

9 r=r | r=b
Split, 8

10 y=r | y=b
Split, 8

11 z=r | z=b
Split, 8

12 ~[r=r & y=r | r=b & y=b | [r=r & z=r | r=b & z=b] | [y=r & z=r | y=b & z=b]]
Split, 8

13 ~~[~[r=r & y=r | r=b & y=b | [r=r & z=r | r=b & z=b]] & ~[y=r & z=r | y=b & z=b]]
DeMorgan, 12

14 ~[r=r & y=r | r=b & y=b | [r=r & z=r | r=b & z=b]] & ~[y=r & z=r | y=b & z=b]
Rem DNeg, 13

15 ~[r=r & y=r | r=b & y=b | [r=r & z=r | r=b & z=b]]
Split, 14

16 ~[y=r & z=r | y=b & z=b]
Split, 14

17 ~~[~[r=r & y=r | r=b & y=b] & ~[r=r & z=r | r=b & z=b]]
DeMorgan, 15

18 ~[r=r & y=r | r=b & y=b] & ~[r=r & z=r | r=b & z=b]
Rem DNeg, 17

19 ~[r=r & y=r | r=b & y=b]
Split, 18

20 ~[r=r & z=r | r=b & z=b]
Split, 18

21 y=r
Premise

22 ~[r=r & r=r | r=b & r=b]
Substitute, 21, 19

23 r=r
Reflex

24 r=r & r=r
Join, 23, 23

25 r=r & r=r | r=b & r=b
Arb Or, 24

26 ~[r=r & r=r | r=b & r=b] & [r=r & r=r | r=b & r=b]
Join, 22, 25

27 ~y=r
Conclusion, 21

28 ~y=r => y=b
Imply-Or, 10

29 y=b
Detach, 28, 27

30 z=r
Premise

31 ~[r=r & r=r | r=b & r=b]
Substitute, 30, 20

32 r=r
Reflex

33 r=r & r=r
Join, 32, 32

34 r=r & r=r | r=b & r=b
Arb Or, 33

35 ~[r=r & r=r | r=b & r=b] & [r=r & r=r | r=b & r=b]
Join, 31, 34

36 ~z=r
Conclusion, 30

37 ~z=r => z=b
Imply-Or, 11

38 z=b
Detach, 37, 36

39 y=b & z=b
Join, 29, 38

40 y=r & z=r | y=b & z=b
Arb Or, 39

41 ~[y=r & z=r | y=b & z=b] & [y=r & z=r | y=b & z=b]
Join, 16, 40

42 ~EXIST(x):EXIST(r):EXIST(b):EXIST(y):EXIST(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]]]
Conclusion, 1

43 ~~ALL(x):~EXIST(r):EXIST(b):EXIST(y):EXIST(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]]]
Quant, 42

44 ALL(x):~EXIST(r):EXIST(b):EXIST(y):EXIST(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, 43

45 ALL(x):~~ALL(r):~EXIST(b):EXIST(y):EXIST(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]]]
Quant, 44

46 ALL(x):ALL(r):~EXIST(b):EXIST(y):EXIST(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, 45

47 ALL(x):ALL(r):~~ALL(b):~EXIST(y):EXIST(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]]]
Quant, 46

48 ALL(x):ALL(r):ALL(b):~EXIST(y):EXIST(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, 47

49 ALL(x):ALL(r):ALL(b):~~ALL(y):~EXIST(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]]]
Quant, 48

50 ALL(x):ALL(r):ALL(b):ALL(y):~EXIST(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, 49

51 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]]]
Quant, 50

52 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, 51

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

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

[Mostowski Collapse]

Still clueless? One more hint:

It is shown here in this thread how its done:

> 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)]
https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/gWDsq2DABgAJ

Now if you can prove the theorem without using x=red and x=blue
essentially same proof twice, then you can also prove
EXIST(p):EXIST(q):[~p=q => color(p)=color(q)] without using
essentially same proof twice.

Or do you disagree on this observation?

[Dan Christensen]

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

[Mostowski Collapse]

Yeah, you missed it. I have completed the proof. See here:

Mostowski Collapse schrieb am Samstag, 26. November 2022 um 16:50:16 UTC+1:
> 117 EXIST(p):EXIST(q):[~p=q => color(p)=color(q)]
> Rem DNeg, 116
https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/skDAmuwmBwAJ

The last step is to show that, from these already proved two theorems:

> Theorem "Specialization to r"

> 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

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

We can deduce:

Theorem "Specialization to b"
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]]]

This is left as an exercise. It would then follow what
is used in the first proof.

[Mostowski Collapse]

Error 404, argument not found.
Why can WLOG not be formalized?

Dan Christensen schrieb am Montag, 21. November 2022 um 21:18:40 UTC+1:
> What is meant by "without loss of generality" in a mathematical proof?
>
> "In giving a mathematical proof, if we say that 'without loss of generality' we may assume that some condition X holds, this means that if we can establish the result in the case where X holds, we can deduce from this that it holds in general. After saying this, one usually assumes that X holds for the rest of the proof. [...]
>
> "Of course, whether it is 'clear' that knowing a result in one case implies that it is true in other cases depends on the situation, and on the mathematical background of one's readership."
> --George Bergman
> https://math.berkeley.edu/~gbergman/ug.hndts/sets_etc,t=1.pdf
>
> Here I formally prove the following theorem from Wikipedia:

>
> "If three objects are each painted either red or blue, then there must be at least two objects of the same color."
>

> Wikipeda provides the following INFORMAL proof:
>
> "A proof: Assume, without loss of generality, that the first object is red. If either of the other two objects is red, then we are finished; if not, then the other two objects must both be blue and we are still finished."
>
> https://en.wikipedia.org/wiki/Without_loss_of_generality#Example
>
> Formally, I prove (link below):
>
> EXIST(a):EXIST(b):[a e s & b e s & [~a=b & color(a)=color(b)]]
>
> Where
>
> s = a set of 3 distinct elements: {x, y, z}
>
> colors = a set of 2 distinct elements: {red, blue}
>
> color(n) = the color of object n
>
> I have been unable to formally justify the without-loss-of-generality claim. Instead, I first prove the case of the first object being red (lines 33-64), then, the case of it being blue (lines 65-96). The two sub-proofs are only superficially alike (both are 31 lines).
>
> It seems unlikely that the without-loss-of-generality claim can be justified using the ordinary rules of logic found in most math textbooks as has been used here.
>
> https://www.dcproof.com/WithoutLossOfGenerality.htm

[Dan Christensen]

On Tuesday, November 29, 2022 at 1:33:59 PM UTC-5, Mostowski Collapse wrote:
> Error 404, argument not found.
> Why can WLOG not be formalized?
>

It can certainly be formalized in some special cases. AFAICT there is no general theory of when WLOG proofs are applicable or not. Perhaps you can develop such a theory, Jan Burse?

Dan

[Mostowski Collapse]

STUDENTS BEWARE: Don't be a victim of Dan Christensen 's fake math and science.
Wonky Man is currently up to some new breakthrough incompleteness.

This will be the next big event after Gödels arithmetic incompletness theorems,
the WLOG incompletness theorem by Wonky Man.

[Mostowski Collapse]

You could equally well claim Q.E.D. isn't formalizable.

Latin phrase quod erat demonstrandum,
https://en.wikipedia.org/wiki/Q.E.D.

Because like WLOG, it involves too much informal reasoning.
Here is an example, which you might also have a hard time
to replicate in DC Proof. Is it therefore not formalizable?

Here is an example:

COROLLARY 1.30
PROOF. Obvious from (1.27) and (1.29). ✷
https://www.jmilne.org/math/CourseNotes/AG.pdf

✷ = Q.E.D.

Dan Christensen schrieb am Mittwoch, 30. November 2022 um 03:37:34 UTC+1:

[Mostowski Collapse]

But reading John Harrison is surely a good idea. Only DC
Proof can hardly be compared to what John Harrison uses.
Because he is usally working with:
- He isn't shy to use higher order logic from time to time
- He isn't shy to use tactics from time to time

So unless you want to add these features to DC Proof, you
will possibly not be able to replicate most of his examples.
For example his theorem here:

(* ------------------------------------------------------------------------- *)
(* A generic "without loss of generality" lemma for symmetry. *)
(* ------------------------------------------------------------------------- *)

let WLOG_RELATION = prove
(`!R P. (!x y. P x y ==> P y x) /\
(!x y. R x y \/ R y x) /\
(!x y. R x y ==> P x y)
==> !x y. P x y`,
REPEAT GEN_TAC THEN DISCH_THEN
(CONJUNCTS_THEN2 ASSUME_TAC (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
STRIP_TAC THEN ASM_SIMP_TAC[]);;
https://github.com/jrh13/hol-light/blob/master/theorems.ml

Quantifies over R and P, that is it quantifies over predicate
symbols, how would you do that in DC Proof?

[Mostowski Collapse]

The tactics of Wolfgang Schwartz tree tool prove
it in a blink. Only Wolfgang Schwartz tree tool cannot
quantify predicates either, so its only this theorem:

(∀x∀y(Pxy → Pyx) ∧ (∀x∀y(Rxy ∨ Ryx) ∧ ∀x∀y(Rxy → Pxy))) → ∀x∀yPxy is valid.
https://www.umsu.de/trees/#~6x~6y(Pxy~5Pyx)~1(~6x~6y(Rxy~2Ryx))~1(~6x~6y(Rxy~5Pxy))~5~6x~6yPxy

If you can quantify predicates you can use a theorem
as a template for other theorems. It becomes more
generic. It can be instantiated by other predicates or

formulae. Thats why I intially asked "Why Sets?". Because
John Harrison, especially from his HOL Light background,
is more used in using higher order stuff, and predicates

is one of the rather easy higher order stuff. They usually
have only the type i -> o or in the present example you
can view them having the type i x i -> o, or even polymorphic

most likely, type A x A -> o, where A is some type.

[Mild Shock]

I guess the generalized drinker paradox thus uses extraordinary logic.

[Mild Shock]

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)]]

[Mild Shock]

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".