Prev: A=Z-Regularity.
Next: A reformulation of ZF-Reg.
From: zuhair on 18 Jun 2010 17:31
A is the set of all sentences(entailed from FOL with identity "=" and
membership "e") by the following non logical axioms:

(1) Comprehension: for n=0,1,2,3,...; if phi(y,w1,...,wn)
is a formula in which y,w1,...,wn *are* its sole free variables
and in which x is not free,then

Aw1...wn Ar As E!x Ay
( y e x <-> (( y c r \/ y c s ) /\ phi(y,w1,...,wn)))

were c is the subset relation defined in the standard manner.

(2) Union: Ar Ex Ayer(ycx)

were c is the subset relation defined in the standard manner.

(3) Infinity: as in Z.

/ Theory definition finished.

I: The proof that A->Z-Reg.

(1) Theorem schema of unique separation:

for n=1,2,3,...., if pi(y,w1,...,wn) is a formula were at most
y,w1,...,wn occur free, and having w2,...,wn free in it,
and in which x is not free, then

Aw1...wn E!x Ay (y e x <-> (y e w1 & pi(y,w1,...,wn))).

Proof:

Let s=r in the comprehension schema,
then for the same specifications
in *comprehension* we get:

Aw1...wn Ar E!x Ay
(y e x <-> (y c r /\ phi(y,w1,...,wn)))

Let phi(y,w1,...,wn)<-> [y e w1 /\ pi(y,w1,...,wn)]

were pi(y,w1,...,wn) is a formula were at most
y,w1,...,wn occur free, and having w2,...,wn free in it, and
in which x is not free.

substitute in the above formula

and we get:

for n=1,2,3,.....

Aw1...wn Ar E!x Ay
( y e x <-> (y c r /\ y e w1 /\ pi(y,w1,...,wn)))

From union we have

Aw1 Ew* Ayew1(ycw*)

now w* is not unique, but we know that for every w1,
at least one w* must exist such that all members of w1
are subsets of w*.

Now instantiate any one of the w* sets for r in the
above formula, we get:

Aw1...wn E!x Ay
(y e x <-> (y c w* /\ y e w1 /\ pi(y,w1,...,wn)))

Now since every member of w1 is subset of w*
(by definition of w* sets). then we have

(y c w* /\ y e w1) -> y e w1

thus the above formula would be reduced to:

Aw1...wn E!x Ay
(y e x <-> (y e w1 /\ pi(y,w1,...,wn)))

QED.

This implies:

Aw1...wn E!x Ay
(y e x <-> (y e w1 /\ pi(y,w1,...,wn)))

which is separation in Z set theory.

(2) Extensionality: Ax Ay (Az(zex<->zey) ->x=y).

Proof: let n=1, and pi(y,w1)<->yew1,
substitute in unique separation,
then we have:

Aw1E!x Ay (y e x <-> y e w1)

QED.

(3) Pairing: Ar As Ex ( r e x /\ s e x ).

Proof: from comprehension with n=0 ,we have:

Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ phi(y)))

let phi(y)<-> y=y

then:

Ar As E!x Ay (y e x <-> (y c r \/ y c s))

since Ar As ( r c r /\ s c s )

then r and s are members of x

QED

(4)Power:Ar E!x Ay (y e x <-> y c r)

Proof: The formula in comprehension schema reads:

Aw1...wn Ar As E!x Ay (y e x <-> (( y c r \/ y c s ) /\
phi(y,w1,...,wn)))

Let r=s, and let n=0, then we'll have:

Ar E!x Ay (y e x <-> ( y c r /\ phi(y)))

Let phi(y)<->y=y

thus we'll end up with

Ar E!x Ay (y e x <-> y c r)

QED.

From the above we proved that: Extensionality, Separation,Pairing
and Power are theorems of
A. On the other hand Union and Infinity are axioms of A.

Thus Z-Reg is a subtheory of A.

So: A->Z-Reg.

QED

II: The proof that Z-Reg. -> A

In Z-Reg we have:

(y c r \/ y c s) <-> y e P(r) U P(s).

were P stands for 'power-set'

Now in Z-Reg. P(r) U P(s) is a set , thus the formula in Comprehension
schema of A would mount to:

Ar As E!x Ay (y e x <-> (y e P(r) U P(s) /\ phi))

which is a sub-theory of Z-Reg, since it is an instance
of separation in Z-Reg-Infinity.

So the comprehension schema in A is provable from Z-Reg.-Infinity.

Of course the proof of this schema in Z-Reg.-Infinity requires all of:
Extensionality,Separation,Pairing,Union and Power.

Now, Union and Infinity in A are already axioms of Z-Reg.

thus, A is a subtheory of Z-Reg.

So: Z-Reg. -> A

QED

III: The proof that A=Z-Reg.

Proof: I and II.

QED

As one can see A is nothing but a reformulation of Z-Reg.,however it
is a shorter way to understand Z-Reg.
compared to the standard way which use six axiom schemes.

Zuhair





 | 
Pages: 1
Prev: A=Z-Regularity.
Next: A reformulation of ZF-Reg.