Prev: A Reformulation of Z-Reg.
Next: Question for Aatu Koskensilta
From: zuhair on 16 Jun 2010 15:32
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

Moe Blee in a previous post asked me to show the following:

For ARBITRARY formula Phi (except we know x not free in Phi):

all closures of

ExAy(yex <-> (yez & Phi)).

/

I say the above statement is actually equivalent to the unique
separation schema mentioned above.

Zuhair
From: MoeBlee on 16 Jun 2010 17:15
On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote:

> Moe Blee in a previous post asked me to show the following:
>
> For ARBITRARY formula Phi (except we know x not free in Phi):
>
> all closures of
>
> ExAy(yex <-> (yez & Phi)).
>
> /
>
> I say the above statement is actually equivalent to the unique
> separation schema mentioned above.

I haven't looked over your new formulations, but last night I did
figure out a way to formulate your compression schema so that it and
your union axiom entail the separation(with built in extensionality)
schema, while the separation schema (with built in extensionality)
entails your compression schema.

However, then it can't be the case that your compression schema, union
schema, and infinity entail pairing and power set (did I understand
correctly that you claim they do entail pairing and power set?), for
then they would not be independent in Z set theory, though it has been
proven that they are independent in Z set theory.

MoeBlee

From: zuhair on 16 Jun 2010 17:50
On Jun 16, 4:15 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote:
>
> > Moe Blee in a previous post asked me to show the following:
>
> > For ARBITRARY formula Phi (except we know x not free in Phi):
>
> > all closures of
>
> > ExAy(yex <-> (yez & Phi)).
>
> > /
>
> > I say the above statement is actually equivalent to the unique
> > separation schema mentioned above.
>
> I haven't looked over your new formulations, but last night I did
> figure out a way to formulate your compression schema so that it and
> your union axiom entail the separation(with built in extensionality)
> schema, while the separation schema (with built in extensionality)
> entails your compression schema.
>
> However, then it can't be the case that your compression schema, union
> schema, and infinity entail pairing and power set (did I understand
> correctly that you claim they do entail pairing and power set?), for
> then they would not be independent in Z set theory, though it has been
> proven that they are independent in Z set theory.
>
> MoeBlee

Well I don't know what is your formulation yet. But I think we need to
look at what I wrote here. Since there might be a mistake then.

Anyhow let see the proof of pairing and power.

(1)The proof of power:

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

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

It is clear that x is the power-set of r. Thus power is proved.

(2)The proof of pairing:

from comprehension with n=2 ,we have:

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

let phi(y,w1,w2)<->(y=w1 \/ y=w2)

then:

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

let phi(y,w1,w2)<-> (y=w1 \/ y=w2)

then:

Aw1 Aw2 Ar As E!x Ay (y e x <-> ((y c r \/ y c s) /\ (y=w1 \/
y=w2)))

take r=w1, s=w2

then:

Aw1 Aw2 E!x Ay (y e x <-> ((y c w1 \/ y c w2) /\ (y=w1 \/ y=w2)))

which is reduced to:

Aw1 Aw2 E!x Ay (y e x <-> (y=w1 \/ y=w2))

which is pairing.

I don't know what you meant about the issue with the independence of
these axioms in Z, and how that can be affected if they spring from
the same comprehension and union axioms. To me I don't see that this
would affect their
independence at all.


Zuhair




From: zuhair on 16 Jun 2010 17:53
On Jun 16, 4:15 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote:
>
> > Moe Blee in a previous post asked me to show the following:
>
> > For ARBITRARY formula Phi (except we know x not free in Phi):
>
> > all closures of
>
> > ExAy(yex <-> (yez & Phi)).
>
> > /
>
> > I say the above statement is actually equivalent to the unique
> > separation schema mentioned above.
>
> I haven't looked over your new formulations, but last night I did
> figure out a way to formulate your compression schema so that it and
> your union axiom entail the separation(with built in extensionality)
> schema, while the separation schema (with built in extensionality)
> entails your compression schema.
>
> However, then it can't be the case that your compression schema, union
> schema, and infinity entail pairing and power set (did I understand
> correctly that you claim they do entail pairing and power set?), for
> then they would not be independent in Z set theory, though it has been
> proven that they are independent in Z set theory.
>
> MoeBlee

Well I don't know what is your formulation yet. But I think we need to
look at what I wrote here. Since there might be a mistake then.

Anyhow let see the proof of pairing and power.

(1)The proof of power:

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

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

It is clear that x is the power-set of r. Thus power is proved.

(2)The proof of pairing:

from comprehension with n=2 ,we have:

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

let phi(y,w1,w2)<->(y=w1 \/ y=w2)

then:

Aw1 Aw2 Ar As
E!x Ay (y e x <-> ((y c r \/ y c s) /\ (y=w1 \/ y=w2)))

take r=w1, s=w2

then:

Aw1 Aw2 E!x Ay (y e x <-> ((y c w1 \/ y c w2) /\ (y=w1 \/ y=w2)))

which is reduced to:

Aw1 Aw2 E!x Ay (y e x <-> (y=w1 \/ y=w2))

which is pairing.

I don't know what you meant about the issue with the independence of
these axioms in Z, and how that can be affected if they spring from
comprehension and union. To me I don't see that this would affect
their
independence at all.

Zuhair
From: zuhair on 16 Jun 2010 17:58
On Jun 16, 4:15 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 16, 2:32 pm, zuhair <zaljo...(a)gmail.com> wrote:
>
> > Moe Blee in a previous post asked me to show the following:
>
> > For ARBITRARY formula Phi (except we know x not free in Phi):
>
> > all closures of
>
> > ExAy(yex <-> (yez & Phi)).
>
> > /
>
> > I say the above statement is actually equivalent to the unique
> > separation schema mentioned above.
>
> I haven't looked over your new formulations, but last night I did
> figure out a way to formulate your compression schema so that it and
> your union axiom entail the separation(with built in extensionality)
> schema, while the separation schema (with built in extensionality)
> entails your compression schema.
>
> However, then it can't be the case that your compression schema, union
> schema, and infinity entail pairing and power set (did I understand
> correctly that you claim they do entail pairing and power set?), for
> then they would not be independent in Z set theory, though it has been
> proven that they are independent in Z set theory.
>
> MoeBlee

Well I don't know what is your formulation yet. But I think we need to
look at what I wrote here. Since there might be a mistake then.

Anyhow let see the proof of pairing and power.

(1)The proof of power:

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

Now 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.

(2)The proof of pairing:

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

thus pairing proved! (axiom of pairing is
Ar As Ex ( r e x /\ s e x ).

QED


I don't know what you meant about the issue with the independence of
these axioms in Z, and how that can be affected if they spring from
comprehension and union. To me I don't see that this would affect
their independence at all.

Zuhair
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: A Reformulation of Z-Reg.
Next: Question for Aatu Koskensilta