Re: Axiom of Pairing

apoorv wrote:
The Axiom of Pairing is:
If x and y are sets then there exists a set containing both of them.

'contain' is sometimes used for subsets, while the pairing axiom does
not say that there is a set that has x and y as subsets.

The pairing axiom is:

AbAcExAy(yex <-> (y=b v y=c)).

Less formally, the pairing axiom is that

{b c} is a set.

This is equivalent to asserting both:
A)If x and y are finite sets, then there exists a set containing both
of them.
B) if x and y are two sets, at least one of which is infinite, then
there is a set containing both of them.

I would put that as:

pairing axiom
<->
AbAc(b and c are both finite -> ExAy(yex <-> (y=b v y=c))) &
AbAc(b is infinite v c is infinite) -> ExAy(yex <-> (y=b v y=c)))

If 'infinite' is defined as 'not finite', then the above is a logical
truth.

The question is, whether B can be deduced from A and the other axioms
of ZFC less powerset, or is B an independent assertion?

I take it you mean also less the pairing axiom. So you want to know
whether we can derive (with only extensionality, replacement, union,
and choice):

AbAc(b and c are both finite -> ExAy(yex <-> (y=b v y=c)))
->
AbAc(b is infinite v c is infinite) -> ExAy(yex <-> (y=b v y=c)))

The answer is yes. And it's trivial (I didn't even need to set up all
that clarification).

The pairing axiom is derivable straight from the axiom schema of
replacement alone. And...

AbAc(b is infinite v c is infinite) -> ExAy(yex <-> (y=b v y=c)))

....is derivable from the pairing axiom.

MoeBlee

.