Re: Axiom of Pairing, Scheme of Replacement from others

Please pardon the top posting here. I want to make it clear from the outset that I value MB's contributions to this discussion, and I hope he will continue.

MoeBlee wrote:

Stephen J. Herschkorn wrote:


MoeBlee wrote:



Stephen J. Herschkorn wrote:




According to Wikipedia
(http://en.wikipedia.org/wiki/Axiom_of_separation), "the axiom of
separation follows from the axiom of replacement together with the axiom
of empty set."



First, I take formal Z set theories to use classical first order logic
with identity (or, just as well, we can do without identity theory and
without special identity semantics by defining '=' from 'e', though
this has no bearing on the present matter of discussion). Such logic
includes such rules as universal instantiation, universal
generalization, existential instantiation, and existential
generalization, either as primitive or as derived rules, as found in
many textbooks and as is STANDARD first order predicate logic.

Notation:

'e' (read as 'epsilon') is the usual membership symbol.

'P[t|x]' stands for replacing the term t for all free occurrences of
the variable x in the formula P, as a rigorous definition is provided
by definition by recursion.

'v occurs free in P' has a rigorous definition provided by definition
by recursion.

't is free for x in P' has a rigorous definition provided by definition
by recursion.

'Q is a closure of P' is defined: Q is a sentence that is the result of
adding a finite (possibly 0) number of universal quantifiers to the
front of P.

Here 'v', 'w', 'y', 'z', and 'b' are variables of the object language
(they are distinct); and P (read as 'phi') and Q (read as 'chi') are
meta-variables.



There was no need to go to the level of detail presented above (except perhaps for the "[ | ]" notation). In fact, while I appreciate the effort MB went to, presenting a proof in such low-level detail obscures the issue at hand.

Axiom schema of replacement
For all P,
if P is a formula and
v does not occur free in P and
w does not occur free in P and
v is free for y in P and
w is free for y in P and
b does not occur free in P, the all closures of

AuezAvAw(P[v|y] & P[w|y]) -> v=w) -> EbAy(yeb <-> EuezP)

are axioms.



That is not how I understand repleacement. Your hypothesis has uniqueness but not existence. Should it not be

Auez (Ey P & (AvAw(P[v|y] & P[w|y]) -> v=w)) -> EbAy(yeb <-> EuezP)
?

Or, in notation I find a little bit clearer, let f be a formula wherein w is not free. We have the universal closure of

[Ay (y in x -> E!z f)] -> Ew Az [z in w <-> Ey (y in x & f)]


Axiom schema of separation:

For all Q,
if Q is a formula and
b does not occur free in Q, then all closures of

EbAy(yeb <-> (yez & P))

are axioms.

/

Proof of separation from replacement (in tedious detail):

Let Q be a formula such that b does not occur free in Q.

Let P be the formula Q & u=y.

An instance of the axiom schema of replacement:

AuezAvAw((Q & u=y)[v|y] & (Q & u=y)[w|y]) -> v=w) -> EbAy(yeb <->
Euez(Q & u=y)), which is:

AuezAvAw(Q[v|y] & u=v & Q[w|y] & u=w) -> v=w) -> EbAy(yeb <-> Euez(Q &
u=y)).

The antecedent is a theorem of identity theory, since u=v & u=w implies
v=w.

So, by sentential logic, EbAy(yeb <-> Euez(Q & u=y)).



Here is where the omission in your statement of the replacement scheme wreaks havoc.

By existential instantiation, let Ay(yeb <-> Euez(Q & u=y)).

Suppose yeb.

So, by universal instantiation and sentential logic, Euez(Q & u=y).

By existential instantiation, let uez & Q & u=y.

So, by identity theory, yez & Q.

So, by sentential logic, yeb -> (yez & Q).

So, by universal generalization Ay(yeb -> (yez & Q)).

Suppose yez & Q.

So, by existential generalization and identity theory, Eu(uez & Q &
u=y), which is

Euez(Q & u=y).

So, by universal instantiation and sentential logic, yeb.

So, by universal generalization and sentential logic, Ay((yez & Q) ->
yeb).

So Ay(yeb -> (yez & Q)) & Ay((yez & Q) -> yeb).

So, by obvious predicate and sentential logic (details available upon
request), Ay(yeb <-> (yez & Q)).

By existential generalization, EbAy(yeb <-> yez & Q).

/

Proof of ExAy ~yex from the axiom schema of separation:



This part was unncessary.

Let Q be the formula yey & ~ yey.

An instance of the axiom schema of separation:

