Now that you have this nifty theorem, for a domain of
discourse that potentially has also sets:

28 ALL(s):[Set(s) => EXIST(a):~a e s]
Rem DNeg, 27
http://www.dcproof.com/UniversalSet.htm

Can you also prove what Quine proves here:

212. ALL(y):EXIST(x):[x =\= y]
https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up

I mean if ~a e s, then s u {a} =\= s. But how would
we get rid of Set(s), so that we don't end up with

ALL(y):[Set(y) => ...]. Do we even have in DC Proof
~EXIST(x): [Set(x) & ~Set(x)] ? Would this help?

Why can Quine even prove it? Does he by chance assume
a non-empty universe? Although ALL(y):... would be automatically
true in a empty universe. And for a non-empty universe there is

only the struggle between sets and urelements. What does the
subset axiom do for an urelement? It could treat the urelement
like the empty set. Quine writes:

"With help of f210 and *202 it is now possible to prove a theorem
to the effect that, whatever y may be, there is something else.; in
other words, that there is more than one entity."
212. ALL(y):EXIST(x):[x =\= y]
https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up

But this is from his "new foundation" I guess. His 210 is already
a little alien, it has a) existence of the some universal set V,
and curiously this set has b) V e V. And his 202 is subset axiom,

but unrestricted, respectively restricted to V, also alien to normal
set theory. He also shows somewhere existence of empty set
Λ, written by a kind of greek big lambda, not sure whether his proof 212

amounts to showing V =\= Λ, at least this would also suffice. Right?

Mostowski Collapse schrieb am Sonntag, 20. November 2022 um 20:25:43 UTC+1:
> Now that you have this nifty theorem, for a domain of
> discourse that potentially has also sets:
>
> 28 ALL(s):[Set(s) => EXIST(a):~a e s]
> Rem DNeg, 27
> http://www.dcproof.com/UniversalSet.htm
>
> Can you also prove what Quine proves here:
>
> 212. ALL(y):EXIST(x):[x =\= y]
> https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up
>
> I mean if ~a e s, then s u {a} =\= s. But how would
> we get rid of Set(s), so that we don't end up with
>
> ALL(y):[Set(y) => ...]. Do we even have in DC Proof
> ~EXIST(x): [Set(x) & ~Set(x)] ? Would this help?

I think Dan could prove this here:

ALL(s):[Set(s) => ALL(y):EXIST(x):[~x=y]]

Because he can use Set(s) to construct the empty set. And he
can use Set(s) to construct s u {a} which will not be empty.
As soon as we have two elements the conclusion follows:

∃x∃y¬x=y → ∀x∃y¬x=y is valid.
https://www.umsu.de/trees/#~7x~7y%28~3x=y%29~5~6x~7y%28~3x=y%29

Funny theorem, which gives the impression of a movement
where a quantifier goes from ∃x to ∀x. But can we get rid
of the ALL(s):[Set(s) => ..] precondition? So as to arrive

at the same result as Quine. So Quine assumes a non-empty
domain of discourse, even more specifically he has EXIST(a):Set(a).
So where are the many text books that don't assume a non-empty

domain of discourse, I am still currious!

Mostowski Collapse schrieb am Sonntag, 20. November 2022 um 20:35:42 UTC+1:
> Why can Quine even prove it? Does he by chance assume
> a non-empty universe? Although ALL(y):... would be automatically
> true in a empty universe. And for a non-empty universe there is
>
> only the struggle between sets and urelements. What does the
> subset axiom do for an urelement? It could treat the urelement
> like the empty set. Quine writes:
>
> "With help of f210 and *202 it is now possible to prove a theorem
> to the effect that, whatever y may be, there is something else.; in
> other words, that there is more than one entity."
> 212. ALL(y):EXIST(x):[x =\= y]
> https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up
> But this is from his "new foundation" I guess. His 210 is already
> a little alien, it has a) existence of the some universal set V,
> and curiously this set has b) V e V. And his 202 is subset axiom,
>
> but unrestricted, respectively restricted to V, also alien to normal
> set theory. He also shows somewhere existence of empty set
> Λ, written by a kind of greek big lambda, not sure whether his proof 212
>
> amounts to showing V =\= Λ, at least this would also suffice. Right?
> Mostowski Collapse schrieb am Sonntag, 20. November 2022 um 20:25:43 UTC+1:
> > Now that you have this nifty theorem, for a domain of
> > discourse that potentially has also sets:
> >
> > 28 ALL(s):[Set(s) => EXIST(a):~a e s]
> > Rem DNeg, 27
> > http://www.dcproof.com/UniversalSet.htm
> >
> > Can you also prove what Quine proves here:
> >
> > 212. ALL(y):EXIST(x):[x =\= y]
> > https://archive.org/details/QUINEMathematicalLogic/page/n175/mode/2up
> >
> > I mean if ~a e s, then s u {a} =\= s. But how would
> > we get rid of Set(s), so that we don't end up with
> >
> > ALL(y):[Set(y) => ...]. Do we even have in DC Proof
> > ~EXIST(x): [Set(x) & ~Set(x)] ? Would this help?