From: zuhair on
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
On Jun 15, 7:03 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> (1) You mean 'x' does not occur free in Pi or in Phi, right?
>
> (2) When you say "a formula that has y w1,...,wn as its sole free
> variables", you mean that AT MOST y, w1, ... wn occur free while it
> might be that none or only some of them occur free, right?
>
> (3) There's too much clutter now in all our back and forth. Please
> write a post all by itself in which you purport to show:
>
> For ARBITRARY formula Phi (except we know x not free in Phi):
>
> all closures of
>
> ExAy(yex <-> (yez & Phi)).
>
> Leave out all the old quotes conversation. Please just let me see your
> argument in a post by itself.
>
> MoeBlee

You'll see all the answers in a separate topic at:

http://groups.google.com.jm/group/sci.logic/browse_thread/thread/d672cf805e3d242a?hl=en

From: zuhair on
On Jun 15, 7:03 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> (1) You mean 'x' does not occur free in Pi or in Phi, right?

Yes, of course, this goes without saying really.
>
> (2) When you say "a formula that has y w1,...,wn as its sole free
> variables", you mean that AT MOST y, w1, ... wn occur free while it
> might be that none or only some of them occur free, right?

NO, not right.

When I say a formula that has y,w1,...,wn as its sole free variables,
it means what is said, it means that it has n+1 free variables in it,
and those free variables are y, w1,...,wn, that what it means.

it is a schema really, so when n=0 then ONLY y is free in that
formula, when n=1, then y and w1 are the only free variables, etc....
>
> (3) There's too much clutter now in all our back and forth. Please
> write a post all by itself in which you purport to show:
>
> For ARBITRARY formula Phi (except we know x not free in Phi):
>
> all closures of
>
> ExAy(yex <-> (yez & Phi)).
>
> Leave out all the old quotes conversation. Please just let me see your
> argument in a post by itself.
>
> MoeBlee

I did that see my previous reply to you above.

Zuhair