EQUATION.TXT            2001 January 23

The idea of formulating set theory as an equational theory was
inspired by Tarski and Givant's book, but we do not follow their
specific formalism.

Using the assert function in the GOEDEL program, one can convert any
statement into an equation of the form equal[V,x]. The rules that were
found for converting clauses to equations have been gathered together in
the standalone program CONVERT.M. The GOEDEL program was also used to
eliminate all Skolem functions appearing in Quaife's axioms and
definitions for set theory, resulting in the 60 clauses listed in
AXIOMS.M. 

The CONVERT.M program contains a few simplification rules that were
present in the GOEDEL program back in 1998, when this work was done. It
is doubtful whether these rules are actually used in converting the 60
clauses representing Quaife's axioms and definitions for set theory.
If they are used, it is conceivable that some of these rules would 
need to be added to provide a complete set of equational axioms for
set theory. 

The Mathematica log file EQUATION.LOG contains the results of converting
the 60 clauses to equational form.  The clauses that are simplified to 
True should probably simply be omitted.

Some further caveats:

1.  The equations are on the whole rather complicated and therefore
    less appealing than the clauses from which they were obtained.

2.  The conversion to equational form depends on using NBG style
    axioms.  The universal class V appears prominently.

3.  It is probably too naive to assume that simply translating a set
    of axioms for set theory into equational form would suffice to 
    obtain an adequate foundation for set theory.  One would need to
    be convinced that the equations obtained could actually be used 
    to prove theorems of set theory.

4.  All the equations are of the form equal[V,z].  There is a rule
    in CONVERT.M that converts any equation equal[x,y] to this
    special form.  Should that rule be made into an inference rule?