[FOM] Martin-Lof predicativity

[Harvey Friedman]

On 4/9/06 1:32 PM, "Jesper Carlström" <jesper_fom at math.su.se> wrote:

> Friedman wrote:
>> I had in mind both the recent use of the term by type theorists discussed
>> by Spitters, but also use of the term by Weaver.
> 
> The type theorists' use is maybe not that recent. It goes back at least
> to 1973:
> 
> Per Martin-Löf, An intuitionistic theory of types: Predicative part. In
> H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium `73, pages
> 73-118. North-Holland, 1975.

Did this 1975 publication already go beyond the strength of the
Feferman/Schutte formalism? 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?

Feferman/Schutte is around 1964 and was, I think, well accepted before 1975.

Harvey Friedman