A Reformulation of Z-Reg.2 [Math]

Prev: 24 is gorgeous
Next: MGW: Retiring from the fray

From: zuhair on 15 Jun 2010 20:42

Theory A is the set of all sentences(entailed from FOL with identity
and membership) 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,...,1n *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.

(2) Union: Ar Ex Ayer(ycx)

were c is the subset relation.

(3) Infinity: as in Z.

/

Theorem schema of unique separation:

for n=1,2,3,...., if pi(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 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 in which y,w1,...,wn *are* its sole
free variables and in which x is not free.

substitute in the above formula and we get:

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)))

Theorem schema of unique separation proved.

Zuhair

From: zuhair on 15 Jun 2010 21:39

Theory A is the set of all sentences(entailed from FOL with identity
and membership) 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.

(2) Union: Ar Ex Ayer(ycx)

were c is the subset relation.

(3) Infinity: as in Z.

/

Theorem schema of unique separation:

for n=1,2,3,...., if pi(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 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 in which y,w1,...,wn *are* its sole
free variables and in which x is not free.

substitute in the above formula and we get:

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)))

Theorem schema of unique separation proved.

Zuhair

From: zuhair on 15 Jun 2010 21:49

On Jun 15, 8:39 pm, zuhair <zaljo...(a)gmail.com> wrote:
> Theory A is the set of all sentences(entailed from FOL with identity
> and membership) 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.
>
> (2) Union: Ar Ex Ayer(ycx)
>
> were c is the subset relation.
>
> (3) Infinity: as in Z.
>
> /
>
> Theorem schema of unique separation:
>
> for n=1,2,3,...., if pi(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 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 in which y,w1,...,wn *are* its sole
> free variables and in which x is not free.
>
> substitute in the above formula and we get:
>
> 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)))
>
> Theorem schema of unique separation proved.
>
> Zuhair

Addendum:

Extensionality, pairing, power, separation are all theorems of this
theory, and thus theory A=Z-Reg.

Zuhair

From: zuhair on 15 Jun 2010 21:51

From: zuhair on 16 Jun 2010 05:39

On Jun 15, 8:39 pm, zuhair <zaljo...(a)gmail.com> wrote:
> Theory A is the set of all sentences(entailed from FOL with identity
> and membership) 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.
>
> (2) Union: Ar Ex Ayer(ycx)
>
> were c is the subset relation.
>
> (3) Infinity: as in Z.
>
> /
>
> Theorem schema of unique separation:
>
> for n=1,2,3,...., if pi(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 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 in which y,w1,...,wn *are* its sole
> free variables and in which x is not free.
>
> substitute in the above formula and we get:
>
> 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)))
>
> Theorem schema of unique separation proved.
>
> Zuhair

Addendum:

Extensionality,Pairing, Power, Separation all are theorems of this
theory, and thus Z-Reg is a sub-theory of Theory A.
On the other hand: Comprehension in Theory A is a theorem of Z-Reg;
therefore Theory A is a sub-theory of Z-Reg, so

Theory A=Z-Reg.

| Next | Last
Pages: 1 2 3 4 5
Prev: 24 is gorgeous
Next: MGW: Retiring from the fray