The non-existence of the set of all things that are NOT purple

[Dan Christensen]

I wrote the attached proof in response to a discussion at Quora. Here I show that, in set theory, there exists no set of all those things that are NOT PURPLE.

In the language of set theory: For every set p, there does NOT exist a set p' of all those elements NOT in p.

ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

Your comments are welcomed.

Dan

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


THE NON-EXISTENCE OF UNIVERSAL SET COMPLEMENTS

THEOREM

ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)]
=> ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

PROOF:

Suppose we have set p such that...

1 Set(p) & ALL(b):[b in p <=> P(b)]
Premise

2 Set(p)
Split, 1

3 ALL(b):[b in p <=> P(b)]
Split, 1


Suppose to the contrary that we have set p' (the complement of p) such that...

4 Set(p') & ALL(b):[b in p' <=> ~b in p]
Premise

5 Set(p')
Split, 4

6 ALL(b):[b in p' <=> ~b in p]
Split, 4

Apply axiom of Pairwise Union

7 ALL(a):ALL(b):[Set(a) & Set(b) => EXIST(c):[Set(c) & ALL(d):[d in c <=> d in a | d in b]]]
Pw Union

8 ALL(b):[Set(p) & Set(b) => EXIST(c):[Set(c) & ALL(d):[d in c <=> d in p | d in b]]]
U Spec, 7

9 Set(p) & Set(p') => EXIST(c):[Set(c) & ALL(d):[d in c <=> d in p | d in p']]
U Spec, 8

10 Set(p) & Set(p')
Join, 2, 5

11 EXIST(c):[Set(c) & ALL(d):[d in c <=> d in p | d in p']]
Detach, 9, 10

12 Set(u) & ALL(d):[d in u <=> d in p | d in p']
E Spec, 11

Define: Set u (the "universal set", the union of p and p')

13 Set(u)
Split, 12

14 ALL(d):[d in u <=> d in p | d in p']
Split, 12


Suppose to the contrary that we have x such that...

15 ~x in u
Premise

16 x in u <=> x in p | x in p'
U Spec, 14

17 [x in u => x in p | x in p'] & [x in p | x in p' => x in u]
Iff-And, 16

18 x in u => x in p | x in p'
Split, 17

19 x in p | x in p' => x in u
Split, 17

20 ~x in u => ~[x in p | x in p']
Contra, 19

21 ~[x in p | x in p']
Detach, 20, 15

22 ~[~x in p => x in p']
Imply-Or, 21

23 x in p' <=> ~x in p
U Spec, 6

24 [x in p' => ~x in p] & [~x in p => x in p']
Iff-And, 23

25 x in p' => ~x in p
Split, 24

26 ~x in p => x in p'
Split, 24

27 ~[~x in p => x in p'] & [~x in p => x in p']
Join, 22, 26

By contradiction...

28 ~EXIST(a):~a in u
Conclusion, 15

29 ~~ALL(a):~~a in u
Quant, 28

30 ALL(a):~~a in u
Rem DNeg, 29

31 ALL(a):a in u
Rem DNeg, 30

Apply axiom of Arbitrary Subsets

32 EXIST(r):[Set(r) & ALL(a):[a in r <=> a in u & ~a in a]]
Subset, 13

33 Set(r) & ALL(a):[a in r <=> a in u & ~a in a]
E Spec, 32

34 Set(r)
Split, 33

35 ALL(a):[a in r <=> a in u & ~a in a]
Split, 33

36 r in r <=> r in u & ~r in r
U Spec, 35

37 [r in r => r in u & ~r in r] & [r in u & ~r in r => r in r]
Iff-And, 36

38 r in r => r in u & ~r in r
Split, 37

39 r in u & ~r in r => r in r
Split, 37

Suppose to the contrary...

40 r in r
Premise

41 r in u & ~r in r
Detach, 38, 40

42 ~r in r
Split, 41

43 r in r & ~r in r
Join, 40, 42

By contradiction...

44 ~r in r
Conclusion, 40

45 r in u
U Spec, 31

46 r in u & ~r in r
Join, 45, 44

47 r in r
Detach, 39, 46

48 ~r in r & r in r
Join, 44, 47

By contradiction...

49 ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]
Conclusion, 4

As Required:

50 ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)]
=> ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
Conclusion, 1

[Mostowski Collapse]

You can directly prove:

ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

You don't need ALL(b):[b in p <=> P(b)].

Or verbally, for every set p, V \ p is a proper class.

[Mostowski Collapse]

Proof:
If V \ p were a set, then (V \ p) u p = V were also set,
since the union of two sets is a set. But we already
know that V is a proper class, contradiction.

Q.E.D.

Thanks for the proof idea.

[Mostowski Collapse]

Disclaimer: I am not aware how hard or difficult it
is to prove it without ALL(b):[b in p <=> P(b)] already
in the premisses, according to Basic Set Theory by Levy

classes can be desugared, i.e. they are only syntactic sugar.

[Mostowski Collapse]

Maybe there is even a misconception what you effectively prove,
as misconception related to material implication.

You will not prove that NOT PURPEL is proper class,
when PURPLE is a proper class or a set. So for P proper
class or set, you will not prove that V \ P is a proper class.

Because such a theorem even does not exist, V \ P can
be a set, when P is a class. This is because your implication
will be vacously true when ALL(b):[b in p <=> P(b)] fails. And

ALL(b):[b in p <=> P(b)] will fail whenever P is a proper class
and b is a set, the later is always the case. So what you only
prove will be that NOT SET-LIKE PURPEL is a proper

class. You will only prove for every set p, that V \ p is a proper class.
In fact you can directly prove:

ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

Dan Christensen schrieb am Samstag, 30. Oktober 2021 um 23:31:23 UTC+2:

[Dan Christensen]

On Saturday, October 30, 2021 at 5:42:13 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 30. Oktober 2021 um 23:31:23 UTC+2:
> > I wrote the attached proof in response to a discussion at Quora. Here I show that, in set theory, there exists no set of all those things that are NOT PURPLE.
> >
> > In the language of set theory: For every set p, there does NOT exist a set p' of all those elements NOT in p.
> >
> > ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> >

[snip]

> You can directly prove:
>
> ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
>
> You don't need ALL(b):[b in p <=> P(b)].
>
> Or verbally, for every set p, V \ p is a proper class.

Do pay attention, Jan Burse. Perhaps you missed the bit about SETS and SET THEORY? Nothing here what about you call "classes." Just "sets."

[Dan Christensen]

On Saturday, October 30, 2021 at 10:30:37 PM UTC-4, Dan Christensen wrote:
> On Saturday, October 30, 2021 at 5:42:13 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Samstag, 30. Oktober 2021 um 23:31:23 UTC+2:
> > > I wrote the attached proof in response to a discussion at Quora. Here I show that, in set theory, there exists no set of all those things that are NOT PURPLE.
> > >
> > > In the language of set theory: For every set p, there does NOT exist a set p' of all those elements NOT in p.
> > >
> > > ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> > >
> [snip]
> > You can directly prove:
> >
> > ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> >
> > You don't need ALL(b):[b in p <=> P(b)].
> >
> > Or verbally, for every set p, V \ p is a proper class.
> Do pay attention, Jan Burse. Perhaps you missed the bit about SETS and SET THEORY? Nothing here what about you call "classes." Just "sets."

Is this not still the case:

"Zermelo–Fraenkel set theory is intended to formalize a single primitive notion, that of a hereditary well-founded set, so that all entities in the universe of discourse are such sets. Thus the axioms of Zermelo–Fraenkel set theory refer only to pure sets and prevent its models from containing urelements (elements of sets that are not themselves sets). Furthermore, proper classes (collections of mathematical objects defined by a property shared by their members where the collections are too big to be sets) can only be treated INDIRECTLY [???]. Specifically, Zermelo–Fraenkel set theory does not allow for the existence of a universal set (a set containing all sets) nor for unrestricted comprehension, thereby avoiding Russell's paradox."

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory

[Julio Di Egidio]

On Saturday, 30 October 2021 at 23:31:23 UTC+2, Dan Christensen wrote:

> In the language of set theory: For every set p, there does NOT exist a set p' of all those elements NOT in p.

So, by your token, in the language of set theory set complements do not exist.

You are stupid beyond the pale even of a nazi spammer...

*Plonk*

Julio

[Mostowski Collapse]

The phrase "X is a proper class" translates to:

~EXIST(a):ALL(b):[b e a <=> X(b)]

The above is a ZFC formula, if X is a ZFC formula.

It similar like translating Russells "the X is Y", you also
called me first names, and said I am using non-classical
logic whatever. But classes are only syntactic

sugar, see Basic Set Theory by Levy:
https://www.amazon.com/dp/0486420795

Since you want to prove "non-existence of a set such
that X", using the established phrase "X is a proper class"
instead is the right thing to do.

[Mostowski Collapse]

In as far one can prove the stronger:

ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

Which would then imply the unnecessary, which has a redundant ALL(b):[b in p <=> P(b)]:

ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

[Mostowski Collapse]

Here is a prediction, it will again take 100 days from now
until Dan-O-Matik, Slow-O-Matik, Dull-O-Matik will prove
the stonger. In this interval he will divert into

crank discussions about classes, since he has no clue
how set theory deals with classes. Maybe he will even
come up with some new inventions, like

he invented "some X is Y" to translate "the X is Y".

LoL

BTW: Example set theory translates the phrase
"X equals Y" where X and Y are classes into:

ALL(a):[X(a) <=> Y(a)]

Again a ZFC formula when X and Y are ZFC formulas.
This is called extensional equality of classes.

[Dan Christensen]

On Sunday, October 31, 2021 at 4:36:11 AM UTC-4, Mostowski Collapse wrote:
> The phrase "X is a proper class" translates to:
>
> ~EXIST(a):ALL(b):[b e a <=> X(b)]
>
> The above is a ZFC formula, if X is a ZFC formula.
>
> It similar like translating Russells "the X is Y", you also
> called me first names, and said I am using non-classical
> logic whatever. But classes are only syntactic
>
> sugar, see Basic Set Theory by Levy:
> https://www.amazon.com/dp/0486420795
>
> Since you want to prove "non-existence of a set such
> that X", using the established phrase "X is a proper class"
> instead is the right thing to do.

Too much hand waving for my liking. Will stick to ZFC or my own ZFC-like set theory (without "classes") for now.

BTW, I see no mention of "classes" in Hewitt and Stromberg's "Real and Abstract Analysis." No absolute, just relative set complements (p.3-4). That's good enough for me.

[Mostowski Collapse]

Well you can re-read Russell. Its common
practice to have phrases "X" with one
paramteer. And then turn them into

FOL "X(a)". Thats nothing outside ZFC.
Saying:

"The set of elements such that X does not exist"

Is the same as saying:

"X is a proper class"

Thats very common already for 100 years.
Just re-read Russell, he uses the letter
C for such sentences that have a parameter.

But it goes back much earlier Zermelo,
Neumann, Peano, etc.. all were fluent in having
the word "class" basically standing

for a prametric FOL formula.

You can also buy this booklet, and read
the first few chapters, which also introduces
you to this 100 year old approach:

Basic Set Theory, Levy - 13. August 2002
https://www.amazon.com/dp/0486420795


Its actually 2000 year old, already Aristoteles
was using it, when he discussed "some X is Y"
and "all X are Y". X and Y are also classes.

Dan Christensen schrieb:

[Mostowski Collapse]

But I have more doubt about your DC Proof
capabilities, then whether you would some
time soon understand the concept of classes.

I doubt you can prove in DC Proof:

ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

Why didn't you prove it in your first take?
Too complicated? Why would you prove
a longer formula as a theorem,

when y shorter theorem is available?
This violates conciseness of mathematics.
It shows that the mathematician didn't

do his homework and didn't explore the
shorter formula. It tells that the mathematician
didn't think the problem through.

Why didn't you prove the shorter formula Dan-O-Matik?

Mostowski Collapse schrieb:

[Mostowski Collapse]

Yeah maybe re-read Russell. Its relatively
trivial the concept of a class:

"my theory, briefly, is as follows. I take
the noztion of the variable as fundamental;
I us "C (x) " to mean a proposition in
which x is a consituent, where x, the variable,
is essentially and wholly undetermined."
https://www.uvm.edu/~lderosse/courses/lang/Russell(1905).pdf

In Russells "the X" quantifier, basically
says the class must be a singleton. You
can verbally rephrase the uniqueness quantifier:

EXISTUNIQUE(a):X(a)

As the class X is some singleton a, or
even much shorter, EXIST(a):[X = {a}]. Now
I used equality between a class and a set,

but since sets are transferable into
classes, every set S is also a class, by
virtue of the proposition C(x)= x e S.

The meaning of EXIST(a):[X = {a}] can be derived
from class equality. So it says:

EXIST(a):ALL(b):[X(b) <=> b e {a}]

Which is the same as:

EXIST(a):ALL(b):[X(b) <=> a=b]

Eh voila we have derived some first
order reading for EXISTUNIQUE, simply
from some reading for classes.

Classes are ultra cool! They are the
coolest thing of logic. It helps you very
much in logical thinking.

Mostowski Collapse schrieb:

[Ross A. Finlayson]

Of course usual naive "universes" of closed categories,
are, 'sets in set theory'.

I.e., for any set of things, there is the set of purple of them
and the set of not purple of them.

Or at all purple, or all purple,
or not all purple, or not at all purple.

(Or not at all purple, or not all purple.)

Hey you must keep all four in either/or the minus.

Purple and/or not purple....

[Mostowski Collapse]

Dan-O-Matik didn't postulate a set U of all things.
He is not looking at b = { a e U | P(a) }. Then you could
form b' = { a e U | ~P(a) ] and b and b' are both sets

because of set comprehension:

The ZFC Set Comprehension Axiom:
https://en.wikipedia.org/wiki/Axiom_schema_of_specification

trivially you cannot provoke a contradiction
anymore since b u b' = U, which is a set.
But if you use b' = V \ b, then you can provoke

a contradiction. V \ b can be derived as
the proposition C(x) = ~(x e b). This follows
trivially since C1(x) = true is the proposition

for the univrersal set V, and C2(x) = x e b
is the proposition for the set b, then class
difference V \ b has the proposition

C1(x) & ~C2(x)

Which is:

true & ~(x e b)

Which is:

~(x e b)

Have Fun!

[Julio Di Egidio]

On Sunday, 31 October 2021 at 17:01:30 UTC+1, Mostowski Collapse wrote:

> Dan-O-Matik didn't postulate a set U of all things.

Because he is an idiot: the complement of a set exists only with reference to a containing set. And, to add to the usual half-assed and false theorem, he also offers the usual formalisation that has fuck all to do with what he claimed. But, as long as DC proof says it's proved, "it" is proved, chants that idiot, to the sound of a known rotten march.

But you too are just an incompetent spammer or I shouldn't have to explain that much, ad nauseam, always about the same basic stuff...

EOD.

Julio

[Dan Christensen]

On Sunday, October 31, 2021 at 11:36:25 AM UTC-4, Mostowski Collapse wrote:
> But I have more doubt about your DC Proof
> capabilities, then whether you would some
> time soon understand the concept of classes.
>
> I doubt you can prove in DC Proof:
> ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> Why didn't you prove it in your first take?

Do pay attention, Jan Burse! The predicate P was such that P(x) = "x is purple". See the heading. Still don't get it? Oh, well...

Dan

[Ross A. Finlayson]

The predicate that is modeled by sets that are it or aren't it?

(Which might usually enough be a class, but in the world of
sets is a set.)

I.e. whatever results by separation is for what results that
predicates exist, in a pure set theory: sets.

[An Own]

Is there a set of all things that *are* purple? I can tell you from experience that every set that does not contains itself is the most beautiful purple you have ever seen...

[Mostowski Collapse]

I already wrote that there is a bug somewhere in
your reasoning, because if purple must be SET-LIKE
PURPLE (a set) and not PURPLE (a predication aka class).

You cannot prove this one, it has a counter model,
for example P = V is a counter model, the complement
is then {}, the empty set, which is set and not a proper class:

/* Not Provable, doesn't hold for all P */
~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~P(b)]]]

But you can prove this one:

/* Provable */

ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

[Mostowski Collapse]

The bug in your reasoning has to do with material
implication and naive comprehension, you think
your precondition always returns true for some P:

/* This is Frege Naive Comprehension, such p DOES NOT always exist */
ALL(b):[b in p <=> P(b)]

For example what if P is the Russell Set? i.e. what if
P(x) <=> true. Then p would need to be the Russell Set.
So the precondition ALL(b):[b in p <=> P(b)] fails whenever

P is a proper class, and therefore when you prove this here:

ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

P is irrelevant. It will be anyway pinned to the set
p, and not vice versa. It is not that P pins the set
p, this is impossible, its the other way arround,

you have the universal quantifier for p, and implicitly
P is also universally quantified, you can write
ALL(b):[b in p <=> P(b)] as follows:

p = P

and all you prove is, making the quantification P explicit:

/* Thats all you prove, explicit form */
ALL(P):ALL(p):[Set(p) & p = P => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

But the two quantifiers ALL can switch position. And one
quantifier can move inside. So basically you prove:

/* Thats all you prove, after quantifier movements */
ALL(p):[Set(p) & ALL(P):[p = P => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]]

And now you can use substitution and eliminate the ALL(P) quantifier
namely ALL(x):[t = x => A] is equivalent to A[x/t], so basically you
prove, but P doesn't occur in the RHS of =>:

/* Thats all you prove, after class substitution */
ALL(p):[Set(p) & ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]]

[Mostowski Collapse]

P is irrelevant in your proof. It can be eliminated.
You can show that these two are logically quivalent:

1)
ALL(P):ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

2)

ALL(p):[Set(p) & ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]]

1) and 2) are logically equivalent, irrespective of the
background set theory, only by virtue of FOL.

