home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2066 < prev    next >
Encoding:
Internet Message Format  |  1992-11-17  |  2.7 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.92Nov16194749@tanera.dcs.ed.ac.uk>
  6. Date: 16 Nov 92 19:47:49 GMT
  7. References: <BxIxGz.D7x@access.digex.com> <1992Nov12.144654.7493@ucthpx.uct.ac.za>
  8.     <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
  9.     <1992Nov13.123046.17412@husc3.harvard.edu>
  10. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  11. Organization: LFCS, Edinburgh
  12. Lines: 42
  13. In-Reply-To: zeleny@husc10.harvard.edu's message of 13 Nov 92 17:30:45 GMT
  14.  
  15. In article <1992Nov13.123046.17412@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:
  16.  
  17.    TA:
  18.    >There is still another type of type theory for which the most famous
  19.    >example is Martin-L"of's Type Theory. Here types and propositions are
  20.    >identified, i.e. a proposition is the type of its proofs. This may
  21.    >seem unusual but it leads to a very elegant formalisation of
  22.    >mathematical concepts. This sort of Type Theory is inherently
  23.    >intuitionistic because every proof has to have a constructive content.
  24.    >(I should mention that there is some work going on in extending this
  25.    >to classical reasoning).
  26.  
  27.    I would prefer not to conflate intuitionism with constructivism;
  28.  
  29. Sorry, if I gave this impression. Although Type Theory (in the sense
  30. of Martin-L"of) is constructive it is not necessarily intuitionistic,
  31. i.e. we may accept Markov's principle.  This would be particularly
  32. useful if you use Type Theory for program verification. However, all
  33. the Type Theories I know are actually intuitionistic.
  34.  
  35.    otherwise
  36.    your final remark is misleading, as the results of G\"odel and Tarski imply
  37.    that any proof-theoretic conception of mathematical truth will fall short
  38.    of the bivalence required by the classical reasoning.
  39.  
  40. Certainly, but this just means that you have to give up something to
  41. get classical reasoning AND propositions as types. I am not an expert
  42. in this area but as I understand it: You may have a computational
  43. interpretation of type theory if you 'fix' your evaluation strategy
  44. (i.e. you decide to use only the equations of the call-by-value
  45. \lambda calculus). 
  46.  
  47. I suppose the most famous person working in this direction is Girard
  48. who last year wrote a paper entitled "A New Constructive Logic:
  49. Classical Logic". However, I should also mention Parigot's "Free
  50. Deductions" and Vilinsky's categorical account of continuations.
  51. --
  52.  
  53.  Thorsten Altenkirch             And there's a hand, my trusty fiere,
  54.  Laboratory for Foundations         And gie's a hand o' thine,
  55.  of Computer Science               And we'll tak a right guid-willie waught
  56.  University of Edinburgh            For auld lang syne!
  57.