Categories

INTRODUCTION: The following theory proves all axioms of Morse-Kelley's class theory, and as well it possess a kind of unlimited comprehension over Categories, so we can have the Category of all Categories, of all groups, rings, Topological spaces, actually of all particular kinds of structure. So this extends MK by structural motivation served by Categories. It also enjoys a nice easing on Acyclicity criterion for comprehension in such a manner that allows internal cyclicity of ordered pairs and only forbids external acyclicity, this might lead to provision of additional strength over the complete acyclic (i.e. stratified) approach to class Categories as present in Feferman's system and at the same times meeting all requirements he stipulated for a foundation of Category theory in classes. It might be possible to add an axioms to the effect of having a class of all classes by a similar technique to how ZF axiom were added, i.e. to have a tri-sorted theory with lower cases standing for sets, upper ones for Classes and italics for super-classes, now we add all the axioms below and add on top of them axioms about the super-classes where full stratification holds over them, also we add suitable interchange axioms; by then we'll have a stratified system with double enrichment. 

EXPOSITION

 zfc+CAT: is a bisorted first order theory with extra-logical primitives of equality "=", membership "in" and a primitive ordered pair operator symbol <,>. Upper case variable symbols stand for classes, while sets are represented by lower case symbols.

Identity axioms:

1.X=X

2.x=x

3.X=Y ^ Q(X) -> Q(Y)

4.x=y ^ Q(x) -> Q(y)

5.X=y ^ Q(X) -> Q(y)

6.X=y ^ Q(y) -> Q(X)

Set axioms: 

i, All axioms of ZFC written in lower case.

ii. For all x,y Exist z: z=<x,y>

iii. For all a,b Exist z: z= a x b

iv. For all r (for all m in r (Exist x,y(m=<x,y>)) -> Exit z (z=dom(r))) 

where a x b stand for the Cartesian product of a and b, and dom(r)

stand for the domain of r, both defined in the usual manner.

Set\Class interchange axioms:

I, Axiom of set closure: X in y -> Exist z (z=X)

II, Diagonal axiom: For all x Exist Y (x=Y)

Class axioms (all written in upper case only):

a: Full Extensionality over classes

b: Pairing of Classes

c: Class union of Classes

d: Power class of Classes

Category axioms (upper case):

A: Basic property: For all A,B,C,D (<A,B>=<C,D>  -> A=C ^ B=D)

Definition of Cyclicity\Acyclicity of formulas:

We define a non directed polygraph on each formula written completely in upper case such that its nodes are the variables in the formula, and an edge is defined between any two variables X,Y for each *occurrence* of an atomic formula of the form

X=Y

Y=X

X in Y

Y in X

X=<Y,Z>

X=<Z,Y>

A path is a continuous linear subgraph.

Now a formula would be called externally acyclic on pairs if and only if for every atomic sub-formula of it of the form <X,Z>=Y there exists exactly one edge between Y and X and one edge between Y and Z, and there do not exist a path between Y and any of X or Z that do not have one of those edges as a part of it (i.e. no external path from a pair to a projection of it is possible).

B. Exist X for all Y (Y in X <-> Exist A,B (Y=<A,B>))

This class would be denoted as: {PAIR}.

C. Acyclic Separation Schema: If Q is an externally acyclic formula on pairs, with no occurrence of the symbol C in it, then:

(For all A Exist C for all X (X in C <-> X in A ^ Q))

 is an axiom.

D. Exist X for all Y (Y in X <-> Exist z (z=Y))

/ Theory definition finished.

Zuhair