FOL would be useless if it wouldn't have any scepticism
built-in. But since starting with:

ALL(a):[P(a)=>Q(a)]

It doesn't derive always automatically:

EXIST(a):[P(a)&Q(a)]

It does exactly the same with DC Proof. Plus it does
a little bit more. You can prove more things in FOL, than
you can prove DC Proof. For example you can prove in FOL:

P, ~EXIST(x):x=x |- Q
P, ~EXIST(x):x=x |- ~Q

And show that P, ~EXIST(x):x=x is inconsistent,
i.e. has no domain of discourse, with non-empty
domain, that would satisfy ths formula.

You cannot show the same with DC Proof.

Mostowski Collapse schrieb am Freitag, 4. November 2022 um 00:36:37 UTC+1:
> Why? You still didn't give a reason why it is useless.
> FOL has all the scepticism you want built. You say
> yourself ALL(a):P(a) is uncommon.
>
> Only your beloved ALL(a):[P(a)=>Q(a)] is used.
> Try deriving EXIST(a):[P(a)&Q(a)]. Can you
> derive it in FOL?
> Dan Christensen schrieb am Donnerstag, 3. November 2022 um 23:40:46 UTC+1:
> > On Thursday, November 3, 2022 at 6:02:45 PM UTC-4, Mostowski Collapse wrote:
> > > Because FOL is already careful enough, nobody needs
> > > DC Proof.
> > A system from which you can derive ALL(a):P(a) => EXIST(a):P(a) would be quite useless for learning the methods of mathematical proof. It might a nice little toy system for philosophy or theology classes, but students should be told it may not work in real life.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

In general FOL is more powerful than DC Proof:

- It can show many theorems which DC Proof cannot show
- This can be used to show inconsistencies where DC Proof fails to show the same
- Nevertheless it has the same Scepticism built-in when Range Restricted formulas are used
- It doesn't have substitution anomalies
- The interpolation theorem holds
- What else?

I would say FOL is the perfect tool for a sane person.
On the otherhand we are still waiting for a proof of Zorns
Lemma in DC Proof. We are waiting, waiting, waiting, ...

Mostowski Collapse schrieb am Freitag, 4. November 2022 um 00:41:42 UTC+1:
> FOL would be useless if it wouldn't have any scepticism
> built-in. But since starting with:
>
> ALL(a):[P(a)=>Q(a)]
>
> It doesn't derive always automatically:
>
> EXIST(a):[P(a)&Q(a)]
>
> It does exactly the same with DC Proof. Plus it does
> a little bit more. You can prove more things in FOL, than
> you can prove DC Proof. For example you can prove in FOL:
>
> P, ~EXIST(x):x=x |- Q
> P, ~EXIST(x):x=x |- ~Q
>
> And show that P, ~EXIST(x):x=x is inconsistent,
> i.e. has no domain of discourse, with non-empty
> domain, that would satisfy ths formula.
>
> You cannot show the same with DC Proof.
> Mostowski Collapse schrieb am Freitag, 4. November 2022 um 00:36:37 UTC+1:
> > Why? You still didn't give a reason why it is useless.
> > FOL has all the scepticism you want built. You say
> > yourself ALL(a):P(a) is uncommon.
> >
> > Only your beloved ALL(a):[P(a)=>Q(a)] is used.
> > Try deriving EXIST(a):[P(a)&Q(a)]. Can you
> > derive it in FOL?
> > Dan Christensen schrieb am Donnerstag, 3. November 2022 um 23:40:46 UTC+1:
> > > On Thursday, November 3, 2022 at 6:02:45 PM UTC-4, Mostowski Collapse wrote:
> > > > Because FOL is already careful enough, nobody needs
> > > > DC Proof.
> > > A system from which you can derive ALL(a):P(a) => EXIST(a):P(a) would be quite useless for learning the methods of mathematical proof. It might a nice little toy system for philosophy or theology classes, but students should be told it may not work in real life.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, November 3, 2022 at 7:36:37 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 3. November 2022 um 23:40:46 UTC+1:
> > On Thursday, November 3, 2022 at 6:02:45 PM UTC-4, Mostowski Collapse wrote:
> > > Because FOL is already careful enough, nobody needs
> > > DC Proof.
> > A system from which you can derive ALL(a):P(a) => EXIST(a):P(a) would be quite useless for learning the methods of mathematical proof. It might a nice little toy system for philosophy or theology classes, but students should be told it may not work in real life.

