home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / logic / 2029 < prev    next >
Encoding:
Internet Message Format  |  1992-11-14  |  3.9 KB

  1. Path: sparky!uunet!ogicse!das-news.harvard.edu!husc-news.harvard.edu!husc10.harvard.edu!zeleny
  2. From: zeleny@husc10.harvard.edu (Michael Zeleny)
  3. Newsgroups: sci.logic
  4. Subject: Re: Types of type theory
  5. Message-ID: <1992Nov13.123046.17412@husc3.harvard.edu>
  6. Date: 13 Nov 92 17:30:45 GMT
  7. Article-I.D.: husc3.1992Nov13.123046.17412
  8. References: <BxIxGz.D7x@access.digex.com> <1992Nov12.144654.7493@ucthpx.uct.ac.za> <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
  9. Organization: The Phallogocentric Cabal
  10. Lines: 71
  11. Nntp-Posting-Host: husc10.harvard.edu
  12.  
  13. In article <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk> 
  14. alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:
  15.  
  16. >In article <1992Nov12.144654.7493@ucthpx.uct.ac.za>
  17. >gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:
  18.  
  19. >>dzik@access.digex.com (Joseph Dzikiewicz) writes:
  20.  
  21. JD:
  22. >>>I have come across two uses of the term "type theory" in logic that seem
  23. >>>to be referring to different things.
  24.  
  25. GT:
  26. >>Type theory *is* higher-order logic, where the types are used to
  27. >>avoid the paradoxes. One version -- the one Andrews explains --
  28. >>is Church's Simple Theory of Types. There are others -- the Ramified
  29. >>Theory of types (Ramsey) and the original, Russell's type theory.
  30.  
  31. That's backwards: Russell discovered the ramified type theory, designed to
  32. avoid the eponymous antinomy, as well as the semantic paradoxes, while
  33. Ramsey made the observation that, since mathematics was not concerned with
  34. truth or other such picayunish semantic notions, the ramification into
  35. levels was superfluous.  Alonzo Church is the foremost living authority on
  36. type-theoretic matters.  See his papers "A Formulation of the Simple Theory
  37. of Types" (JSL, 1940), "Russellian Simple Type Theory" (APA, 1975), and
  38. "Comparison of Russell's Resolution of the Semantical Antinomies with that
  39. of Tarski" (JSL, 1977).  Also see Girard's elegant formulation of typed
  40. \lambda-calculus, likewise indebted to Church, in his book _Proofs and
  41. Types_.  The latest formulation of Church's Logic of Sense and Denotation,
  42. in effect an intensional hierarchy of type theories, is forthcoming in
  43. _Nous_, which also contains the earlier version in the 1973-4 volumes.
  44.  
  45. GT:
  46. >>The Simple Theory of Types is just Predicate Calculus 
  47. >>enriched with typed lambda calculus. 
  48.  
  49. Not so.  The addition of \lambda-calculus is in no way essential; all that
  50. is needed is a semantics that supports the recursively defined hierarchical
  51. partition of quantified variables as ranging over the types of individuals,
  52. as well as functional types with arbitrary choices of domain and range
  53. types; alternatively, relations may be used in place of functions, and a
  54. silly set version of type theory may be formulated to look like a
  55. non-cumulative version of ZF(U), or any other well-founded (or not!) set
  56. theory with (or without!) ur-elements.
  57.  
  58. TA:
  59. >There is still another type of type theory for which the most famous
  60. >example is Martin-L"of's Type Theory. Here types and propositions are
  61. >identified, i.e. a proposition is the type of its proofs. This may
  62. >seem unusual but it leads to a very elegant formalisation of
  63. >mathematical concepts. This sort of Type Theory is inherently
  64. >intuitionistic because every proof has to have a constructive content.
  65. >(I should mention that there is some work going on in extending this
  66. >to classical reasoning).
  67.  
  68. I would prefer not to conflate intuitionism with constructivism; otherwise
  69. your final remark is misleading, as the results of G\"odel and Tarski imply
  70. that any proof-theoretic conception of mathematical truth will fall short
  71. of the bivalence required by the classical reasoning.  See the remarks of
  72. Tarski in his original paper on the concept of truth.
  73.  
  74. >--
  75. >
  76. > Thorsten Altenkirch             And there's a hand, my trusty fiere,
  77. > Laboratory for Foundations         And gie's a hand o' thine,
  78. > of Computer Science               And we'll tak a right guid-willie waught
  79. > University of Edinburgh            For auld lang syne!
  80.  
  81. cordially,
  82. mikhail zeleny@husc.harvard.edu
  83. " -- I shall speak bluntly, because life is short."
  84.