🚀 go-pugleaf

In article <1992Nov12.144654.7493@ucthpx.uct.ac.za> gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:

   dzik@access.digex.com (Joseph Dzikiewicz) writes:
   : I have come across two uses of the term "type theory" in logic that seem
   : to be referring to different things.

   ...

   Type theory *is* higher-order logic, where the types are used to
   avoid the paradoxes. One version -- the one Andrews explains --
   is Church's Simple Theory of Types. There are others -- the Ramified
   Theory of types (Ramsey) and the original, Russell's type theory.

   The Simple Theory of Types is just Predicate Calculus 
   enriched with typed lambda calculus. 

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).

--

 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!