Re: Triclass Theory

On Mar 20, 11:50 am, "MoeBlee" <jazzm...@xxxxxxxxxxx> wrote:
On Mar 20, 8:47 am, "zuhair" <zaljo...@xxxxxxxxx> wrote:

the theorum existing in you mind is

If F is a formula in which c is not free, then all closures of

AxeV E!yeV [F -> Ab(~b=T -> EcAy(yec <-> Exeb F))]
are theorems

No, that is not what I have in mind.

While the actual theorum is:

If F is a formula in which c is not free, then all closures of

[AxeV E!yeV F]-> Ab(~b=T -> EcAy(yec <-> Exeb F))

are theorems

Right, that is what I have in mind and always have had in mind.





and for my side I think it is essential to wight the formula F as
F(x,y) so the theorum should be

If F is a formula in which c is not free, then all closures of

[AxeV E!yeV F(x,y)]
-> Ab(~b=T -> EcAy(yec <-> Exeb F(x,y))).

are theorems

by I still think for the sake of clarity it is more complete to wright
it as:

If F is a formula in two variables in which c is not free, then all
closures of

[AxeV E!yeV(F(x,y))] -> Ab(~b=T -> EcAz(zec <-> Exeb(F(x,z))).

are theorems

I think this is the clearest presentation of this axiom.

Changing the 'y' to 'z' is just alphabetic variance of bound
variables. It doesn't matter. It just shifts the problem over again.
It's equivalent to what you started with.

you see since we have ~b=T and xeb, then x is a set i.e xeV

Right. We asssume ~b=T and we assume Exeb F(x z) then existentially
instantiate to xeb & F(x z), so we have xeV. No problem. And what we
need to prove is zec.

now since F holds for x,

What we have now is E!zeV F(x z) in addition to what I just mentioned.
And we still need to prove zec.

since there should exist a unique zeV for
each xeV
such that F(x,z),

Do you mean, for each xeV, there is a unique z such that zeV and F(x
z)? Right. But notice that this "z" can NOT be assumed to the same "z"
such that we are trying to prove zec. Why is that? Because the "z" we
are trying to prove zec is an ARBITRARY z of which we may suppose
nothing at all except F(x z), while the "z" in E!zeV F(x z) is a
SPECIFIC "z" with a specific property of being BOTH in V and F(x z).
In terms of instantiation we have two choices: Either supppose for an
arbitrary 'z' that F(x z), in which case any subsequent existential
instantation from an Ez quantifier has to go to a NEW variable instead
of z, e.g. 'jeV & F(x j)', and we do not get to use zeV. Or we
instantiate the Ez quantifier to z, so that we have zeV & F(x z) but
then when we suppose for an arbitrary z that 'xeb & F(x z)' we must
use a NEW variable so that we have 'xeb & F(x j)', and we do not get
to use 'xeb & F(x z)'.

If that is not clear to you, then it will be once you study that logic
book that you're waiting for.

then c would be the set of all these unique values z
for x e b.

No, that's what your'e trying to PROVE. You can't just assume that it
follows here. You have to PROVE EcAz(zec <-> Exeb F(x z)).

but for every b:~b=T we already have EcAz(zec <->( Exeb(F(x,z)) &
zeV)).
we have that from global comprehension when letting
P<-> Exeb(F(x,z)).

lets call this theorum schema of Collection.

For instance let me wright the theorum of large replacement again.

If F is a formula in two variables in which c is not free, then all
closures of

[AxeV E!yeV(F(x,y))] -> Ab(~b=T -> EcAz(zec <-> Exeb(F(x,z))).

are theorems

from the left hand we already have AxAz((F(x,z) & xeV) -> zeV) .

what I want to say is exactly the following:

[AxeV E!yeV(F(x,y))] -> AxAz((F(x,z) & xeV) -> zeV) .

Now since we have ~b=T, then Ax(xeb -> xeV). Definition of sets.
then we have Exeb(F(x,z) -> zeV)
so [Exeb(F(x,z))] -> (Exeb(F(x,z)) & zeV)
then from theorum of collection we have:

EcAz(zec <-> Exeb(F(x,z))).

theorum schema proved.


and since zeV, then c is a class, because all of what is in
it are sets.

You should note that E!zeV for each x, because this is the condition
on the left.

I don't see any problem really.

There might be a way to prove this schema, but what you have so far is
not a proof.

MoeBlee- Hide quoted text -

- Show quoted text -


.

Relevant Pages

  • Re: Triclass Theory
    ... And we still need to prove zec. ... of z, e.g. 'jeV & F', and we do not get to use zeV. ... lets call this theorum schema of Collection. ... For instance let me wright the theorum of large replacement again. ...
    (sci.logic)
  • Re: Triclass Theory
    ... Fand this y is in V, isn't it that what uniqueness mean here. ... What uniqueness means here is that for every xeV there is one and only ... But you don't HAVE zeV. ... But obviouselly I think I should restate this theorum schema. ...
    (sci.logic)
  • Re: Triclass Theory
    ... need to prove that zeV follows from Exeb Fand E!zeV F. ... the "z" you are trying to prove zec cannot be assumed to be the SAME ... then this mean that for every xeV and Fthen z should be in V. ... explaining yet again why they are incorrect. ...
    (sci.logic)
  • Re: Triclass Theory
    ... Fand this y is in V, isn't it that what uniqueness mean here. ... What uniqueness means here is that for every xeV there is one and only ... But you don't HAVE zeV. ... conjunct zeV. ...
    (sci.logic)
  • Re: Triclass Theory
    ... need to prove that zeV follows from Exeb Fand E!zeV F. ... the "z" you are trying to prove zec cannot be assumed to be the SAME ... from the left hand we already have AxAz& xeV) -> zeV). ... explaining yet again why they are incorrect. ...
    (sci.logic)