[Mostowski Collapse]

Separation can be formulated as a class menomic:

"a n C = b"

Which says the intersection of a set a with a proper class
C, is again a set b. Just unravel a, C and b, and you get:

forall x(x e a & C(x) <=> x e b)

And now the ZFC comprehension axiom schema says:

forall C forall a exists b forall x(x e a & C(x) <=> x e b)

> The ZFC Set Comprehension Axiom:
> https://en.wikipedia.org/wiki/Axiom_schema_of_specification

But what we are dealing here is not intersection,
but difference, its about "NOT purple". The other
theorem here can be formulated as a class menomic:

"C \ a = D"

Which says if you subtract a set from a proper class, you
still get a proper class. But there is no theorem "C \ D = E",
because if you subtract two proper classes, you can

indeed get a set sometimes.

[Mostowski Collapse]

Because there is no theorem "C \ D = E", Dan-O-Matik
errs when he thinks PURPLE can be proper class.
It is of course only SET-LIKE PURPLE, some set p,

which are the purple objects. Then we are inside the
theorem "C \ a = D", just use for C = V and for a = p,
and then you get that "V \ p = D".

But if PURPLE were a proper class P, we wouldn't
know whether "V \ P" is a proper class or set. Both
is possible. Its possible that "V \ P" is a set and its

possible that "V \ P" is a proper class. Because both
are possible, there is no theorem:

/* Not Provable, doesn't hold for all P */

~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~P(b)]]]

These things were discovered 100 years ago,
when Russell wrote a letter to Frege, and bombed
his naive set comprehension.

LoL

[Mostowski Collapse]

If Dan-O-Matik would have proved V \ P is a proper
class, i.e. not a set, he would found an inconsistency
in set theory. Because there is an easy counter model.

Take P = V, i.e. assume everything is purple, then V \ P = {},
i.e. nothing is not purple. But {} is a set. A contradiction
to any proof that would show V \ P (NOT PURPLE)

is not a set. V \ P is not always not a set. On the other hand
NOT SET-LIKE PURPLE, i.e. V \ p, is indeed always not a set.

[Jim Burns]

On 10/30/2021 5:31 PM, Dan Christensen wrote:

> I wrote the attached proof in response to a discussion
> at Quora. Here I show that, in set theory, there exists
> no set of all those things that are NOT PURPLE.

I'm sure that depends upon what the set theory is.

