FOM: Revised Axioms for a possible solution to Professor Shavrukov's GC problem

[Matt Insall]

The theory I mentioned in a previous posting to try to solve Professor
Shavrukov's problem should, I think, be modified as follows, because it is a
first order theory of ``collections'', some of which are ``classes'' and
some of which are ``sets'', and some of which are neither.  Roughly, I
intend to axiomatize a theory for structures in which ``collections'' obey
ZF-type axioms, ``classes'' are members of ``collections'' and obey GNB-type
axioms, and ``sets'' are members of ``classes'' and obey ZF(C)-type axioms,
all without an axiom of foundation.  I am trying to make these axioms so
they form an independent set, but there may be some redundancies.

1.  Let L be the first-order language obtained from the language for ZF by
adding a pair of unary predicates, ``class'' and ``set''.

3.  Let T be the theory of L with the following axioms:



First, there is the usual axiom of extensionality.
EXT:
(forall x)(forall y)(forall z){[(z is in x)iff(z is in y)] implies x=y}


Now, a separation axiom schema for ``collections''.
SEP(phi):
(forall x_1,...,x_n)(forall z)(thereis y)[{(forall x)[(x is in y) iff {(x is
in z) & phi(x_1,...,x_n,x)]}& {(y is a set) iff (z is a set)}]

We could have an ``empty collection axiom'' here, but it is redundant, for
it follows from the later ``axiom of infinity'' and the above ``axiom schema
of separation''.

Now, we say what the ``classes'' are.  In fact, they are just all of the
``collections'' of sets.  We also stipulate here that there is at least one
set.
SET/CLASS
(forall x){[x is a class] iff (forall y)[(y is in x) implies (y is a set)]}
(thereis x)[x is a set]


Pairing is done as usual, with the stipulation that pair-collections of sets
are sets.  From the definition of ``class'' up above, it will follow that
any pair-collection of non-sets will not be a class.  (For example, the
collection {A,S}, where S is the class of all sets and A is the class of all
abelian groups defined on sets, is not a class.)

PAIR:
(forall x,y)(thereis z)(forall w)[{[w is in z] iff [(w=x) or (w=y)]}&{[z is
a set] iff [(x is a set)&(y is a set)]}]


In the union axiom, we obtain arbitrary unions of collections.  The union is
a set precisely when the collection to which the ``union operator'' is
applied is itself a set.  The union is a class precisely when the collection
to which the ``union operator'' is applied is itself a class.


UNION:
(forall x)(thereis y)(forall z)[{[z is in y] iff (thereis w)[(z is in w)&(w
is in x)]}&{(y is a class) iff (x is a class)}&{(y is a set) iff (x is a
set)}]


The power axioms provide for the existence of the collection of all
subcollections of a given collection.  The only way such a power collection
can be a class or a set is if it is the power collection of a set.


POWER:
(forall x)(thereis y)(forall z)[{[z is in y] iff (forall w)[(w is in z)
implies (w is in x)]}&{(y is a set) iff (x is a set) iff (y is a class)}]


The axiom of infinity only specifies that there is an infinite collection
whose initial member is an empty collection.  There are various ways to see
why the empty collection is a set.  Using the definition of ``class'' from
above, one can show that the empty collection is a class.  From the set
existence axiom, it follows that the empty class is a subclass of a set.
Using the separation schema, one gets an empty set as well, and it must, by
extension, be the same collection as the empty collection at the ``bottom''
of the infinite collection demanded by the axiom of infinity.


INF:
(thereis x)(thereis y){[(forall t)(t is not in x)]&[x
is in y]&[y is a set]&(forall p)[(p is in y) implies (thereis
q){(q is in y)&(forall r)[(r is in q) iff (r is in p) or (r=p)]}



The axioms of substitution should be written more like the corresponding
axioms from ZF, rather than like the GBN class axioms of substitution.  They
say that functional formulas applied to sets yield sets as images.  It will
follow from this scheme and the definition of classes that the functional
image of a class is a class, even in the case of a proper class.

SUBST(psi):
(forall x)(forall y)(forall z){[psi(x,y)&psi(x,z)] implies y=z} implies
(thereis w)(forall y){[y is in w] iff (thereis x)[(x is in w)&psi(x,y)}



The axiom of global choice for sets is formulated as it is in GBN.  Notice
that it is only ``global choice'' for, as I said, sets.  It is not global
choice for the universe of all collections, or even all classes.

GCS:
(thereis f){[f is a function]&(forall x)[(x is a set) implies {(thereis y)[y
is in x] implies [(x,f(x)) is in f]}]}


Now, to ``force'' the failure of choice for classes, we stipulate the
failure of any function to be a choice function for all classes
(simultaneously).

NCC:
(forall f){[f is a function] implies (thereis x)[(x is a class) & {(thereis
y)[y is in x] & [f(x) is not in x]}]}


Now, the questions I think need to be answered are the following.

1.  Is T a conservative, relatively consistent extension of GNB?

2.  Let NEC be the statement that negates (in L) the one Professor Shavrukov
asked about:
(there is x){(x is a class)&(thereis e)[e is an equivalence on x]&(forall
f)[(f is a function from x into x) implies {(forall p)[(p is in x) implies
((p,f(p)) is in e)] implies [(thereis y)(thereis z){(y is in x)&(z is in
x)&(not[f(y)=f(z)])}]}]

3.  Let EC be the statement (in L) that you asked about:  EC=not(NEC).

4.  Is NEC a theorem of T?

5.  Is EC a theorem of T?







Dr. Matt Insall
http://www.umr.edu/~insall