[FOM] Martin-Lof predicativity

[William Tait]

In view of my previous note today (April 11) on Martin-Loef's type  
theory and, in particular, my statement that it is impredicative,  
some further comment is needed in responsde to the quote below from  
Jesper Carlstroem:

Predicativity is a property of definitions. Impredicative   
definitions of functions are admitted in the M-L theory, as I noted.  
But all of the functions of finite type definable by impredicative  
primitive recursion---indeed, all of the objects definable in the  
Curry-Howard theory---are also definable by predicative recursion on  
epsilon_0 (in the F_S sense). I did not know that Feferman had shown  
that all of the objects defined in M-L's theory, e.g. those defined  
using reflection, also have predicative definitions, although it is  
not surprising. {Perhaps it was forshadowed by Matin-Loef's statement  
that the stregnth of his theory should be close to that of  
predicative analysis.

Bill Tait

On Apr 11, 2006, at 2:14 PM, Jesper Carlström wrote:

> I don't have the paper at hands, but I got a useful comment from  
> Thierry
> Coquand. He says that the type theory presented in this paper  
> [Martin-Loef's]  is, in
> fact, predicative in the sense of Feferman/Schutte. However, it was  
> not
> known to be by that time (although conjectured by Peter Hancock), but
> proved later by Feferman.
> http://www.cs.nyu.edu/mailman/listinfo/fom