home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / logic / 1985 < prev    next >
Encoding:
Text File  |  1992-11-10  |  1.1 KB  |  31 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!digex.com!dzik
  3. From: dzik@access.digex.com (Joseph Dzikiewicz)
  4. Subject: Types of type theory
  5. Message-ID: <BxIxGz.D7x@access.digex.com>
  6. Sender: usenet@access.digex.com
  7. Nntp-Posting-Host: access.digex.com
  8. Organization: Express Access Online Communications, Greenbelt, MD USA
  9. Date: Tue, 10 Nov 1992 23:34:10 GMT
  10. Lines: 19
  11.  
  12. I have come across two uses of the term "type theory" in logic that seem
  13. to be referring to different things.
  14.  
  15. In one, Type Theory seems to relate to the rules for higher-order-logics
  16. (ie, second order logic and up).  This is discussed in Peter Andrews'
  17. book "An Introduction to Logic and Type Theory: To Truth through Proof."
  18. I have also seen it referred to as "Church's Type Theory."
  19.  
  20. In the other, types are sets of formulas in first order logic.  This
  21. is discussed in some detail in Chang and Keisler's book "Model Theory."
  22.  
  23. Am I correct in thinking that these are two different things with the same
  24. name, or are they the same thing presented differently by two
  25. different groups of authors?
  26.  
  27. Any enlightenment would be greatly appreciated.
  28.  
  29. Joe Dzikiewicz
  30.  
  31.