home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / logic / 2026 < prev    next >
Encoding:
Internet Message Format  |  1992-11-13  |  1.9 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: Types of type theory
  5. Message-ID: <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
  6. Date: 13 Nov 92 13:15:46 GMT
  7. References: <BxIxGz.D7x@access.digex.com> <1992Nov12.144654.7493@ucthpx.uct.ac.za>
  8. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  9. Organization: LFCS, Edinburgh
  10. Lines: 31
  11. In-Reply-To: gavan@elc.mth.uct.ac.za's message of 12 Nov 92 14:46:54 GMT
  12.  
  13. In article <1992Nov12.144654.7493@ucthpx.uct.ac.za> gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:
  14.  
  15.    dzik@access.digex.com (Joseph Dzikiewicz) writes:
  16.    : I have come across two uses of the term "type theory" in logic that seem
  17.    : to be referring to different things.
  18.  
  19.    ...
  20.  
  21.    Type theory *is* higher-order logic, where the types are used to
  22.    avoid the paradoxes. One version -- the one Andrews explains --
  23.    is Church's Simple Theory of Types. There are others -- the Ramified
  24.    Theory of types (Ramsey) and the original, Russell's type theory.
  25.  
  26.    The Simple Theory of Types is just Predicate Calculus 
  27.    enriched with typed lambda calculus. 
  28.  
  29. There is still another type of type theory for which the most famous
  30. example is Martin-L"of's Type Theory. Here types and propositions are
  31. identified, i.e. a proposition is the type of its proofs. This may
  32. seem unusual but it leads to a very elegant formalisation of
  33. mathematical concepts. This sort of Type Theory is inherently
  34. intuitionistic because every proof has to have a constructive content.
  35. (I should mention that there is some work going on in extending this
  36. to classical reasoning).
  37.  
  38. --
  39.  
  40.  Thorsten Altenkirch             And there's a hand, my trusty fiere,
  41.  Laboratory for Foundations         And gie's a hand o' thine,
  42.  of Computer Science               And we'll tak a right guid-willie waught
  43.  University of Edinburgh            For auld lang syne!
  44.