🚀 go-pugleaf

In article <1903t2INNanu@cs.utexas.edu> turpin@cs.utexas.edu (Russell Turpin)
 writes:

   >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 ..."

  The concept of a group involves the notion of set, but the
elementary group axioms don't rely on sets any more than the axioms of
any other first order theory. If you want to talk about all models of
the axioms of elementary arithmetic, or about all real-closed fields
you will again speak of sets. In ordinary mathematics, one is very
much concerned with general models of the elementary group axioms,
which were introduced precisely to describe a structure common to many
mathematical objects, but not with general models of the axioms of
elementary arithmetic.

  Most group theory of course cannot be formulated within the elementary
theory of groups, for the reason indicated above. If you want a theory
weaker than ZFC within which e.g. the study of finite groups can be carried
out, such theories have been formulated, and somebody more knowledgeable
will be able to give a suitable reference.

  However, I wish to take issue with your statement that the classical
axiomatizations of arithmetic, real algebra, or elementary geometry do
not rely on sets. In each case the intuitive axiomatization does rely on
some notion of set (of natural numbers, of real numbers, of points) -
namely in the induction axiom or some continuity axiom (such as the
completeness axiom for ordered fields). The corresponding first order
theories are another matter. In the case of arithmetic, the first
order theory is as we know incomplete, in the case of the real numbers,
it turns out to be complete. But in both cases, the classical and
intuitive axiomatization is the second order one.

In article <1903t2INNanu@cs.utexas.edu> turpin@cs.utexas.edu (Russell Turpin) writes:

   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?  

What about Type Theory (i.e. Martin-L"of TT & variations) ? Here a
group is a type + ... The notion of a type is simpler than the one of
sets in particulary you haven't got a "power type". Only if you really
need higher order logic you may use a more powerful Type Theory like
Coquand's Calculus of Constructions.

Martin-L"of actually proposes to use Type Theory as a foundation of
mathematics.

@Book{MartinLoefL84,
  author = 	{P. Martin-L\"of},
  title = 	"Intuitionistic Type Theory",
  publisher = 	"Bibliopolis",
  year = 	"1984"
}
@Book{NordstroemEtAl90,
  author = 	"Begt {Nordstr\"om} and Kent Petersson and Jan Smith",
  title = 	"Programming in {Martin-L\"of's} Type Theory",
  publisher = 	"Oxford University Press",
  year = 	"1990",
}

--
Thorsten Altenkirch		LFCS, Edinburgh

"Germany still proves reluctant to exchange email with other countries 
efficiently" - Summer 1992 Systems Newsletter, Dep. of CS,Edinburgh