🚀 go-pugleaf

In article <1992Nov13.123046.17412@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:

   TA:
   >There is still another type of type theory for which the most famous
   >example is Martin-L"of's Type Theory. Here types and propositions are
   >identified, i.e. a proposition is the type of its proofs. This may
   >seem unusual but it leads to a very elegant formalisation of
   >mathematical concepts. This sort of Type Theory is inherently
   >intuitionistic because every proof has to have a constructive content.
   >(I should mention that there is some work going on in extending this
   >to classical reasoning).

   I would prefer not to conflate intuitionism with constructivism;

Sorry, if I gave this impression. Although Type Theory (in the sense
of Martin-L"of) is constructive it is not necessarily intuitionistic,
i.e. we may accept Markov's principle.  This would be particularly
useful if you use Type Theory for program verification. However, all
the Type Theories I know are actually intuitionistic.

   otherwise
   your final remark is misleading, as the results of G\"odel and Tarski imply
   that any proof-theoretic conception of mathematical truth will fall short
   of the bivalence required by the classical reasoning.

Certainly, but this just means that you have to give up something to
get classical reasoning AND propositions as types. I am not an expert
in this area but as I understand it: You may have a computational
interpretation of type theory if you 'fix' your evaluation strategy
(i.e. you decide to use only the equations of the call-by-value
\lambda calculus). 

I suppose the most famous person working in this direction is Girard
who last year wrote a paper entitled "A New Constructive Logic:
Classical Logic". However, I should also mention Parigot's "Free
Deductions" and Vilinsky's categorical account of continuations.
--

 Thorsten Altenkirch         	And there's a hand, my trusty fiere,
 Laboratory for Foundations  	   And gie's a hand o' thine,
 of Computer Science 	      	And we'll tak a right guid-willie waught
 University of Edinburgh     	   For auld lang syne!