> In the language of set theory: For every set p, there
> does NOT exist a set p' of all those elements NOT in p.

Consider this set theory for sets of
individuals-which-are-not-sets.

( Let x,y,z,... possibly refer to any _individual_
( in the domain of discussion and, thus, not to a set.
( Let A,B,C,... possibly refer to any _set_ of
( individuals in the domain of discussion, and, this,
( not an individual.
(
( Notation.
( '∀x' '∃y' and so on quantify over individuals
( '∀∀A' '∃∃B' and so on quantify over sets.

I. Comprehension
For a predicate P(x) on an individual x,
a set B exists which contains exactly those
individuals x for which P(x) is true.
|
| ∃∃B, ∀x ( x ∈ B <-> P(x) )

II. Extensionality
Sets with the same elements are equal.
|
| ∀∀ B,C ( ∀x (x ∈ B <-> x ∈ B) -> B = C )

----
Let PURPLE be the set of purple things

∃∃B, ∀x ( x ∈ B <-> x ∉ PURPLE )

----
This theory is not ZFC.
I haven't kept up with your work, but
I think your theory is not ZFC, either.

And this is the theory I have been using in my
discussions with WM. Its axioms are very agreeable
to the median intuition, it's Comprehension axiom
makes for short proofs.

Given how long my discussions with WM have been,
it's at least possible that, in some global sense,
my theory has been used more than yours.

Anyway, it is what it is.
My point is that _what the theory is_ is relevant.

[Mostowski Collapse]

If you have a two sorted language, you can
indeed, under certain circumstances, postuale
such a comprehension axiom:

∃B, ∀x ( x ∈ B <-> P(x) )

This is typically what would be allowed in SOL,
second order logic, where you also follow the
x,y,z,... and the A,B,C,... convention.

The “Set theory in sheep’s clothing” doesn't
work really. Since in SOL you have two domains,
since you have two sorts,

and they are interconnected, but since true
SOL has no calculus, you would need general
semantics, and then the interconnection

is a little bit looser. If it were "Set theory in sheep's
clothing", the individual domain I would be a set
and the set domain would P(I). But who says

I could not be a class. And then P(I) would be
the powerset of a class? So I would read DC Proof
rather towards FOL and ZFC, although DC Proof

is a little ambigious here. It allows function quantification
but not predicate quantification, making it a form of
SOL, and it is not definitional consistent, you can

derive an inconsistency from some predicate definition,
using self application. Self application is usually forbidden
in a two sorted setting, you cannot write:

A(A)

But this is allowed in DC Proof for function symbols,
thats also how you can provoke an inconsistency. So to
not frustrate Dan-O-Matik too much, a benevolent

reading of his postings is possibly FOL and ZFC.

[Mostowski Collapse]

Another alternative would be to use ZFC + Universe. The idea
of universes is due to Alexander Grothendieck, who used
them as a way of avoiding proper classes in algebraic geometry.

Could then say for a SET-LIKE PURPLE p, there is some universe
u, with p e u. And we would form u \ p, which is again a set.
But there are many universes u with p e u. Actually there is

a new paradox:

- Grothendieck paradox: In ZFC + Universe, the class of universes
aka inaccessible cardinals is a proper class.

But since the intersection of any class of universes is a universe,
we can pick the smallest universe with p e u? Ha Ha, a lot of
class based reasoning, only to get rid of proper classes.

LoL

Mostowski Collapse schrieb:

[Jim Burns]

On 10/31/2021 8:34 PM, Mostowski Collapse wrote:

> If it were "Set theory in sheep's clothing",

I'm not clear on what you're calling "set theory in
sheep's clothing". Is it the theory I presented?

Since I'm calling it a set theory, it seems as though
"a wolf in set theory's clothing" would be more
appropriate. I consider "a set theory" even more
appropriate than that.

To be honest, I am thinking of plural quantification.
https://en.wikipedia.org/wiki/Plural_quantification
https://plato.stanford.edu/entries/plural-quant/

In those links, A,B,C,... are regarded as not-quite-sets,
pluralities.

I know there are interesting discussions going on about
the ontological status of pluralities, etc, but all I
want to do is describe natural numbers and end segments
and other things that appear in our discussions.
I have called them "pluralities" until I stopped doing
that. The unusual name for them is a nice way to direct
attention to those more technical conversations, but
that is the precise opposite of where I want attention
directed. I want to talk about natural numbers.

( I suppose writing set quantifiers as '∀∀A' '∃∃B'
( doesn't completely support my goal of making
( normal-acting stuff look normal. But there are
( two distinct domains. It seems as though that
( deserves a footnote or something.

Surely, pluralities fall under some wide conceptual umbrella
labeled "sets", where the hereditarily finite sets and
the proper classes and non-well-founded sets also fall.
If this is not a set theory, I would like it explained
why it isn't.

> If it were "Set theory in sheep's clothing",
> the individual domain I would be a set
> and the set domain would P(I). But who says
> I could not be a class. And then P(I) would be
> the powerset of a class?

In this theory,
the individual domain 𝕀 is an element of the set domain 𝕊.
∀x ( x ∈ 𝕀 <-> x = x )

But 𝕊 would be P(𝕀) if P(𝕀) existed.
I suppose this doesn't slay any paradoxes, just
moves them around a bit.

> Jim Burns schrieb
> am Montag, 1. November 2021 um 01:15:17 UTC+1:
>> I. Comprehension
>> For a predicate P(x) on an individual x,
>> a set B exists which contains exactly those
>> individuals x for which P(x) is true.
>> |
>> | ∃B, ∀x ( x ∈ B <-> P(x) )

That should read
| ∃∃B, ∀x ( x ∈ B <-> P(x) )

I'm confident that you can say what you mean to say
without misquoting me.

[Mostowski Collapse]

I am not using ∃∃, only ∃, since the disambiguation
of the two quantifiers happens already by the sort of
the variable. If you have the comprehension,

then it follows:

∃I ∀x ( x ∈ I <-> x = x )

Which only gives you I e S.

What gives you S = P(I)?

[Mostowski Collapse]

BTW: “Set theory in sheep’s clothing” is from here:

https://plato.stanford.edu/entries/logic-higher-order/#SetTheoSheeClot

They discuss that true SOL would be categorical
and either make CH or ~CH true. You also find
attempts of S = P(I), it seems to be quite complicated:

https://plato.stanford.edu/entries/logic-higher-order/#mjx-eqn-ex6

Somehow they dont do S = P(I) directly, some U and P(U) is
modelled. I guess U and P(U) are only subset I. Dont
remember whether I saw somewhere S = P(I).

The simpler SEP article was always this one by Herb:

https://plato.stanford.edu/archives/sum2019/entries/logic-higher-order/

[Julio Di Egidio]

On Monday, 1 November 2021 at 02:19:17 UTC+1, Mostowski Collapse wrote:

> Another alternative would be to use ZFC + Universe

A better alternative would be dropping ZF altogether, and Cantorian set theory before it: fundamentally broken re anything infinite...

Julio

[Mostowski Collapse]

Stop spamming nonsense. You already posted some nonsense
ISO core standard is fundamentally broken. Now you post ZF
is fundamentally broken. What should this even mean?

Whats fundamentally broken is your cerebrum crustae, making
it a wind canal for the void that is found inside your skull.
Not a single brain cell.

LoL

[Jim Burns]

On 11/1/2021 3:31 AM, Mostowski Collapse wrote:

> I am not using ∃∃, only ∃,

However, what you have done is make it appear that
_I_ (JB) am not using ∃∃, only ∃,
Please stop doing that.

> I am not using ∃∃, only ∃, since the disambiguation
> of the two quantifiers happens already by the sort of
> the variable.

Your usage agrees with the two links I gave.

However, your '∃B' and '∃x' quantify over two different
domains. I would like that to be very clear,
no matter what variable names I may be using next,
that they are not the same quantifier.

Perhaps I can be convicted of wearing both belt and
suspenders. Or perhaps I will only getting a stern
warning from the fashion police, before they're off
to pursue more interesting criminals.

Either way, please do not remove my belt yourself.
Asking me to take my own belt off is fine.
Thanks in advance.

> If you have the comprehension,
>
> then it follows:
>
> ∃I ∀x ( x ∈ I <-> x = x )
>
> Which only gives you I e S.
>
> What gives you S = P(I)?
>

I think Comprehension+Extensionality (CE)
doesn't give me that. This is its semantics.
I think one must go to its metatheory. Such as ZFC.

Suppose the CE-element-domain 𝕀 is a ZFC-set I
and the CE-set domain 𝕊 is its ZFC-powerset P(I).

Then, from ZFC
|| Axiom of Restricted Comprehension

we can prove in ZFC for CE
| Axiom of Comprehension.

----
I have been proceeding on the assumption that all this
has been vetted by a better-informed Them.

What I have been thinking is that the two CE-domains
are actually the ZFC-sets I⨯{0} and P(I)⨯{1}
in order that what is in CE
| ∃∃B (∃x ( x ∈ B ))

becomes, in ZFC
|| ∃B B[2]=1 ∃x x[2]=0 ( x[1] ∈ B[1] ∧ x[2]=0 ∧ B[2]=1 )

My concern is that how I've filled in the blanks maybe
allows us to claim the set of all sets not containing
themselves exists.

Up to this point, I've avoided the question by saying
| x ∉ x
is neither true nor false, but unpronounceable.
By eliminating Russell's set at the language definition.

I'm not sure my dodge continues to work
if we have only one quantifier ∃

I'm not entirely sure my dodge works anyway.

[Mostowski Collapse]

If you have a comprehension axiom, in SOL Peano,
it controls SOL induction, since it allows transfer
between set and formula, where SOL induction uses set:

∃B ∀x ( x ∈ B <-> P(x) )

You might not only ask what is the domain of
sets S, where B comes from, and what is teh domain
of individuals I, where x comes from.

You might also ask what kind of P do I allow.
This leads to reverse mathematics, which somehow
starts of with SOL Peano, and the idea to

have both I = N and S = P(N), and then looks
at what classes of P(x) exist, and what is
the prove strength, if we would restrict P(x).

RCA0: P(x) is Δ_1^0
WKL0: RCA0 plus Weak K ̈onig’s Lemma
ACA0: P(x) is Σ_1^0
ATR0: P(x) is Σ_1^1
Π_1^1-CA0: P(x) is Π_1^1

But Dan Christensen left us in the dark, whether he
uses some of this logics. Also whether p, the purple
things, stem from some resticted P(x).

Δ_1^0 is closed over complement?

[Mostowski Collapse]

Being closed over complement is often needed, for
example a sigma algebra has it:

https://en.wikipedia.org/wiki/%CE%A3-algebra#Definition

[Julio Di Egidio]

On Monday, 1 November 2021 at 14:22:11 UTC+1, Mostowski Collapse wrote:

> Stop spamming nonsense.

You stupid cunt are a systematic spammer. ESAD.

*Plonk*

Julio

[Mostowski Collapse]

You are definitively a moron. You use also classes in DC
Proof. You just posted here a proof that uses classes:

32 EXIST(r):[Set(r) & ALL(a):[a in r <=> a in u & ~a in a]]
Subset, 13

ZFC has two axiom schemas that deal with classes.
One axiom schema deals with unary predicates as classes,
and one axiom schema deals with binary mappings as classes,

the axiom schemas are:

Axiom schema of specification
It says { x | P(x) & x e y } is a set, when y is a set and P is a class
https://en.wikipedia.org/wiki/Axiom_schema_of_specification

Axiom schema of replacement
It says that { F(x) | x e y } is a set, when y is a set and F is a class
https://en.wikipedia.org/wiki/Axiom_schema_of_replacement

Your Subset is just Axiom schema of specification.
The two axiom schemas are the interface between classes
and sets in ZFC.

Dan Christensen schrieb am Sonntag, 31. Oktober 2021 um 15:11:25 UTC+1:
> On Sunday, October 31, 2021 at 4:36:11 AM UTC-4, Mostowski Collapse wrote:
> > The phrase "X is a proper class" translates to:
> >
> > ~EXIST(a):ALL(b):[b e a <=> X(b)]
> >
> > The above is a ZFC formula, if X is a ZFC formula.
> >
> > It similar like translating Russells "the X is Y", you also
> > called me first names, and said I am using non-classical
> > logic whatever. But classes are only syntactic
> >
> > sugar, see Basic Set Theory by Levy:
> > https://www.amazon.com/dp/0486420795
> >
> > Since you want to prove "non-existence of a set such
> > that X", using the established phrase "X is a proper class"
> > instead is the right thing to do.
> Too much hand waving for my liking. Will stick to ZFC or my own ZFC-like set theory (without "classes") for now.
>
> BTW, I see no mention of "classes" in Hewitt and Stromberg's "Real and Abstract Analysis." No absolute, just relative set complements (p.3-4). That's good enough for me.

[Mostowski Collapse]

The word class is used when you are interested in
the extension of a concept. A predicate does not really
capture the connotation of a class. If I say I have

a predicate P(x), one usually assumes that its intention
is also given, i.e. that you have a formula which is
the predicate P(x). By class we mean only the extensional

aspect which is defined as the elements from domain
of discourse that make the predicate true, i.e. {x | P(x)}.
In as far you can have two predicates P1 and P2 which

are intensionally different, i.e. which are different formulas,
but neverless are the same class, since {x | P1(x)} = {x | P2(x)}
a typical example where different intensions give the

same extension is the universal "set", in ZFC these are all
the same class:

{ x | true }

{ x | x = x }

{ x | ~(x e x) }

You can prove {x | P1(x)} = {x | P2(x)}, in that you simply
prove forall x (P1(x) <=> P2(x)).

[Dan Christensen]

On Sunday, October 31, 2021 at 6:35:33 PM UTC-4, Mostowski Collapse wrote:
> I already wrote that there is a bug somewhere in
> your reasoning, because if purple must be SET-LIKE
> PURPLE (a set) and not PURPLE (a predication aka class).
>
> You cannot prove this one, it has a counter model,
> for example P = V is a counter model, the complement
> is then {}, the empty set, which is set and not a proper class:
>

Again, there are no formally defined classes in ZFC. It has no V as you seem to have defined it.

[Mostowski Collapse]

V is just a shorthand for:

x = x

true

~(x e x)

In ZFC the above all have the same extension.

You should be able to prove that in DC Proof?

[Mostowski Collapse]

To deal with classes you only need FOL. Why do you
think classes have something to do with ZFC? Thats
just plain crazy Dan-O-Matik.

Classes also exist without ZFC, for example if you
don't have the relationsymbol e , membership. V is
then just a shorthand for the extension of:

x = x

true

The subject matter of ZFC is not classes. Classes come
from the underlying FOL. ZFC is a FOL theory, which
even uses classes in two of its axiom schemas.

I nowhere said classes come from ZFC. They come from
FOL (first order logic). BTW, you have them also in SOL
and HOL, but lets stick to FOL.

[Dan Christensen]

On Wednesday, November 10, 2021 at 7:09:10 AM UTC-5, Mostowski Collapse wrote:
> To deal with classes you only need FOL. Why do you
> think classes have something to do with ZFC?

Prove, using ONLY the axioms of ZFC that there exists a universal set. Good luck with that, Jan Burse.

[Mostowski Collapse]

I nowhere claimed that there exists an universal set in ZFC?

Whats wrong with you?

[Mostowski Collapse]

Now I have the feeling there is a shorter proof.
You use the universal class V = { x | x = x } to
provoke a contradiction. But the Russell class

R = { x | ~(x e x) } comes also into play. You
use it when you show that V is a proper class.
Basically you derive a contradiction as follows:

1) You assume V is a set,

2) Then by the separation axiom you get:

R = { x | ~(x e x) } = { x | x e V & ~(x e x) } is also a set.

3) Then you make the usual Russell contradiction argument.

You need 17 lines of proof for that. Thats huge.
I have seen much shorter Russell contradiction
arguments. Most likely there is a universal

proof, and maybe also a short shorter purple proof?

Mostowski Collapse schrieb am Samstag, 30. Oktober 2021 um 23:45:14 UTC+2:
> Proof:
> If V \ p were a set, then (V \ p) u p = V were also set,
> since the union of two sets is a set. But we already
> know that V is a proper class, contradiction.
>
> Q.E.D.
>
> Thanks for the proof idea.
> Mostowski Collapse schrieb am Samstag, 30. Oktober 2021 um 23:42:13 UTC+2:
> > You can directly prove:

> >
> > ALL(p):[Set(p) => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> >

> > You don't need ALL(b):[b in p <=> P(b)].
> >
> > Or verbally, for every set p, V \ p is a proper class.

> > Dan Christensen schrieb am Samstag, 30. Oktober 2021 um 23:31:23 UTC+2:
> > > I wrote the attached proof in response to a discussion at Quora. Here I show that, in set theory, there exists no set of all those things that are NOT PURPLE.
> > >

> > > In the language of set theory: For every set p, there does NOT exist a set p' of all those elements NOT in p.
> > >

> > > ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)] => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> > >
> > > Your comments are welcomed.

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

> > > THE NON-EXISTENCE OF UNIVERSAL SET COMPLEMENTS
> > >
> > > THEOREM
> > >
> > > ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)]

> > > => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]
> > >

> > > PROOF:
> > >
> > > Suppose we have set p such that...
> > >
> > > 1 Set(p) & ALL(b):[b in p <=> P(b)]
> > > Premise
> > >
> > > 2 Set(p)
> > > Split, 1
> > >
> > > 3 ALL(b):[b in p <=> P(b)]
> > > Split, 1
> > >
> > >
> > > Suppose to the contrary that we have set p' (the complement of p) such that...
> > >
> > > 4 Set(p') & ALL(b):[b in p' <=> ~b in p]
> > > Premise
> > >
> > > 5 Set(p')
> > > Split, 4
> > >
> > > 6 ALL(b):[b in p' <=> ~b in p]
> > > Split, 4
> > >
> > > Apply axiom of Pairwise Union
> > >
> > > 7 ALL(a):ALL(b):[Set(a) & Set(b) => EXIST(c):[Set(c) & ALL(d):[d in c <=> d in a | d in b]]]
> > > Pw Union
> > >
> > > 8 ALL(b):[Set(p) & Set(b) => EXIST(c):[Set(c) & ALL(d):[d in c <=> d in p | d in b]]]
> > > U Spec, 7
> > >
> > > 9 Set(p) & Set(p') => EXIST(c):[Set(c) & ALL(d):[d in c <=> d in p | d in p']]
> > > U Spec, 8
> > >
> > > 10 Set(p) & Set(p')
> > > Join, 2, 5
> > >
> > > 11 EXIST(c):[Set(c) & ALL(d):[d in c <=> d in p | d in p']]
> > > Detach, 9, 10
> > >
> > > 12 Set(u) & ALL(d):[d in u <=> d in p | d in p']
> > > E Spec, 11
> > >
> > > Define: Set u (the "universal set", the union of p and p')
> > >
> > > 13 Set(u)
> > > Split, 12
> > >
> > > 14 ALL(d):[d in u <=> d in p | d in p']
> > > Split, 12
> > >
> > >
> > > Suppose to the contrary that we have x such that...
> > >
> > > 15 ~x in u
> > > Premise
> > >
> > > 16 x in u <=> x in p | x in p'
> > > U Spec, 14
> > >
> > > 17 [x in u => x in p | x in p'] & [x in p | x in p' => x in u]
> > > Iff-And, 16
> > >
> > > 18 x in u => x in p | x in p'
> > > Split, 17
> > >
> > > 19 x in p | x in p' => x in u
> > > Split, 17
> > >
> > > 20 ~x in u => ~[x in p | x in p']
> > > Contra, 19
> > >
> > > 21 ~[x in p | x in p']
> > > Detach, 20, 15
> > >
> > > 22 ~[~x in p => x in p']
> > > Imply-Or, 21
> > >
> > > 23 x in p' <=> ~x in p
> > > U Spec, 6
> > >
> > > 24 [x in p' => ~x in p] & [~x in p => x in p']
> > > Iff-And, 23
> > >
> > > 25 x in p' => ~x in p
> > > Split, 24
> > >
> > > 26 ~x in p => x in p'
> > > Split, 24
> > >
> > > 27 ~[~x in p => x in p'] & [~x in p => x in p']
> > > Join, 22, 26
> > >
> > > By contradiction...
> > >
> > > 28 ~EXIST(a):~a in u
> > > Conclusion, 15
> > >
> > > 29 ~~ALL(a):~~a in u
> > > Quant, 28
> > >
> > > 30 ALL(a):~~a in u
> > > Rem DNeg, 29
> > >
> > > 31 ALL(a):a in u
> > > Rem DNeg, 30
> > >
> > > Apply axiom of Arbitrary Subsets

> > >
> > > 32 EXIST(r):[Set(r) & ALL(a):[a in r <=> a in u & ~a in a]]
> > > Subset, 13
> > >

> > > 33 Set(r) & ALL(a):[a in r <=> a in u & ~a in a]
> > > E Spec, 32
> > >
> > > 34 Set(r)
> > > Split, 33
> > >
> > > 35 ALL(a):[a in r <=> a in u & ~a in a]
> > > Split, 33
> > >
> > > 36 r in r <=> r in u & ~r in r
> > > U Spec, 35
> > >
> > > 37 [r in r => r in u & ~r in r] & [r in u & ~r in r => r in r]
> > > Iff-And, 36
> > >
> > > 38 r in r => r in u & ~r in r
> > > Split, 37
> > >
> > > 39 r in u & ~r in r => r in r
> > > Split, 37
> > >
> > > Suppose to the contrary...
> > >
> > > 40 r in r
> > > Premise
> > >
> > > 41 r in u & ~r in r
> > > Detach, 38, 40
> > >
> > > 42 ~r in r
> > > Split, 41
> > >
> > > 43 r in r & ~r in r
> > > Join, 40, 42
> > >
> > > By contradiction...
> > >
> > > 44 ~r in r
> > > Conclusion, 40
> > >
> > > 45 r in u
> > > U Spec, 31
> > >
> > > 46 r in u & ~r in r
> > > Join, 45, 44
> > >
> > > 47 r in r
> > > Detach, 39, 46
> > >
> > > 48 ~r in r & r in r
> > > Join, 44, 47
> > >
> > > By contradiction...
> > >
> > > 49 ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]
> > > Conclusion, 4
> > >
> > > As Required:
> > >
> > > 50 ALL(p):[Set(p) & ALL(b):[b in p <=> P(b)]

> > > => ~EXIST(p'):[Set(p') & ALL(b):[b in p' <=> ~b in p]]]

> > > Conclusion, 1

[Mostowski Collapse]

The nice thing about this kind of proof of non-existence
of the universal set, you don't need the assumption V = R.
The resulting set R in step 2) can be a subset of V.

So basically you don't need the axiom of regularity. And the
same proof would also work in some of the Non-well-founded
set theories, that do not have the axiom of regularity.

So the stipulation in Wikipedia:

"Many set theories do not allow for the existence of a universal set.
For example, it is directly contradicted by the axioms such as the
axiom of regularity and its existence would imply inconsistencies."
https://en.wikipedia.org/wiki/Universal_set

Is utter nonsense. The axiom of regularity was never needed
to show that the universal class is a proper class.

[Dan Christensen]

On Wednesday, November 10, 2021 at 10:31:22 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 10. November 2021 um 14:24:18 UTC+1:

> > On Wednesday, November 10, 2021 at 7:09:10 AM UTC-5, Mostowski Collapse wrote:
> > > To deal with classes you only need FOL.

FOL is the underlying logic of ZFC.

> > > Why do you
> > > think classes have something to do with ZFC?
> > Prove, using ONLY the axioms of ZFC that there exists a universal set. Good luck with that, Jan Burse.

> I nowhere claimed that there exists an universal set in ZFC?
>

Thanks for clearing that up, Jan Burse.

So, in ZFC you cannot deal with classes other than those are themselves sets. I guess, that's why they it SET theory, not CLASS theory!

[Mostowski Collapse]

Basically your proof can be also applied in non-well
founded set theory. See here:

https://en.wikipedia.org/wiki/Non-well-founded_set_theory

Non-well founded sets, called extra-ordinary sets
by Ross Finalyson. LoL

[Mostowski Collapse]

"Mirimanoff in a 1917 paper introduced the concept of well-founded
set and the notion of rank of a set.[5] Mirimanoff called a set x "regular"
(French: "ordinaire") if every descending chain x ∋ x1 ∋ x2 ∋ ... is finite.

Mirimanoff however did not consider his notion of regularity (well-foundedness)
as an axiom to be observed by all sets; in later papers Mirimanoff also explored
what are now called non-well-founded sets ("extraordinaire" in Mirimanoff's terminology).+"

https://en.wikipedia.org/wiki/Dmitry_Mirimanoff

Subsequently that V \ p is a proper class, the purple theorem, also holds
when p is set that has extraordinary elements, or is itself extraordinary.
Means the purple theorem does not make use of the regularity axiom,

therefore it also holds in non-well founded set theory.

[Mostowski Collapse]

Dan-O-Matik halucinated, because he doesn't have a clue:

> So, in ZFC you cannot deal with classes other than those are themselves sets.
> I guess, that's why they it SET theory, not CLASS theory!

ZFC does impact classes. Since the elements of a class
are sets, guarded by ZFC or other set theories around, the
background set theory also determines which classes

are available. Since it determines which class elements
are available. You can try yourself with your
lame and stupid DC Proof:

ZFC |- V = R

SATA |- V ≠ R

Or translation into FOL, since you are too stupid to do the
translation into FOL yourself (Like Russells the Bald King,
you are awfully bad in translating into FOL):

ZFC |- forall x(x=x <=> ~(x e x))

SATA |- exist x(x=x <=> x e x)

Do it with DC Proof. Can you?

Disclaimer: The ZFC axioms are rather clear. SATA
might be more challenging. You might need to
read Peter Aczel or some such.

Both ZFC and SATA have presumable a common subset of
axioms, which are possibly already available in DC Proof,
namely ZFC-, which is ZFC without axiom of regularity.

[Mostowski Collapse]

What is SATA? Well I mean SAFA, sorry for the typo.

- AFA ("Anti-Foundation Axiom") – due to M. Forti and F. Honsell,
- SAFA ("Scott’s AFA") – due to Dana Scott,
- FAFA ("Finsler’s AFA") – due to Paul Finsler,
- BAFA ("Boffa’s AFA") – due to Maurice Boffa.
https://en.wikipedia.org/wiki/Non-well-founded_set_theory#Details

Maybe you need to read Dana Scott and not
only Peter Aczel. But Peter Aczel is more know
for things AFA, he published a book in 1988.
https://de.wikipedia.org/wiki/Peter_Aczel

[Mostowski Collapse]

Or to make it simple so that even Dan-O-Matik understands it,
who makes hillarious posts with titles such as "The non-existence
of the set of all things that are NOT PURPLE":

- The set theory determines what THINGS are around.

For example if your set theory were ALL(x):[x = foo], then
only the thing around would be foo. What things are around
in ZFC? What things are around in SAFA?

Usually the things around are denoted by V. But V does
vary, from model to model, and since the permissible models
are guarded by the given axiom system,

V varies constrained on the axiom system you use. Since
V varies, also the NOT varies, so since V varies, also
V \ p, the NOT PURPLE things varies. The complement

V \ p is different in ZFC and SAFA, not the same class.

[Mostowski Collapse]

It might be questionable to use the Russell definite description
"the X is Y" here, for "the set of all things such that". But you
are lucky, thanks to extensionality of sets, the axiom of

separation would deliver a set that is unique inside a model.
But you apple "the X is Y" to a class, not to a set, you prove
that "the X is Y" object under consideration is not a set.

So you would need class extensionality to see that this
class is unique inside a model. Is the class unique? Does
this class buider lead to something unique?

{ x | P(x) }

Inside a model yes. But across different models no. So
when we would read "the X is Y" on meta level, because
DC Proof does only use ZFC-, it doesn't prove axiom of

regularity. Then we must say "the X is Y" would be
possibly false, since it is not uniquely determine what
the complement should be. There are kind of two Kings,

since DC Proof does only use ZFC-. Unfortunately ZFC
is never complete, also ZFC does not decide CH, so
I guess "the X is Y" is always a varying. A mathematician

would probably formulate the theorem less sassy:

"In a XYZ structure bla bla".

Where XYZ captures the axioms that are needed for
the theorem. Extensionality and comprehension are the
only needed axioms? Thats kind of a Proto Set structure?

[Dan Christensen]

On Thursday, November 11, 2021 at 8:27:43 AM UTC-5, Mostowski Collapse wrote:

> > [DC wrote:] So, in ZFC you cannot deal with classes other than those are themselves sets.

> > I guess, that's why they it SET theory, not CLASS theory!
> ZFC does impact classes. Since the elements of a class
> are sets, guarded by ZFC or other set theories around, the
> background set theory also determines which classes
>
> are available. Since it determines which class elements
> are available.
>

> ZFC |- V = R
>
> SATA |- V ≠ R
>
> Or translation into FOL, since you are too stupid to do the
> translation into FOL yourself (Like Russells the Bald King,
> you are awfully bad in translating into FOL):
>

It seems you have never gotten over the fact that since there is presently no king of France, it must therefore be vacuously true that all present kings of France are bald. Contrary to what you seem to think, it really makes no difference whether or not you also assume there is presently at most one king of France. Deal with it, Jan Burse. To get you started, you really must read: https://en.wikipedia.org/wiki/Vacuous_truth

> ZFC |- forall x(x=x <=> ~(x e x))
>
> SATA |- exist x(x=x <=> x e x)
>
> Do it with DC Proof. Can you?
>

The axioms of set theory built into (hard-coded in) DC Proof reflect those implicitly used in most math textbooks. Whether a particular set is actually an element of itself or not never seems to be an issue.

Users, can of course introduce additional axioms at the beginning of any proof, e.g. ALL(a):~a in a (line 1 below)

1 ALL(a):~a in a
Axiom

2 x=x
Premise

3 ~x in x
U Spec, 1

4 ALL(a):[a=a => ~a in a]
Conclusion, 2

5 ~y in y
Premise

6 y=y
Reflex

7 ALL(a):[~a in a => a=a]
Conclusion, 5

8 ALL(a):[[a=a => ~a in a] & [~a in a => a=a]]
Join, 4, 7

9 ALL(a):[a=a <=> ~a in a]
Iff-And, 8

Dan

[Mostowski Collapse]

ZFC doesn't have an axiom ALL(a):~a in a.
This axiom would be too weak for regularity.
For example take the natural numbers 0, 1, 2, 3, ...

and then assume there exist sets s0, s1, s2, s3, ...
With sj+1 in sj. What would prevent the existence
of such a non-well founded set s0?

ALL(a):~a in a is a theorem of ZFC, derived from
the regularity axiom and other axioms. How do
you prove this theorem?

[Dan Christensen]

> ZFC doesn't have an axiom ALL(a):~a in a.
> This axiom would be too weak for regularity.

For the ZF Axiom of Regularity, you can use:

ALL(x):[EXIST(a):a in x => EXIST(y):[y in x & ~EXIST(z):[z in y & z in x]]]

> For example take the natural numbers 0, 1, 2, 3, ...
>
> and then assume there exist sets s0, s1, s2, s3, ...
> With sj+1 in sj. What would prevent the existence
> of such a non-well founded set s0?
>
> ALL(a):~a in a is a theorem of ZFC, derived from
> the regularity axiom and other axioms. How do
> you prove this theorem?

You will also need the ZF Axiom of Pairings:

ALL(x):ALL(y):EXIST(z):[x in z & y in z]

[Dan Christensen]

On Thursday, November 11, 2021 at 2:25:00 PM UTC-5, Mostowski Collapse wrote:

> ALL(a):~a in a is a theorem of ZFC, derived from
> the regularity axiom and other axioms. How do
> you prove this theorem?

The following formal proof is based on Asaf Karagila's informal proof at MSE:

"Let A be any set. Then {A} is a set, and by regularity {A} must contain an element disjoint from {A}. The only element of {A} is A, so A n {A} = { }, and it follows immediately that ~ A in A."
https://math.stackexchange.com/questions/271555/how-does-the-axiom-of-regularity-forbid-self-containing-sets

My formal proof in DC Proof format (comments inserted):

ZF Axiom of Regularity:

1 ALL(x):[EXIST(a):a in x => EXIST(y):[y in x & ~EXIST(z):[z in y & z in x]]]
Axiom

ZF Axiom of Pairing:

2 ALL(x):ALL(y):EXIST(z):[x in z & y in z]
Axiom

Instance of the ZF Axiom Schema of Specification:

3 ALL(a):ALL(b):EXIST(c):ALL(d):[d in c <=> d in a & d=b]
Axiom


Prove: ~EXIST(a):~a in a

Suppose to the contrary...

4 x in x
Premise

5 ALL(y):EXIST(z):[x in z & y in z]
U Spec, 2

6 EXIST(z):[x in z & x in z]
U Spec, 5

7 x in z & x in z
E Spec, 6

8 x in z
Split, 7

Apply the ZF Axiom Schema of Specification to construct the singleton {x}

9 ALL(b):EXIST(c):ALL(d):[d in c <=> d in z & d=b]
U Spec, 3

10 EXIST(c):ALL(d):[d in c <=> d in z & d=x]
U Spec, 9

Define: sx (the singleton {x})

11 ALL(d):[d in sx <=> d in z & d=x]
E Spec, 10


Prove: ALL(a):[a in sx <=> a=x]

'=>'
Prove: ALL(a):[a in sx => a=x]

Suppose...

12 y in sx
Premise

13 y in sx <=> y in z & y=x
U Spec, 11

14 [y in sx => y in z & y=x] & [y in z & y=x => y in sx]
Iff-And, 13

15 y in sx => y in z & y=x
Split, 14

16 y in z & y=x
Detach, 15, 12

17 y=x
Split, 16

As Required:

18 ALL(a):[a in sx => a=x]
Conclusion, 12


'<='
Prove: ALL(a):[a=x => a in sx]

Suppose...

19 y=x
Premise

20 y in sx <=> y in z & y=x
U Spec, 11

21 [y in sx => y in z & y=x] & [y in z & y=x => y in sx]
Iff-And, 20

22 y in z & y=x => y in sx
Split, 21

23 y in z
Substitute, 19, 8

24 y in z & y=x
Join, 23, 19

25 y in sx
Detach, 22, 24

As Required:

26 ALL(a):[a=x => a in sx]
Conclusion, 19

27 ALL(a):[[a in sx => a=x] & [a=x => a in sx]]
Join, 18, 26

As Required:

28 ALL(a):[a in sx <=> a=x]
Iff-And, 27

Apply ZF Axiom of Regularity

29 EXIST(a):a in sx => EXIST(y):[y in sx & ~EXIST(z):[z in y & z in sx]]
U Spec, 1

Apply definition of sx

30 x in sx <=> x=x
U Spec, 28

31 [x in sx => x=x] & [x=x => x in sx]
Iff-And, 30

32 x=x => x in sx
Split, 31

33 x=x
Reflex

34 x in sx
Detach, 32, 33

35 EXIST(a):a in sx
E Gen, 34

36 EXIST(y):[y in sx & ~EXIST(z):[z in y & z in sx]]
Detach, 29, 35

37 y in sx & ~EXIST(z):[z in y & z in sx]
E Spec, 36

By Regularity, there exists y such that...

38 y in sx
Split, 37

39 ~EXIST(z):[z in y & z in sx]
Split, 37

Apply definition of sx

40 y in sx <=> y in z & y=x
U Spec, 11

41 [y in sx => y in z & y=x] & [y in z & y=x => y in sx]
Iff-And, 40

42 y in sx => y in z & y=x
Split, 41

43 y in z & y=x
Detach, 42, 38

44 y in z
Split, 43

45 y=x
Split, 43

46 x in y
Substitute, 45, 4

47 x in y & x in sx
Join, 46, 34

48 EXIST(z):[z in y & z in sx]
E Gen, 47

Obtain the contradiction:

49 EXIST(z):[z in y & z in sx]
& ~EXIST(z):[z in y & z in sx]
Join, 48, 39

As Required:

50 ~EXIST(x):x in x
Conclusion, 4

51 ~~ALL(x):~x in x
Quant, 50

52 ALL(x):~x in x
Rem DNeg, 51

[Mostowski Collapse]

Ok, do you accept this as a theorem of ZFC then:

ALL(x):~x in x

You didn't use your Set(), so I guess you only used FOL+ZFC.

[Dan Christensen]

On Saturday, November 13, 2021 at 7:32:47 AM UTC-5, Mostowski Collapse wrote:
> Ok, do you accept this as a theorem of ZFC then:
>
> ALL(x):~x in x
>

Yes.

> You didn't use your Set(), so I guess you only used FOL+ZFC.

In this proof, I don't use the axioms of set theory built into DC Proof. I use only those axioms of set theory from ZFC introduced in the first 3 lines here. I make use of the rules of logic that are built into DC Proof (a simplified version of FOL).

[Mostowski Collapse]

Ok, you accept ALL(x):~x in x as a ZFC theorem.

Do you also accept the axiom schema of separation
from ZFC, like here with any formula φ as here:

https://en.wikipedia.org/wiki/Axiom_schema_of_specification

And you would NOT call this wonky, when I make use of
this axiom schema in DC proof to produce a proof

from ZFC in DC proof?

[Dan Christensen]

On Saturday, November 13, 2021 at 11:17:11 AM UTC-5, Mostowski Collapse wrote:
> Ok, you accept ALL(x):~x in x as a ZFC theorem.
>

Yes. It follows from the Regularity, Pairing and Specification Axioms in ZFC.

DC Proof does not have a built-in Regularity Axiom. Whether or not a particular set is element of itself never seems to come up most math textbooks, so why hard-code this bizarre looking axiom that most likely will never be used and will only confuse users? As you can see here, determined users can manually introduce their own version of Regularity.

> Do you also accept the axiom schema of separation
> from ZFC, like here with any formula φ as here:
>
> https://en.wikipedia.org/wiki/Axiom_schema_of_specification
>
> And you would NOT call this wonky, when I make use of
> this axiom schema in DC proof to produce a proof
>
> from ZFC in DC proof?

Not sure. Can you give an example of what you have in mind? You have to be very careful when introducing an axiom. The only requirement for an axiom introduced by the user is that it be syntactically correct. There is no checking for consistency with other axioms. It can even be self-contradictory, e.g. P & ~P.

[Mostowski Collapse]

Like here in your own proof:

Dan Christensen schrieb am Freitag, 12. November 2021 um 19:25:19 UTC+1:
> My formal proof in DC Proof format (comments inserted):

> [...]

> Instance of the ZF Axiom Schema of Specification:
> 3 ALL(a):ALL(b):EXIST(c):ALL(d):[d in c <=> d in a & d=b]
> Axiom

> [...]
https://groups.google.com/g/sci.logic/c/nzEj1sXJCUg/m/3aelYPfyDQAJ

You used for the formula φ the formula d=b.
In ZFC any formula φ is allowed.
You can make any instance of the Axiom Schema of Specification.
This is why its called a "Schema".

So you accept this axiom schema, yes or no?

[Mostowski Collapse]

The only restriction is, B ∉ free(φ), so that it gets "predicative":

"So B does not occur free in φ.
In the formal language of set theory, the axiom schema is:
∀w1, …, wn∀A∃B∀x(x ∈ B ⇔ [x ∈ A ∧ φ (x, w1, … , wn, A)])"
https://en.wikipedia.org/wiki/Axiom_schema_of_specification#Statement

Do you accept this axiom schema being part if ZFC?

[Mostowski Collapse]

"impredicativity" would lead to an inconsistent ZFC:

"If we omit the requirement that 𝑦 not occur in 𝜑, we can derive
a contradiction, as notzfaus shows (contradicting zfauscl).
However, as axsep2 shows, we can eliminate the restriction
that 𝑧 not occur in 𝜑."
http://us.metamath.org/mpeuni/axsep.html

[Dan Christensen]

On Saturday, November 13, 2021 at 1:48:09 PM UTC-5, Mostowski Collapse wrote:
> Like here in your own proof:
> Dan Christensen schrieb am Freitag, 12. November 2021 um 19:25:19 UTC+1:
> > My formal proof in DC Proof format (comments inserted):
> > [...]
> > Instance of the ZF Axiom Schema of Specification:
> > 3 ALL(a):ALL(b):EXIST(c):ALL(d):[d in c <=> d in a & d=b]
> > Axiom
> > [...]
> https://groups.google.com/g/sci.logic/c/nzEj1sXJCUg/m/3aelYPfyDQAJ
>
> You used for the formula φ the formula d=b.

The only restriction in this case is that c is not free in this formula.

> In ZFC any formula φ is allowed.
> You can make any instance of the Axiom Schema of Specification.
> This is why its called a "Schema".
>
> So you accept this axiom schema, yes or no?

The Subset Axiom in DC Proof can only be applied to free variables that have been declared to be a set. In ZFC, where everything is a set, the Specification Axiom Schema (for subsets) can be applied to any free variable. So there may be some incompatibilities. I'm not sure. It's not something I have given much thought to with ZFC being so rarely used in most math textbooks.

[Mostowski Collapse]

I wasn't asking about DC Proof. I was asking:

"Do you accept the axiom schema of separation from
ZFC, like you used it in your ALL(x):~x in x proof?"

Whats your answer exactly? You write " I'm not sure." So you don't know?
Why did you use it then? You are not sure whether it belongs to ZFC or not?

[Mostowski Collapse]

By accept I mean whether you recognize it as belonging
to ZFC, and whether you wouldn't call it wonky using it.
Unless you think ZFC itself is wonky, well, ... what then?

[Dan Christensen]

On Saturday, November 13, 2021 at 4:36:38 PM UTC-5, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Samstag, 13. November 2021 um 22:31:07 UTC+1:
> > I wasn't asking about DC Proof. I was asking:
> >
> > "Do you accept the axiom schema of separation from
> > ZFC, like you used it in your ALL(x):~x in x proof?"
> >

> By accept I mean whether you recognize it as belonging

> to ZFC.

Of course it belongs to ZFC. What is your point?

[Mostowski Collapse]

So if I use axiom schema of separation, in your tool DC Proof,
by manually mentioning an instance of the axiom schema,
I am not using some wonky stuff. I am only using ZFC, right?

[Dan Christensen]

On Saturday, November 13, 2021 at 7:24:37 PM UTC-5, Mostowski Collapse wrote:

> > > > "Do you accept the axiom schema of separation from
> > > > ZFC, like you used it in your ALL(x):~x in x proof?"
> > > >
> > > By accept I mean whether you recognize it as belonging
> > > to ZFC.
> >
> > Of course it belongs to ZFC. What is your point?

> So if I use axiom schema of separation, in your tool DC Proof,
> by manually mentioning an instance of the axiom schema,
> I am not using some wonky stuff. I am only using ZFC, right?

I don't foresee any theoretical limitations. A non-empty universe would be guaranteed by an axiom for the empty set as in some presentations of ZFC. It's not something that interests me, but give it a try and report back. :^)

[Dan Christensen]

On Saturday, November 13, 2021 at 8:07:12 PM UTC-5, Dan Christensen wrote:
> On Saturday, November 13, 2021 at 7:24:37 PM UTC-5, Mostowski Collapse wrote:
>
> > > > > "Do you accept the axiom schema of separation from
> > > > > ZFC, like you used it in your ALL(x):~x in x proof?"
> > > > >
> > > > By accept I mean whether you recognize it as belonging
> > > > to ZFC.
> > >
> > > Of course it belongs to ZFC. What is your point?
> > So if I use axiom schema of separation, in your tool DC Proof,
> > by manually mentioning an instance of the axiom schema,
> > I am not using some wonky stuff. I am only using ZFC, right?
> I don't foresee any theoretical limitations. A non-empty universe would be guaranteed by an axiom for the empty set as in some presentations of ZFC. It's not something that interests me, but give it a try and report back. :^)

You might start by constructing the set of natural numbers. Then the addition function, showing that it is associative, commutative and cancelable.

[Mostowski Collapse]

Why should I do such a thing? Bootsrapping N?
The proof ALL(x):~(x in x) was also not some
proof of this sort. Why do you think people

do only such things like Boostrapping N, Q, etc..
with ZFC? Do you think I asked the ZFC sep
axiom because I want to Boostrap something?

I nowhere said that.

> On Saturday, November 13, 2021 at 8:07:12 PM UTC-5, Dan Christensen
wrote:

[Dan Christensen]

On Saturday, November 13, 2021 at 8:47:03 PM UTC-5, Mostowski Collapse wrote:
> Why should I do such a thing? Bootsrapping N?
> The proof ALL(x):~(x in x) was also not some
> proof of this sort. Why do you think people
>
> do only such things like Boostrapping N, Q, etc..
> with ZFC?
>

For fun? For the challenge of it? Maybe just to see how wonky ZFC really is? I think you would come away from such an exercise with an appreciation of DC Proof as an educational aid.
>
OK, so you don't want to do this exercise. Oh, well...

[Mostowski Collapse]

Its relative trivial to do N in ZFC, you don't need any new axioms.
Since ZFC has the infinite axiom. Zermelo showed in his
1908 paper how to do it.

To the best of my knowledge DC Proof has no infinity axiom,
so unlike ZFC, DC Proof cannot intrinsicly do N, i.e. without new
axioms. Unlike ZFC which can do it.

So why would one call ZFC wonky?

[Mostowski Collapse]

You are confused if you think ZFC works like you
worked with DC Proof so far. In ZFC there is no
preamble, and now we have additionally this

and that Peano axioms. In ZFC you can prove Peano
axioms from within ZFC via some encoding, i.e.
interpret. You can even prove Peano consistent.

ZFC is stronger than Peano.

"One way to compare them is to measure their arithmetical
consequences. Both 𝖹𝖥𝖢 and 𝖯𝖠 can express statements
on arithmetic, and we can see that 𝖹𝖥𝖢 proves more
arithmetic statements than 𝖯𝖠. (𝖢𝗈𝗇(𝖯𝖠) is an example.)"
https://math.stackexchange.com/a/3818226/4414

[Mostowski Collapse]

The easiest encoding are von Neuman ordinals. You
then have the following:

0 = {}
1 = {{}}
2 = {{{}}, {}}
Etc..

Von Neuman ordinals are funny since if n and m such
ordinals, then n in m is logically equivalent to n < m.
You can then identify N with the ordinal ω. But I am

pretty sure you confuse ZFC with Landau's was sind
die Zahlen. You don't need ZFC for that. ZFC is not
made to proof associative, commutative and cancelable,

thats nonsense. Its not made for natural number
algebra. It has a different story and application area.
It helps a lot for example in analysis.

https://en.wikipedia.org/wiki/Ordinal_number

[Dan Christensen]

On Saturday, November 13, 2021 at 9:15:18 PM UTC-5, Mostowski Collapse wrote:
> Its relative trivial to do N in ZFC, you don't need any new axioms.
> Since ZFC has the infinite axiom. Zermelo showed in his
> 1908 paper how to do it.
>

Then it SHOULD be easy to do it in DC Proof. (Hee, hee!)

>
> To the best of my knowledge DC Proof has no infinity axiom,
>

Correct. I usually start by simply introducing Peano's 5 Axioms. But if you are determined to derive them, you can start with an arbitrary Dedekind infinite set X and select the required subset N and prove that Peano's 5 Axioms hold on it.

>
>
> so unlike ZFC, DC Proof cannot intrinsicly do N, i.e. without new
> axioms. Unlike ZFC which can do it.
>
> So why would one call ZFC wonky?
>

I think you will find out if you try to do the exercises I suggested.

[Mostowski Collapse]

What exercise? The exercise you suggested is a typical Peano
exercise, which isn't very interesting for ZFC. In ZFC you
would rather prove things like Zorns lemma etc..

LoL

[Mostowski Collapse]

Its a little idiotic to do exercises with the infinite ordinal ω,
when ZFC offers much more infinities. It doesn't get less
moronic if one looks at add ⊆ ω^3.

Most of ZFC "exercises" explore the whole structure of a
ZFC universum, which goes beyond the ordinal ω, or
relations over the ordinal ω.

This paper mentions 124+30 set theory problems:

Automated ZFC Theorem Proving with E
https://arxiv.org/abs/1902.00818

[Mostowski Collapse]

But I dont know the exact where about of these 124+30
set theory problem. Looks like this is only an excerpt?

https://github.com/hesterj/E-ZFC2/tree/zfc/EXAMPLE_PROBLEMS

[Dan Christensen]

On Sunday, November 14, 2021 at 3:44:23 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 14. November 2021 um 04:14:48 UTC+1:
> > On Saturday, November 13, 2021 at 9:15:18 PM UTC-5, Mostowski Collapse wrote:
> > > Its relative trivial to do N in ZFC, you don't need any new axioms.
> > > Since ZFC has the infinite axiom. Zermelo showed in his
> > > 1908 paper how to do it.
> > >
> > Then it SHOULD be easy to do it in DC Proof. (Hee, hee!)
> > >
> > > To the best of my knowledge DC Proof has no infinity axiom,
> > >
> > Correct. I usually start by simply introducing Peano's 5 Axioms. But if you are determined to derive them, you can start with an arbitrary Dedekind infinite set X and select the required subset N and prove that Peano's 5 Axioms hold on it.
> > >
> > >
> > > so unlike ZFC, DC Proof cannot intrinsicly do N, i.e. without new
> > > axioms. Unlike ZFC which can do it.
> > >
> > > So why would one call ZFC wonky?
> > >
> > I think you will find out if you try to do the exercises I suggested.
> > >

> What exercise? The exercise you suggested is a typical Peano
> exercise, which isn't very interesting for ZFC. In ZFC you
> would rather prove things like Zorns lemma etc..
>

Better that you should start with the basics. Again, you might start by constructing (i.e. proving the existence of) the set of natural numbers N. Then try constructing the addition function, and showing that it is unique in N, associative, commutative and cancelable.

If that didn't exhaust you, you might then try Zorn's Lemma. Better still, try Cantor-Burnstein-Schroeder. Here is my DC Proof version of the proof to get you started: http://dcproof.com/CBS.htm I think you will find it challenging. Enjoy.

[Mostowski Collapse]

Why would you need the proof? You are awfully bad in
statistical induction (scientific hypothesis from data).

You see one purple flower, and then you think all flowers
are purple. So your NOT PURPLE is anyway always empty.

LMAO!

Dan Christensen schrieb am Samstag, 30. Oktober 2021 um 23:31:23 UTC+2:
> I wrote the attached proof in response to a discussion at Quora. Here I show that, in set theory, there exists no set of all those things that are NOT PURPLE.

[Mostowski Collapse]

Are you afraid of the dark like WM? Ha Ha, for Dan-O-Matik
mathematics and logic is the same as what for WM the
natural numbers are. For WM the natural numbers are

the identifiable natural numbers, the natural numbers he
has seen in his lifetime, basically his hands and toes.
Same for Dan-O-Matik, he made some Peano and other

proofs with DC Proof and now he thinks he has covered
much of mathematics.

LoL

[Mostowski Collapse]

Dan-O-Matiks motto for mathematics:

https://www.youtube.com/watch?v=O4irXQhgMqg
I see a red door
And I want it painted black
No colors anymore
I want them to turn black
I see the girls walk by
Dressed in their summer clothes
I have to turn my head
Until my darkness goes
I see a line of cars
And they're all painted black
With flowers and my love
Both never to come back
I've seen people turn their heads
And quickly look away
Like a newborn baby
It just happens everyday
I look inside myself
And see my heart is black
I see my red door
I must have it painted black
Maybe then, I'll fade away
And not have to face the facts
It's not easy facing up
When your whole world is black
No more will my green sea
Go turn a deeper blue
I could not foresee this thing
Happening to you
If I look hard enough
Into the setting sun
My love will laugh with me
Before the morning comes
I see a red door
And I want it painted black
No colors anymore
I want them to turn black
I see the girls walk by
Dressed in their summer clothes
I have to turn my head
Until my darkness goes
I wanna see it painted
Painted black
Black as night
Black as coal
I wanna see the sun
Blotted out from the sky
I wanna see it painted, painted, painted
Painted black, yeah

[Dan Christensen]

On Sunday, November 14, 2021 at 6:09:08 PM UTC-5, Mostowski Collapse wrote:

> > Better that you should start with the basics. Again, you might start by constructing (i.e. proving the existence of) the set of natural numbers N.
>

> Why would you need the proof?
>

If you CAN'T prove the existence of N from the ZFC axioms, that's... OK. No shame in that. It is kind of tricky.
>
But it DOES require a proof, Jan Burse. Sorry.

[Mostowski Collapse]

Try proving proposition 2.20 (goes back to Cantor 1897):
The proposition is in Basic Set Theory, Levy.

"If <A, <> is a well ordered class and B is subclass of A, then
<B, <> is isomorphic to <A,<> or to a section of <A, <>."
https://www.amazon.de/dp/0486420795

Thats a quite interesting proposition, you can of couse also
make examples from N. Like for example the even Even numbers
are a subset of N, and <N,<> and <Even,<> are indeeded isomorphic.

Cantor was not interested in the balant infinite of N. He was
interested in the transfinite. So proving existence of N is not
very interesting, since it is not a transfinite extercise,

transfinite is every thing above N.

[Mostowski Collapse]

I demanded a proof in ZFC, for some definition def of
omega, that we can show existence:

- EXIST(omega):Def(omega)

And not only:

- ALL(omega):[Def(omega) => Peano(omega)]

What I never asked was whether we can also show uniqueness:

- ALL(omega1):ALL(omega2):[Def(omega1) & Def(omega2) => omega1 = omega2]

It seems the axiom of foundation becomes now necessary!
And Halmos might really have botched it.

At least this take, an Agda and HoTT paper, has it that in AFA
there might be multiple omega's, which isn't good:

See Example 1 on Page 8
Non-wellfounded sets in homotopy type theory
Håkon Robbestad Gylterud, Elisabeth Bonnevier
6 Jul 2020
https://arxiv.org/abs/2001.06696

[Fritz Feldhase]

On Sunday, November 21, 2021 at 2:44:34 AM UTC+1, Mostowski Collapse wrote:

> I demanded a proof in ZFC [...]

Fair enough.

I'm just rereading Halmos' book. I'll post a proof in due time.

[Mostowski Collapse]

Now I have doubts that the Agda example applies. Usually
proving uniqueness is not that much an issue, if omega
is defined, in def, as a least element.

It then usually follows that omega is unique. Since there
cannot be two different least elements. The construction
usually doesn't need axiom of regularity, definining

the least element, in the form an infinite intersection
is already possible with classes, and needs only a little
axioms of ZFC. Right? But Agda does a lot of things

different from Zermelos 1908 original idea. For example they
don't use the simple definition of an inductive set:

ind(S) <=> 0 e S /\ forall x (x e S => x u {x} e S)

They rather use already the stronger definition, that all
elements have a predecessor:

ind_comp(S) <=> 0 e S /\ forall x (x e S => x u {x} e S)
/\ forall x(x e S /\ x <> 0 => exist y(y e S /\ y u {y} = x))

Usually such things are proved later, and the Zermelo 1908
axiom of infinity doesn't require it either.

[Fritz Feldhase]

On Sunday, November 21, 2021 at 12:35:17 PM UTC+1, Mostowski Collapse wrote:

> Now I have doubts that the Agda example applies. Usually
> proving uniqueness is not that much an issue, if omega
> is defined, in def, as a least element.
>
> It then usually follows that omega is unique. Since there
> cannot be two different least elements. The construction
> usually doesn't need axiom of regularity, definining
> the least element, in the form an infinite intersection
> is already possible with classes, and needs only a little
> axioms of ZFC. Right?

That's exactly Halmos' approach in his book.

> But Agda does a lot of things different [...]. For example they

> don't use the simple definition of an inductive set:
>
> ind(S) <=> 0 e S /\ forall x (x e S => x u {x} e S)

Certainly not Halmos' fault, is it?

> They rather use already the stronger definition, that all
> elements have a predecessor:
>
> ind_comp(S) <=> 0 e S /\ forall x (x e S => x u {x} e S)
> /\ forall x(x e S /\ x <> 0 => exist y(y e S /\ y u {y} = x))

I see. Well, Halmos' approach uses

ind(S) <=> 0 e S /\ forall x (x e S => x u {x} e S) .

> Usually such things are proved later, and the Zermelo 1908 axiom of infinity doesn't require it either.

Halmos is primarilly concerned with the proofs of the "Peano Axioms". After establishing these "Axioms" (as theorems), we might very well proceed like Edmund Landau in his book "Foundations of Analysis".

"There is very little preparatory knowledge required in Landau’s Foundations of Analysis. Starting from the Peano axioms, the whole number system theory from natural number to complex number are given in turn. In this book, there are several important theorems proved: minimum principle, Archimedes theorem for rational number, the existence of irrational number, and Dedekind fundamental theorem, which embodies the completeness of real number. The whole process is natural and beautiful. Many theories can be developed based on this."

After all, this work has already been completely formalized:

"There already exists some formalizations of Landau’s “Foundations of Analysis”. de Bruijn designed earliest proof checker Automath, and his student van Benthem Jutting has completed the formalization of Landau’s “Foundations of Analysis” in AUT-QE. This work was significant early progress in formal mathematics. Moreover, Brown has given a particular faithful reproduction of a signature corresponding to the Automath version of Landau’s book. Guidi has encoded this specification into the formal language “λδ”, and, furthermore, presents an implemented procedure producing a representation of the “Foundations of Analysis” in Coq."

Moroever:

"...we developed the formal system of real number theory strictly following Landau’s “Foundations of Analysis”. Moreover, the every step of the formalizations has been verified in Coq, which can check and enrich the many details in traditional proofs. Additionally, we have presented some new methods to optimize proof steps. All the formal proofs are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. Furthermore, there are several important theory, such as calculus, general topology, and complex analysis, can be constructed based on the “Foundations of Analysis” formal system."

Source: https://www.mdpi.com/2227-7390/9/1/38/htm

[Julio Di Egidio]

On Monday, 22 November 2021 at 15:49:05 UTC+1, Fritz Feldhase wrote:
> On Sunday, November 21, 2021 at 12:35:17 PM UTC+1, Mostowski Collapse wrote:
>
> > Now I have doubts that the Agda example applies. Usually
> > proving uniqueness is not that much an issue, if omega
> > is defined, in def, as a least element.
> >
> > It then usually follows that omega is unique. Since there
> > cannot be two different least elements. The construction
> > usually doesn't need axiom of regularity, definining
> > the least element, in the form an infinite intersection
> > is already possible with classes, and needs only a little
> > axioms of ZFC. Right?
>
> That's exactly Halmos' approach in his book.

How do we/Halmos know there is a least element?

Julio

[Fritz Feldhase]

It seems to me that MC was talking about successor sets here. There is exactly one minimal succesor set (namely omega).

See my other post.

[Julio Di Egidio]

Which post is that, there are countless posts in this thread alone...?

Maybe it's trivial, but I'd expect some proof of existence of a least element or something...

Julio

[Mostowski Collapse]

Not necessarely. For example in Prolog you can define:

nat(z).
nat(s(X)) :- nat(X).

Now the result of this query:

?- X = s(X), nat(X).

Depends on the occurs check. The recursion with X = s(X)
when a circular terms are allowed, leads to an infinite decend.
Logic itself is too defensible to make a decision here.

You would need to make a formalization, where this decision
is made by the formalization, so that an infinite decend would
lead to what? That the element is excluded? That

the element is included? What if the model of ZFC is such
that it happens that the element is always in a set, so that
the minimum would also include it?

For a set X, P(X) is a lattice. But this here:

P'(X) = { x u {x0} | x subset X }

Is also a lattice. So I guess you need an axiom of regularity
to make sure that the unwanted elements x0 do not appear,
or otherwise another axiom that assures that

your models have enough diversity.