🚀 go-pugleaf

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