Q:\CHOICE\ALL.TXT      

2000 June 4

Comment: Our axiom of choice is the one published in the paper
about ordinal numbers.  It is a stronger version than the standard
axiom of choice used in Zermelo-Fraenckel set theory, and it is
not possible to translate our version to ZF because our version
uses proper classes.  In fact, our function CHOICE is a proper
class.

We created a variant AC-ALL.POS of the ALL.POS file in which the
flag AxCh is added to the sos list.  Doing so reveals which equations
would be demodulators in the presence of the axiom of choice.  We need
to know this to decide where to place CHOICE in the lex order.  Our
tentative idea is to place CHOICE following all other functions,
but before inverse and E.  No final decision has yet been made.
Our current lex order is this:

lex([0,Id,V,pair(x,x),singleton(x),cart(x,x),
     SINGLETON,complement(x),fix(x),D(x),apply(x,x),
     CHOICE,composite(x,x),inverse(x),E,
     AxCh,equal(x,x),member(x,x),subclass(x,x)]).

The CHOICE group uses no theorems at present beyond the VS groups,
and at present nothing depends on the theorems of the CHOICE group.
So we are tentatively placing the CHOICE group in the STANDARD.IN
file immediately following the VS groups.  If we find that any 
theorem using AxCh requires anything else, we will move it further
back.