home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #20 / NN_1992_20.iso / spool / sci / logic / 1389 < prev    next >
Encoding:
Internet Message Format  |  1992-09-15  |  2.3 KB
  1. Path: sparky!uunet!mcsun!uknet!edcastle!dcs.ed.ac.uk!alti
  2. From: alti@dcs.ed.ac.uk (Thorsten Altenkirch)
  3. Newsgroups: sci.logic
  4. Subject: Re: How does one formalize "small" mathematical theories?
  5. Message-ID: <ALTI.92Sep15135932@tanera.dcs.ed.ac.uk>
  6. Date: 15 Sep 92 12:59:32 GMT
  7. References: <1903t2INNanu@cs.utexas.edu>
  8. Sender: nnews@dcs.ed.ac.uk
  9. Organization: LFCS, Edinburgh
  10. Lines: 46
  11. In-reply-to: turpin@cs.utexas.edu's message of 13 Sep 92 19:13:38 GMT
  12.  
  13. In article <1903t2INNanu@cs.utexas.edu> turpin@cs.utexas.edu (Russell Turpin) writes:
  14.  
  15.    The wonderful thing about set theory, of course, is that in it
  16.    one can define almost all the other parts of mathematics: group
  17.    theory, field theory, measure theory, point set topology, etc.
  18.    But if one were writing or using theorem-proving tools to work
  19.    proofs in, say, group theory, one might not want to start with
  20.    the heavy load of ZF.  
  21.  
  22.    For some theories, there are classical axiomatizations that stand
  23.    apart from set theory, e.g., arithmetic, real algebra, and plane
  24.    geometry.  Curiously, these all have intuitive axiomatizations
  25.    that do not rely on sets, and at least in the case of arithmetic
  26.    and plane geometry, axioms that were stated before set theory was
  27.    developed.  But the "natural" axioms for groups seem to rely on
  28.    sets: "a group is a *set* with a binary operator + such that ..."
  29.  
  30.    So how would one axiomatize a "simple" group theory?  
  31.  
  32. What about Type Theory (i.e. Martin-L"of TT & variations) ? Here a
  33. group is a type + ... The notion of a type is simpler than the one of
  34. sets in particulary you haven't got a "power type". Only if you really
  35. need higher order logic you may use a more powerful Type Theory like
  36. Coquand's Calculus of Constructions.
  37.  
  38. Martin-L"of actually proposes to use Type Theory as a foundation of
  39. mathematics.
  40.  
  41. @Book{MartinLoefL84,
  42.   author =     {P. Martin-L\"of},
  43.   title =     "Intuitionistic Type Theory",
  44.   publisher =     "Bibliopolis",
  45.   year =     "1984"
  46. }
  47. @Book{NordstroemEtAl90,
  48.   author =     "Begt {Nordstr\"om} and Kent Petersson and Jan Smith",
  49.   title =     "Programming in {Martin-L\"of's} Type Theory",
  50.   publisher =     "Oxford University Press",
  51.   year =     "1990",
  52. }
  53.  
  54. --
  55. Thorsten Altenkirch        LFCS, Edinburgh
  56.  
  57. "Germany still proves reluctant to exchange email with other countries 
  58. efficiently" - Summer 1992 Systems Newsletter, Dep. of CS,Edinburgh
  59.