Prev: Yet Another SD Rodrian Prediction True: Gravity is NOT an attractive force between bodies
Next: A Reformulation of Z-Reg.2
From: zuhair on 15 Jun 2010 20:41 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 20:48 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 16 Jun 2010 15:28
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 |