Re: The MetaMathematical Theorem that Almost Was


Charlie-Boo wrote:
> george wrote:
>
> > ZF has the rather weird property that EVERYthing that exists
> > is a set, automagically.
>
> I could never see that.

Well, it's not provable, but it's still true.
Everything either has elements or it doesn't.
Ax[ Ey[yex] V ~Ez[zex] ]
is a theorem because it's valid because
the thing inside the universal quantifier is a tautology.
For every thing, if it doesn't have elements, then by
extensionality, it is equal to the empty set, so it is a set.
If it does have elements, then it must be a set because
sets by definition are the things that elements are elements OF.

This is just a property of this formalism; sets are all and only
the things it WANTS to talk about -- they're just all there is.
There are plenty of reasonable theories with more things in
them than sets, but ZF, BEING A *SET* theory, doesn't happen
to concern itself with any of them.

> Doesn't that produce an infinite chain, which
> is prohibited (for any non-empty set)?

It's prohibited for the empty set as well.
It's prohibited by the axiom of foundation.
But no, "everything"'s being a set does NOT
produce an infinite "descending" chain. Inifnite "ascending"
chains are of course what ZF is all about.

> I also don't agree that {x|x ~e x} is a set,
> but argue that it IS something (or another.)

You are not the first person to argue this.
In any case, regardless of what you argue,
in ZFC, this "thing" simply does NOT exist;
whatever kind of "thing" it may be, it is NOT
the kind of thing that exists as an object of the domain
of a model. In other set theories (other than ZF), it
might be called a class, but using the {}'s is a little
problematic in that case.

> > If you are in FOL withOUT equality then it is not yet clear to me
> > how you proof-theoretically exploit the non-emptiness of the
> > domain, maybe Ex[xexV~xex]. THEN you have a set.
>
> Or simple use false (as above): {x|~false} or {x|true}.

In ZF, you CAN'T do that.
You CAN'T do {x|whatever}. That is known as "unrestricted"
comprehension and leads to "naive" set theory. In ZF, you have
to use the axiom of Separation instead which looks like
{x|xey/\ whatever(x)}, where y is some pre-existing other set.
That is why I had to keep beating MoeBlee over the head that
you are NOT "proving the existence" of the empty set when you
replace "whatever" by "false" in this schema.
It bears further stressing that "false" is NOT part of the LANGUAGE
of ZF, and that in order to actually do this, in addition to needing
something that IS part of the language, you need something that
at least CAN be thought of as a function of x (you need a unary
first-order formula-schema). "False", even when it is available, is
normally
NOT that (it is 0-ary or constant, NOT unary), so it does MATTER that
we phrase this some other way.

.

Relevant Pages