Re: Some basic set theory questions

On Jul 8, 1:34 am, David Bernier <david...@xxxxxxxxxxxx> wrote:
Stephen J. Herschkorn wrote:
Dave Seaman wrote:

The usual statement of the axiom of infinity is Ex(0 in x and ...),
thus presuming that the empty set exists before the AoI can even be
stated.  Therefore, I don't see how we can claim that the existence of
the emptyset "follows from" the AoI in its usual form.

I think the AoI can be formulated as "there exists an inductive set",
meaning "there exists a nonempty set that is closed under the successor
operation".  This establishes that at least one set exists without
mentioning the empty set.

"0 in x"  is just short for  "Ey in x [Az ~(z in y)]."  It follows by
basic logic that  Ey [Az ~(z in y)],  which is precisely the statement
of the existence of an empty set.  (Extensionality implies that the
empty set is unique.)

I'd be pleased for any enlightenment about what appears below.

Without AoI, I'm not sure that the axiom of pairing, or say the axiom of
separation, will prove that a set exists.

In a formal Z set theory in which the only non-logical symbol is 'e',
and with a definition of 'x is a set' as 'Ey xey', there is a proof
that there exists a unique empty set, using only the axiom schema of
separation, the axiom of extensionality, and the pairing axiom. This
is not a matter of debate. It's a plain finite fact about sequences of
formulas.

So say without AoI, how might it be possible to show:

(1) Ex: Ay:  y e x  <==> ( y =/= y)   , expanded:

(2) Ex: Ay:  y e x  <===> ( Az: (z e y) <===> not(z e y) ).

I already gave a variation of that. I'll give it for your specific
formulation:

First, I take it you don't need me to prove

~Az(zey <-> ~zey).

That is, we'll take that as already proven.

AzExAy(yex <-> (yez & ~yez)) ... instance of separation
ExAy(yex <-> (yez & ~yez)) ... universal instantiation
Let Ay(yex <-> (yez & ~yez)) ... letting 'x' be the x mentioned above
(since 'x' not previously free)
yex <-> (yez & ~yez) ... universal instantiation
~yex ... sentential logic
yex <-> Az(zey <-> ~zey) ... sentential logic and our already proven
theorem ~Az(zey <-> ~zey).
Ay(yex <-> Az(zey <-> ~zey)) ... universal instantiation (since y was
not free previous to instantiation to it)
ExAy(yex <-> Az(zey <-> ~zey) ... existential generalization (since
the conditions on the variables are satisfied)

Note: The use of 'z' in the formula P ("~zey") is not disallowed, only
'x' in P is disallowed. But if one is squeemish about 'z' used that
way, then just use any other contradiction or negation of a theorem
you like adjusted suitably, blah blah blah...

If the universe of discourse U (or V ... ) has nothing,

Nope. The official logic for formal Z set theory is plain first order
logic. Any universe of discourse for a structure for the language is
non-empty.

Of course, if we used a logic that were built otherwise, we might not
have this guarantee of a nonvoid universe of discourse.

So I'd like to get opinions/ideas about the question:
Is (1) provable in   ZF - AoI  ?

Since, by definition, ZF is a theory in first order logic, the answer
is yes.

But, of course, if you prefer to ponder the axioms of ZF with some
other logic, then your results will be different.

At the moment, what I think is that the Axiom of Separation
looks promising for proving (1), but how to apply Separation
if we don't already "know" that a set exists?

We don't need to know a set exists. Rather we work in a logic that
ensures that some object exists. Then upon a suitable definition of
'is a set' we also get that the unique empty object is a set. Or, many
(probably most) authors speak more informally in such contexts so that
they speak of everything as a set, and of 'classes' in general
(including proper classes) as a certain kind of figure of speech; or,
they present not Z set theory but rather NB or NBG or MK or even ZF
(with possible urelements) where it is not the case that everything is
a set.

MoeBlee
.

Relevant Pages

  • Re: Some basic set theory questions
    ... thus presuming that the empty set exists before the AoI can even be ... the emptyset "follows from" the AoI in its usual form. ... of the existence of an empty set. ... Without AoI, I'm not sure that the axiom of pairing, or say the axiom of ...
    (sci.math)
  • Re: Kuratowski Ordered Pair
    ... It is defining a certain type of order with respect to the element ... Then with the axiom of extensionality, ... need the empty set axiom. ... You did talk about ZFC set theory, about set theory without axiom of ...
    (sci.math)
  • Re: Axiom of Pairing, Scheme of Replacement from others
    ... separation follows from the axiom of replacement together with the axiom ... Your hypothesis has uniqueness but not existence. ... Proof of separation from replacement: ... empty set is required. ...
    (sci.math)
  • Re: Some basic set theory questions
    ... The usual statement of the axiom of infinity is Ex, ... presuming that the empty set exists before the AoI can even be stated. ...
    (sci.math)
  • Re: Axiom of Pairing, Scheme of Replacement from others
    ... separation follows from the axiom of replacement together with the axiom ... empty set is required. ...
    (sci.math)