> Why? You still didn't give a reason why it is useless.

Have done so.

> FOL has all the scepticism you want built. You say
> yourself ALL(a):P(a) is uncommon.
>

You should either have to formally prove or assume the existence of some object.

> Only your beloved ALL(a):[P(a)=>Q(a)] is used.
> Try deriving EXIST(a):[P(a)&Q(a)].

Not possible in DC Proof (or, generally speaking, in mathematics) without first explicitly proving or assuming EXIST(a):P(a).

Dan

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

The cringe thing, his DC Proof is still full of bugs. We
are now at version dcpsetup19.exe. I guess there
is soon a new version. Not sure, can this unallowed

substitiution bug be used to derive an inconsistency?
Maybe he better make it open source on Git, maybe
some poor souls could review the code or contribute

fixes. Maybe his other mathematicians could help
him, if they are not imaginary?

Dan Christensen schrieb am Freitag, 4. November 2022 um 01:38:34 UTC+1:
> On Thursday, November 3, 2022 at 7:36:37 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Donnerstag, 3. November 2022 um 23:40:46 UTC+1:
> > > On Thursday, November 3, 2022 at 6:02:45 PM UTC-4, Mostowski Collapse wrote:
> > > > Because FOL is already careful enough, nobody needs
> > > > DC Proof.
> > > A system from which you can derive ALL(a):P(a) => EXIST(a):P(a) would be quite useless for learning the methods of mathematical proof. It might a nice little toy system for philosophy or theology classes, but students should be told it may not work in real life.
> > Why? You still didn't give a reason why it is useless.
> Have done so.
> > FOL has all the scepticism you want built. You say
> > yourself ALL(a):P(a) is uncommon.
> >
> You should either have to formally prove or assume the existence of some object.
> > Only your beloved ALL(a):[P(a)=>Q(a)] is used.
> > Try deriving EXIST(a):[P(a)&Q(a)].
> Not possible in DC Proof (or, generally speaking, in mathematics) without first explicitly proving or assuming EXIST(a):P(a).
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, November 5, 2022 at 5:08:33 PM UTC-4, Mostowski Collapse wrote:
> The cringe thing, his DC Proof is still full of bugs.

There are no known bugs in DC Proof that would lead to an incorrect proof.

> We
> are now at version dcpsetup19.exe. I guess there
> is soon a new version. Not sure, can this unallowed
>
> substitiution bug be used to derive an inconsistency?