EbAy(yeb <-> (yez & (yey & ~yey))).

By existential instantiation let, Ay(yeb <-> (yez & (yey & ~yey))).

Suppose yeb.

So, by universal instantiation and sentential logic, yey & ~yey.

So, by sentential logic, ~yeb.

So, by universal generalization, Ay ~yeb.

So, by existential generalization, ExAy ~yex.

/

Proof of E!xAy ~yex from the axiom schema of separation and the axiom
of extensionality:

We already have ExAy ~yex.

By existential instantiation, let Ay ~yex.

Suppose Ay ~yec.

So, by universal instantiation, sentential logic, and universal
generalization, Ay(yex <-> yec).

So, by the axiom of extensionality, x=c.

So, by definition of '!', we have E!xAy ~yex.

/



The first Wikipedia page cited gives a brief, explicit proof of
separation from replacement, given we are assured the existence of an
empty set. The page also desribes in detail why the existence of an
empty set is required.



Among the relevent pages (if I recall correctly, one you linked to),
there is an auxilliary discussion (found under the tab 'discussion')
about the page itself. There you will see that other people have
corrected the author of the page. His defense is that he is not
assuming the non-empty domain principle. And that is the crux of the
problem with his presentation.


I have looked at that tab, and I find no such discussion. Do you have a more precise URL?

Without even appealing to the semantic
principle of non-empty domain, the SYNTACTICAL rules of first order
logic allow the derivation I gave. Yes, I recognize that the syntactic
rules are meant to work with a semantics that presuposes non-empty
domains, but the question here was the PROVABILITY of the replacement
from separation and the provability of the empty set from separation.
And the proofs I gave are correct (adjusting for any possible typos).


No. See above.

Now, in informal set theory that does not use first order logic so
strictly so that one may not appeal to all the rules of formal first
order logic, one might argue that we can't assume the non-empty domain
principle. But my proofs are in formal set theory using ONLY STANDARD
rules of first order logic. And using ONLY STANDARD rules of first
order logic, as I showed, separation is derivable from replacement and
empty set from separation and uniqueness of empty set from
extensionality. Granted, some authors use an empty set axiom or
introduce an explict assumption that there exists at least one set or
similar assumptions. And that may make the theory more intuitive,
especially for readers who are not so versed in the details of the
rules of standard first order logic. However, for standard formal Z set
theory, for the pure question of proving one thing from another, such
extra assumptions and empty set axiom are not necessary, as I have
shown, and as other authors also show.



MB's repetitions demonstrate how easy it is to claim something is not
true. However, without explicit presentation of a proof which does not
rely on the existence of the empty sets, such claims are not credible in
this case. MB, can you present such a proof?



I very much respect your knowledge of set theory and mathematics, which
is far greater than mine. So I am sorry to say that I find your above
note may insinuate that I am somehow intractable by not providing a
proof. For any mathematical claim I make, I will provide a proof or
refer to one in the literature, or I will admit it is a claim whose
proof is known in the literature but that I haven't read or fully
understood myself. Here, previously, a proof was not asked for, and my
purpose at that point in my posting was simply to state, for the
record, that it is incorrect that a proof of separation from
replacement requires an empty set axiom or that separation alone
doesn't prove the existence of an empty set, especially as there are
plenty of places in the literature and in basic textbooks where one can
find such proofs without the empty set, and also as it is easy enough
for one to make such a proof for oneself. IF I had been called upon for
a proof, I would have given one or pointed to one. In the future,
please give me the benefit of that consideration as I would for you.



Let us review here. I paraprhase.

SJH 1: Replacement + existence of empty set implies separation.
MB 1: You do not need the empty set for such a proof.
SJH 2: Well, here are reputable sites which explicitly show why you do.
MB 2: It's not true. It's not. It's not. It's not. [See that post - it really reads that way.]
SJH 3: Just saying that is not enough. Prove it.
MB 3: Here's a [faulty] proof. You never said you wanted one before. Are you calling me stupid?

In this forum, or in any rational discussion of mathematics (and other subjects), if one is going to claim something discussed elsewhere is not true, then one should give a justification of the claim. Such a justification can be either an explicit proof (or outline of one) or a citation. There is no need to wait for an invitation. And your detection of insinuations are your own inference.

That much said, I repeat what I said at the beginning of this post.

I value MB's contributions to this discussion, and I hope he will continue.


Respectfully,

--
Stephen J. Herschkorn sjherschko@xxxxxxxxxxxx
Math Tutor on the Internet and in Central New Jersey and Manhattan

.

Relevant Pages