home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / logic / 2013 < prev    next >
Encoding:
Internet Message Format  |  1992-11-12  |  2.0 KB
  1. Path: sparky!uunet!charon.amdahl.com!pacbell.com!sgiblab!cs.uoregon.edu!ogicse!psgrain!ee.und.ac.za!shrike.und.ac.za!casper.cs.uct.ac.za!ucthpx!elc.mth.uct.ac.za!gavan
  2. From: gavan@elc.mth.uct.ac.za (Gavan Tredoux)
  3. Newsgroups: sci.logic
  4. Subject: Re: Types of type theory
  5. Message-ID: <1992Nov12.144654.7493@ucthpx.uct.ac.za>
  6. Date: 12 Nov 92 14:46:54 GMT
  7. Article-I.D.: ucthpx.1992Nov12.144654.7493
  8. References: <BxIxGz.D7x@access.digex.com>
  9. Sender: news@ucthpx.uct.ac.za (UCT News Admin.)
  10. Organization: University of Cape Town
  11. Lines: 34
  12. X-Newsreader: Tin 1.1 PL4
  13.  
  14. dzik@access.digex.com (Joseph Dzikiewicz) writes:
  15. : I have come across two uses of the term "type theory" in logic that seem
  16. : to be referring to different things.
  17. : 
  18. : In one, Type Theory seems to relate to the rules for higher-order-logics
  19. : (ie, second order logic and up).  This is discussed in Peter Andrews'
  20. : book "An Introduction to Logic and Type Theory: To Truth through Proof."
  21. : I have also seen it referred to as "Church's Type Theory."
  22. : 
  23. : In the other, types are sets of formulas in first order logic.  This
  24. : is discussed in some detail in Chang and Keisler's book "Model Theory."
  25. : 
  26. : Am I correct in thinking that these are two different things with the same
  27. : name, or are they the same thing presented differently by two
  28. : different groups of authors?
  29.  
  30. Type theory *is* higher-order logic, where the types are used to
  31. avoid the paradoxes. One version -- the one Andrews explains --
  32. is Church's Simple Theory of Types. There are others -- the Ramified
  33. Theory of types (Ramsey) and the original, Russell's type theory.
  34.  
  35. The Simple Theory of Types is just Predicate Calculus 
  36. enriched with typed lambda calculus. 
  37.  
  38. Types themselves can be thought of as sets, with a little care, 
  39. depending on how you want to give the *semantics*. Chang and Kreisler
  40. deal with models, Andrews with the logic. 
  41.  
  42. But, ahem, types pitch up all over the place: they just prevent certain
  43. things (eg. applying a function to the wrong arguments) from happening.
  44. Eg. types of variables in computer languages.
  45.  
  46. Gavan Tredoux
  47. UCT
  48.