It would be seen that through the following four concepts of
restrictions on formulas defining sets:
1. Non trans-passing.
2. Non Redundancy.
3. Exclusion of big classes.
4. Restrictions on parameters and constants.
then perhaps we can reconcile these two opposing approaches.
Lets begin with the MK approach
set is to be defined as a class that is a member of a class
Define(set): x is a set <-> Ey ( x e y )
The letter "M" was given by Cantor to denote a set, and it was used
in the original writing of Ackermann so I will use it here
so Mx <-> x is a set.
Now we come to the class comprehension schema which is:
If phi is a formula in which at least y is free, and in which x is
not free, then all closures of
Exist x for all y ( y e x <-> My phi )
are axioms.
Now from this we can build a class for any arbitrary formula phi, so
we can proceed an use the class abstraction { | }, and define the
class builder {y|phi}
Define: x ={y|phi} <-> for all y ( y e x <-> My phi )
Now lets come to the condition of Exclusion of big classes, or
actually formula leading to big classes or more precisely proper
classes.
Before that one can from the above schema prove the existence of a
transitive closure for any class defined as below:
Define: y transitional of x <->
( x subclass y & y is transitive )
Define: z=Tc(x) <->
( z transitional of x &
for all y ( y transitional of x -> z subclass y ) )
"Tc" stands for "Transitive Closure".
Now lets examine formula satisfying the following condition:
for all x (Mx -> Exist y (phi(y) & x subclass Tc(y)))
I shall call this formula the primary exclusion formula.
However I simpler version of this principal of exclusion would be the
following:
for all x (Mx -> Exist y (phi(y) & x e y))
Now it is clear that such a formula phi would not define a set, i.e.
the class {y|phi} would not be a set, since every set x is a subclass
of the transitive closure of some set that satisfy phi, then it is
clear that the class of all sets that satisfy phi will be as big as
the class of all sets.
Lets Add the condition of Foundation to this theory.
Then the formulas: y=y , y is well founded , ~y e y ,
y is a singleton, y is of cardinality n>0 , etc.... all are formulas
that satisfy the above condition.
So this was the third of conditions imposed to select formulas
defining sets(see above: condition of Exclusion of big classes)
However this is not enough, since the formula
"x is ordinal" doesn't satisfy the primary exclusion formula, and it
is clear that "x is ordinal" cannot define a set, this takes us to
the second of the conditions imposed on formulas in defining sets.
The condition of "Non Trans-passing".
A trans-passing formula is a formula when used to define a well
founded class, then it will not be confined to the members of the
class.
For example y=y, the class {y|y=y} if obviously identical to itself!
so y=y is a trans-passing formula.
So all trans-passing formulas should be Excluded from the formulas
that define sets.
Trans-passing can be qualified formally in the following manner:
phi is a trans-passing formula if
For all c ((c={y|phi} -> Exist z (c subclass z & phi(z)))
phi would be a non trans-passing formula if
For all c,z ((c={y|phi} & c subclass z) -> ~ phi(z))
However the problem with this is "Redundancy", which would lead to
the condition of the same class being defined by a trans-passing
formula, would be defined by another non trans-passing formula!
Example: take the class {y|y is ordinal} which is of course the class
of all ordinals that are sets.
Now the formula y is ordinal is trans-passing formula because we have
the class {y|y is ordinal} itself as an ordinal!
however one can take the formula "y is ordinal & y is a set"
so we'll have the class {y|y is ordinal & y is a set}
now this class is not an ordinal that is a set, nor any class z such
that it is subclass of it would be an ordinal that is a set.
So the formula " y is ordinal & y is a set " is a non trans-passing
formula,But both formulas "y is ordinal", and
"y is ordinal & y is a set" define
the same class! a dilemma.
However the formula "y is ordinal & y is a set" is actually
a redundant formula, and what I mean by that is that it is a longer
formula that is basically saying nothing other than what the formula
y is ordinal say.
Formally speaking on can define Redundant formula as a formula in
which a proper subformula of it is equivalent to it.
So if we have the formula phi and we have Q1,....,Qm as proper
subformulas of phi and we have the following:
~ ( ~for all y ( phi <-> Q1),....., ~for all y ( phi <-> Qm) )
then phi is said to be a redundant formula, because this would mean
that one of the proper subformulas of phi is equivalent to phi, which
makes phi a redundant formula.
So for the condition of non trans-passing to work in defining sets,
one should have the condition of Non redundancy with it.
However their remain another kind of redundancy, that is what I
call, the basic or rather primary redundancy, which is the redundancy
of the formula "x is a set" itself.
To explain that, we know that in this theory every class is defined
after formulas conjuncted to the formula " x is a set ", so the class
builder notation {y|phi} mean the class of all y such that " y is a
set" and " y is phi" , however we didn't right the class notation
as {y|Myphi} because My is trivially present in all classes.
so phi here is the additional formula to the basic(primary) formula
which is " y is a set ".
Now if we take the formula phi itself to be "y is a set" then
although phi would not be redundant but the class notation itself
would be! it would be something like {y|MyMy} which is clearly
redundant.
So it would be better to define the condition of redundancy taking
this point in mind as below:
the formula phi would be redundant if
~ ( ~for all y ( My phi <-> Q1),....., ~for all y ( My phi <-> Qm) )
were Q1,...,Qm are "subformula" of phi including phi itself.
So the condition of non redundancy would be the negation of the
condition above.
However the problem do not stop here, still we can have formulas
defined in two way giving conflicting result, and this can be done
though parameters that are not sets, i.e parameters that are proper
classes.
Take the class {y| y is ordinal} which is the class of all ordinals
that are sets, now with Extensionality this would be unique,
so lets denoted it by the constant D
Now we can have the formula "y e D" now this formula is not
redundant, not trans-passing, and not general for exclude it by
condition 3, but yet it cannot define a set.
So we need to exclude all parameters in phi and all constants used in
phi from being standing form proper classes.
To sum all of that we wright the following axiom schema:
If phi is a formula in which at least y is free, and in which c is
not free, with parameters x1,...,xn, and Q1,...,Qm are all subformulas
of phi, then all closures of:
c={y|phi} &
Mx1,...,Mxn &
for all c,z ((c={y|phi} & c subclass z) -> ~ phi(z)) &
~for all x ( Mx ->Exist y (phi(y) & x e y)) &
~for all y (Myphi<->Q1)&...,&~for all y (Myphi<->Qm)
-> Mc
are axioms.
Now we come to the last of all axioms, which is the one which asserts
the existence of at least two sets. This is a consequence of the
condition of non redundancy, the formula ~y=y when substituted in the
above schema we need to prove that
~for all y (Myphi<->~y=y)
which is impossible using the above axiom schemes.
Axiom of two sets: Exist(many) x : Mx.
So in summary NST2 is defined below:
NST2: is the set of all sentences entailed (from FOL with identity
and e) by the following non logical axioms:
1. Extensionality: for all z ( z e y <-> z e x) -> x=y
2. Foundation: Exist y y e x -> Exist y (y e x & y disjoint x)
3. Classes: If phi is a formula in which at least y is free, and in
which x is not free, then all closures of
Exist x for all y ( y e x <-> My phi )
are axioms.
4. Sets:If phi is a formula in which at least y is free, and in which
c is not free, with parameters x1,...,xn, and Q1,...,Qm are all
subformulas of phi, then all closures of:
c={y|phi} &
Mx1,...,Mxn &
for all c,z ((c={y|phi} & c subclass z) -> ~ phi(z)) &
~for all x ( Mx ->Exist y (phi(y) & x e y)) &
~for all y (Myphi<->Q1)&...,&~for all y (Myphi<->Qm)
-> Mc
are axioms.
5. Two sets: Exist(many) x : Mx.
Theory definition finished/
This theory is simpler that NST, but yet I cannot be sure of its
consistency.
Last word is that it is better to define a subformula of phi as a
formula having at least y free, and all parameters in it are
parameters in phi.
Regards
Zuhair
are axioms.
However w can overcome that by defining redundant formulas and
excluding them.
So if we have the formula phi and we have Q1,....,Qm as proper
subformulas of phi and we have the following:
~(~for all y (Myphi<->MyQ1),...,~for all y(Myphi<->MyQm))
then phi is a trans-passing formula.
So for the condition of non trans-passing to work in defining sets,
one should have the condition of Non redundancy with it.
However their remain another kind of redundancy, that is what I
call, the basic or rather primary redundancy, which is the redundancy
of the formula "x is a set" itself.
To explain that, we know that in this theory every class is defined
after formulas conjuncted to the formula " x is a set ", so the class
builder notation {y|phi} mean the class of all y such that " y is a
set" and " y is phi" , however we didn't right the class notation
as {y|Myphi} because My is trivially present in all classes.
so phi here is the additional formula to the basic(primary) formula
which is " y is a set ".
Now if we take the formula phi itself to be "y is a set" then
although phi would not be redundant but the class notation itself
would be! it would be something like {y|MyMy} which is clearly
redundant.
so the formula "y is a set" or any formula equivalent to it should be
excluded
So in addition to the above definition of redundancy we should add the
following condition
~ for all y (phi<->My)
However the problem do not stop here, still we can have formulas
defined in two way giving conflicting result, and this can be done
though parameters that are not sets, i.e parameters that are proper
classes.
Take the class {y| y is ordinal} which is the class of all ordinals
that are sets, now with Extensionality this would be unique,
so lets denoted it by the constant D
Now we can have the formula "y e D" now this formula is not
redundant, not trans-passing, and not general for exclude it by
condition 3, but yet it cannot define a set.
So we need to exclude all parameters in phi and all constants used in
phi from being standing form proper classes.
To sum all of that we wright the following axiom schema:
If phi is a formula in which at least y is free, and in which c is
not free, with parameters x1,...,xn, and Q1,...,Qm are all proper
subformulas of phi, then all closures of:
c={y|phi} &
Mx1,...,Mxn &
for all c,z ((c={y|phi} & c subclass z) -> ~ phi(z)) &
~for all x ( Mx ->Exist y (phi(y) & x e y)) &
~(~for all y (Myphi<->MyQ1),...,~for all y(Myphi<->MyQm))
& ~ for all y (phi<->My)
-> Mc
are axioms.
Now we come to the last of all axioms, which is the one which asserts
the existence of at least two sets. This is a consequence of the
condition of non redundancy, the formula ~y=y when substituted in the
above schema we need to prove that
~for all y (Myphi<->~y=y)
which is impossible using the above axiom schemes.
Axiom of two sets: Exist(many) x : Mx.
So in summary NST2 is defined below:
NST2: is the set of all sentences entailed (from FOL with identity
and e) by the following non logical axioms:
1. Extensionality: for all z ( z e y <-> z e x) -> x=y
2. Foundation: Exist y y e x -> Exist y (y e x & y disjoint x)
3. Classes: If phi is a formula in which at least y is free, and in
which x is not free, then all closures of
Exist x for all y ( y e x <-> My phi )
are axioms.
4. Sets:If phi is a formula in which at least y is free, and in which
c is not free, with parameters x1,...,xn, and Q1,...,Qm are all
proper subformulas of phi, then all closures of:
c={y|phi} &
Mx1,...,Mxn &
for all c,z ((c={y|phi} & c subclass z) -> ~ phi(z)) &
~for all x ( Mx ->Exist y (phi(y) & x e y)) &
~(~for all y (Myphi<->MyQ1),...,~for all y(Myphi<->MyQm))
& ~ for all y (phi<->My)
-> Mc
are axioms.
5. Two sets: Exist(many) x : Mx.
Theory definition finished/
This theory is simpler that NST, but yet I cannot be sure of its
consistency.
Last word is that it is better to define a proper subformula of phi as
a proper sub-formula having at least y free, and all parameters in it
The second message is the correct one, the first message at the head
post is not correct as regards to the definition of redundancy and
subformula and set comprehension.
Zuhair
the condition ~ for all y (phi<->My) can ommitted!
And actually one can reduce axiom 4 to the following:
Exist x : Mx.
Which is simpler and very trivial axiom.
Zuhair
Oops the formula should be
c={y|phi} &
Mx1,...,Mxn &
for all c,z ((c={y|phi} & c subclass z) -> ~ phi(z)) &
~for all x ( Mx ->Exist y (phi(y) & x e y)) &
~for all y (Myphi<->MyQ1),...,~for all y(Myphi<->MyQm)
& ~ for all y (phi<->My)
-> Mc
>