[FOM] Martin-Lof predicativity

[William Tait]

On Apr 9, 2006, at 4:39 PM, Harvey Friedman wrote:

> Did this [Per Martin-Loef] 1975 publication already go beyond the  
> strength of the
> Feferman/Schutte formalism?

Martin-Loef, in an earlier paper (but not published until 1998)  
states that the strength of this theory "should be close to that of  
predicative analysis", where it seems clear he means in the sense of  
Schuette and Feferman.  ("An intuitionistic theory of types", *Twenty- 
five Years of Constructive Type Theory", [ed. by G. Sambin and J.  
Smith] OUP: 127-172).

> Did it contain an explanation of the notion of
> "predicative" that was being used? Did it refer to Feferman/ 
> Schutte? If it
> did, did Feferman comment on it?

M-L's theory of types includes as types all of the finite types over  
N (the type of natural numbers) in the sense of Goedel and its  
applies primitive recursion at each type. So it admits defining  
functions G of type A --> A and then using them to define objects G^n 
(a) of type A (where a is of type A). For example, when A is N --> N,  
this kind of definition yields the Ackermann function, which cannot  
be defined by ordinary 'predicative' primitive recursion.  This would  
seem, on anyone's conception of predicativity, to be impredicative.

M-L's use of the term 'predicative' was, I think, meant only to  
distinguish this system from an earlier theory (unpublished and shown  
by Girard to be inconsistent) which contained the 'type of all  
types'. In the 'predicative' version, this is replaced by a  
reflection principle which permits the passing from, say, the  
universe V of the 'small' types of the so-called Curry-Howard theory  
to a universe V' in which the types of V are terms. This creates  
another source of impredicativity in the usual sense(s) in that  
objects of types in V may be constructed from objects of types in V'.  
(If that weren't so, then the proof-theoretic strength of the theory  
would be that of the Curry-Howard theory, i.e. epsilon_0, not gamma_0  
as M-L states.

Bill Tait