It is up to users must make consistent use of variable names. As it suggests on the Premise and Axiom screens, "Letters a-j should be used for bound variables." That suggestion can, of course, be ignored (as you did, Jan Burse), but then extra care must then be taken by the user (which you didn't).

Dan

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

On Sunday, November 6, 2022 at 5:54:37 AM UTC+1, Dan Christensen wrote:
> On Saturday, November 5, 2022 at 5:08:33 PM UTC-4, Mostowski Collapse wrote:
>
> There are no known bugs in DC Proof that would lead to an incorrect proof..

Looks as if there is at least one such bug.

> > We are now at version dcpsetup19.exe. I guess there
> > is soon a new version. Not sure, can this unallowed
> > substitiution bug be used to derive an inconsistency?

Guess have found one (in the context of arithmetic, say).

> It is up to users must make consistent use of variable names.

Nonsense. A system like DC Spoof has to enforce the usage of variables in a way such that no inconsistencies can arise _just from using variables in an "inappropriate" way_. There are (substitiution) RULES for that, dumbo. They are usually part of the/a "formal system" (if it allows for substitution at all).

Hence

> extra care must [...] be taken by

your system, you silly idiot!

This could be tricky to model in Wolfgang Schwarz tree tool,
namely that these two are the same in FOL and DC Proof:

ALL(x):[P(x) => ...]

P(x) => ...

Provided P(x) is such that it is false in an empty domain model.

Lets first allow an empty domain, DC Proof, Ux can be empty,
since we also require ∀x(Px → Ux), P(x) will be false when
Ux is empty as required, so we get this kind of modelling:

∀x(Px → Ux) → (∀x(Ux → (Px → Qx)) ↔ ∀x(Px → Qx)) is valid.
https://www.umsu.de/trees/#%28~6x%28Px~5Ux%29%29~5%28~6x%28Ux~5%28Px~5Qx%29%29~4~6x%28Px~5Qx%29%29

Now lets try FOL, obviously still valid, its only a weakening by ∃xUx:

∃xUx → (∀x(Px → Ux) → (∀x(Ux → (Px → Qx)) ↔ ∀x(Px → Qx))) is valid.
https://www.umsu.de/trees/#~7xUx~5%28~6x%28Px~5Ux%29%29~5%28~6x%28Ux~5%28Px~5Qx%29%29~4~6x%28Px~5Qx%29%29

How interesting is the case of an empty domain? Not very intersting
anyway, provide P(x) is such that it is false in an empty domain model:

¬∃xUx → (∀x(Px → Ux) → (∀x(Ux → (Px → Qx)) ↔ (R∨¬R))) is valid.
https://www.umsu.de/trees/#~3~7xUx~5~6x%28Px~5Ux%29~5%28~6x%28Ux~5%28Px~5Qx%29%29~4R~2~3R%29

What would be an example of an interesting case, hopefully documented
somewhere in the literature, where ¬∃xUx leads to something else

than the triviality R∨¬R, i.e. always true?

DC Proof tried to solve this here:

> - Predicates and set are not the same
> - Function symbols and sets of pairs are not same

By a balancing act, through his function axiom.
Unfortunately the result is not very convincing. Where
as for two function graphs f and g we have:

~f=g => ~dom(f)=dom(g) v EXIST(x):[x e dom(f) & ~f(x)=g(x)]

The corresponding functions f' and g', that come out of
Dan Christensens function axiom, do not satisfy anymore:

~f'=g' => ~dom(f')=dom(g') v EXIST(x):[x e dom(f') & ~f'(x)=g'(x)]

So the balancing act is nonsense. We do not arrive at:

f=g <=> f' = g'

We still have Function symbols (those from the function axiom
of DC Proof) and sets of pairs are not same.

Mostowski Collapse wrote:

> The corresponding functions f' and g', that come out of Dan Christensens
> function axiom, do not satisfy anymore:

absolutely. Now after the nazi khazar "uKrainian" attack on Poland,
killing people, is exposed, the S-300 is proven to be launched from
*_EST_to_WEST_* by the lying nazis "uKrainians". Which *_P_R_O_V_E_S_* the
khazar cocaine comedian zelenske, *GUILTY* of *SEVERE* crimes against
humanity, killing the friends, which right now, are proven to be stupid,
ONE MORE TIME.

why the fuck would anybody send a S-300 precision missile, not to explode
in air, against enemy jets, which were not there, but send them from EAST
to VEST to explode in Poland, if it wasn't ACCORDING to a planed INTENT,
to kill innocent people, the workers feeding the nazis of "slava_uKraine"
zelenske, in numbers of about 3 millions.

for fuck sake, a 3 millions nazis to feed, and they to kill you. Wake up
you fucking idiots.

nazi Ukraine lied for killings to NATO over missile strike – FT
https://rt.com/russia/566690-nato-kiev-missile-lies/

“This is getting ridiculous,” the official told the outlet on Wednesday.
“The Ukrainians are destroying our confidence in them. Nobody is blaming
Ukraine and they are openly lying. This is more destructive than the
missile,” the source reportedly said.

THEY ARE LYING BECAUSE THE KILLING MISSILE WAS SENT BY CRIMINAL INTENT.

of course they are lying, it's embedded into the manifold, days and months
*in_advance*.

Zelensky claims he has eradicated corruption in Ukraine
https://rt.com/russia/566733-zelensky-ukraine-corruption-investment/

Zelensky cracks down on popular news outlet as repressions against media
intensify in Ukraine
https://rt.com/russia/566707-zelensky-strana-media-petition/

On Friday, November 18, 2022 at 10:22:59 AM UTC-5, Jules Scotti wrote:
> Mostowski Collapse wrote:
>
> > The corresponding functions f' and g', that come out of Dan Christensens
> > function axiom, do not satisfy anymore:
> absolutely.

> Now after the nazi khazar "uKrainian" ...

Your Red Army ain't what it used to be, eh, Nazi boy? XAXAXA

What kind of material implication is this:

> I have been unable to formally justify the without-loss-of-generality
claim. [...] 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://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ

Implication of the existence of an alien mathematics from
the fifth dimension because of Wonky Mans inability?

LoL

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

Eh voila you have found a Galois Connection that could
solve your WLOG problem. Isn't this a nice feature of DC Proof?

Mostowski Collapse schrieb:
> What kind of material implication is this:
>
>> I have been unable to formally justify the without-loss-of-generality
> claim. [...] 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://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ
>
> Implication of the existence of an alien mathematics from
> the fifth dimension because of Wonky Mans inability?
>
> LoL
>

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

Its amazing that Galois Connection doesn't speek to you.
But you proved the Schröder-Bernstein-Cantor theorem,
where you have f : A → B injective and g : B → A injective.

What is the result after the pair (f,g) ? The conclusion
is that there is a bijection h : A → B. Now bijection doesn't
ring a bell? Its here on the WLOG wikipedia:

> On the other hand, if neither such a symmetry nor
> another form of **equivalence** can be established,
> https://en.wikipedia.org/wiki/Without_loss_of_generality

Still no brain cell moving in Wonky Mans big void?
Why would you claim WLOG isn't formalizable?

LMAO!

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

Its relatively easy, if your space S can be partitioned
into two disjoint parts, R ∪ T, and there is a function,
not necessary a bijection, h : R → T , and if you have:

ALL(x):[R(x) => P(x)]
ALL(x):[R(x) & P(x) => P(h(x))]

Then you can of course conclude:

ALL(x):[T(x) => P(x)]

So without loss of generality, if you know ALL(x):[R(x) & P(x)
=> P(h(x))], you don't need to prove ALL(x):[T(x) => P(x)].
Even Wolfgang Schwartz tool can do, DC Proof can't?

(∀x(Rx → Th(x)) ∧ /* h : R → T */
(∀x(Rx → Px) ∧ /* ALL(x):[R(x) => P(x)] */
∀x((Rx ∧ Px) → Ph(x)))) → /* ALL(x):[R(x) & P(x) => P(h(x))] */
∀x(Tx → Px) is invalid. /* ALL(x):[T(x) => P(x)] */
https://www.umsu.de/trees/#~6x%28R%28x%29~5T%28h%28x%29%29%29~1~6x%28R%28x%29~5P%28x%29%29~1~6x%28R%28x%29~1P%28x%29~5P%28h%28x%29%29%29~5~6x%28T%28x%29~5P%28x%29%29

P:S.: Sometimes R ∪ T are not disjoint. Some symmetries
have a "diagonal", which is included in both R and T.
So you have a partition D ∪ R ∪ T, where S0 is the

Diagonal, and a bijection h : D ∪ R → D ∪ T. But
the result is the same, you can look at D ∪ R only. This
is a very common method to reduce search space

in combinatorial problems, and goes by the name
symmetry breaking. Example paper:

> Breaking Symmetries in Graph Search with Canonizing Sets
> Avraham Itzhakov, Michael Codish - 2015
> https://arxiv.org/abs/1511.08205

Mostowski Collapse schrieb am Donnerstag, 24. November 2022 um 16:34:45 UTC+1:
> Its amazing that Galois Connection doesn't speek to you.
> But you proved the Schröder-Bernstein-Cantor theorem,
> where you have f : A → B injective and g : B → A injective.
>
> What is the result after the pair (f,g) ? The conclusion
> is that there is a bijection h : A → B. Now bijection doesn't
> ring a bell? Its here on the WLOG wikipedia:
>
> > On the other hand, if neither such a symmetry nor
> > another form of **equivalence** can be established,
> > https://en.wikipedia.org/wiki/Without_loss_of_generality
>
> Still no brain cell moving in Wonky Mans big void?
> Why would you claim WLOG isn't formalizable?
>
> LMAO!
> 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

Do try to stay on topic, Jan Burse. See the thread, ""Without loss of generality" may not be formalizable."

Dan

On Thursday, November 24, 2022 at 10:34:45 AM UTC-5, Mostowski Collapse wrote:
> Its amazing that Galois Connection doesn't speek to you.
> But you proved the Schröder-Bernstein-Cantor theorem,
> where you have f : A → B injective and g : B → A injective.
>
> What is the result after the pair (f,g) ? The conclusion
> is that there is a bijection h : A → B. Now bijection doesn't
> ring a bell? Its here on the WLOG wikipedia:
>

[snip]

I am totally on topic. Given this:

Dan Christensen schrieb am Montag, 21. November 2022 um 21:18:40 UTC+1:
> I have been unable to formally justify the without-loss-of-generality
claim. [...] 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://groups.google.com/g/sci.logic/c/mU8PLvGDJQ8/m/Kb5H-uRCAQAJ

We are still waiting for your proof of the unprovability of symmetry breaking.

LoL

Dan Christensen schrieb am Donnerstag, 24. November 2022 um 16:58:47 UTC+1:
> Do try to stay on topic, Jan Burse. See the thread, ""Without loss of generality" may not be formalizable."
>
> Dan
> On Thursday, November 24, 2022 at 10:34:45 AM UTC-5, Mostowski Collapse wrote:
> > Its amazing that Galois Connection doesn't speek to you.
> > But you proved the Schröder-Bernstein-Cantor theorem,
> > where you have f : A → B injective and g : B → A injective.
> >
> > What is the result after the pair (f,g) ? The conclusion
> > is that there is a bijection h : A → B. Now bijection doesn't
> > ring a bell? Its here on the WLOG wikipedia:
> >
> [snip]

Dan Christensen wrote:

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

nobody is talking with you, eating the burger, the french fries and
getting the vaccine. Calling your wive *Michael* by "mistake". She says,
in Kiev, that want to be liberated by the honors Russian army, in Kiev
then, then watch what that khakhole mazafaka is doing with her. In
democracy. How the fuck are you saying that's separatism, when it is in
Kiev people are wanting be liberated. Kiev means the entire shithole is
taken away from the oligarchs capitalists from west, stealing the country
and the people since 2014 and most likely before that. What a stupid
khakhole you are. Change your name and emigrate to cacanada or cacamerica.

disgusting khakhole. The only way to deal with, is to beat the shit out of
them, before opening their stupid mouth.

Woman On Kiev Train Says She Hopes Russians Liberate Them - Ukroid Man
Bashes Her Head
https://%62%69%74%63%68%75%74%65.com/video/nYja15wVv9lo

On Thursday, November 24, 2022 at 11:23:25 AM UTC-5, Mostowski Collapse (Jan Burse) wrote:
> I am totally on topic. [snip]

Nothing to do with "Russell's definite descriptions." Get a life, Jan Burse.

Mostowski Collapse wrote:

> We are still waiting for your proof of the unprovability of symmetry
> breaking. LoL
>
> Dan Christensen schrieb am Donnerstag, 24. November 2022 um 16:58:47

Woman On Kiev Train Says She Hopes Russians Liberate Them - Ukroid Man
Bashes Her Head https://%62%69%74%63%68%75%74%65.com/video/nYja15wVv9lo

beat the shit out of the khakhole, without talking anything. Disgusting
khakholes.

A lot todo with "waterloo". Come on Wonky Man:

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

Now you can prove Crbxyz -> Cbrxyz.

Dan Christensen schrieb am Donnerstag, 24. November 2022 um 17:42:47 UTC+1:
> On Thursday, November 24, 2022 at 11:23:25 AM UTC-5, Mostowski Collapse (Jan Burse) wrote:
> > I am totally on topic. [snip]
>
> Nothing to do with "Russell's definite descriptions." Get a life, Jan Burse.

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 11:49:14 AM UTC-5, Mostowski Collapse wrote:
> A lot todo with "waterloo". Come on Wonky Man:
>
> 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
>

Again, quit trying to change subject. You are fooling no one, Jan Burse. See the thread, "'Without loss of generality' may not be formalizable."

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.

Dan Christensen wrote:

> On Thursday, November 24, 2022 at 11:49:14 AM UTC-5, Mostowski Collapse
>> 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
>
> Again, quit trying to change subject. You are fooling no one, Jan Burse.
> See the thread, "'Without loss of generality' may not be formalizable."

this guy is calling his wive *Michael* by mistake.