🚀 go-pugleaf

-*----
The wonderful thing about set theory, of course, is that in it
one can define almost all the other parts of mathematics: group
theory, field theory, measure theory, point set topology, etc.
But if one were writing or using theorem-proving tools to work
proofs in, say, group theory, one might not want to start with
the heavy load of ZF.  

For some theories, there are classical axiomatizations that stand
apart from set theory, e.g., arithmetic, real algebra, and plane
geometry.  Curiously, these all have intuitive axiomatizations
that do not rely on sets, and at least in the case of arithmetic
and plane geometry, axioms that were stated before set theory was
developed.  But the "natural" axioms for groups seem to rely on
sets: "a group is a *set* with a binary operator + such that ..."

So how would one axiomatize a "simple" group theory?  

Russell