[FOM] Martin-Lof predicativity

[Jesper Carlström]

Harvey Friedman wrote:
>> 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?

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 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. I think that the conjecture could hardly be 
the reason for the choice of the title. Rather, I think the title was 
meant to say that the impredicativity problem of an earlier theory had 
been removed. I must confess that this is pure speculation of mine. It 
is clear however that when W-types and other constructions beyond Gamma0 
were introduced later on, this was not considered to be a step back to 
impredicativity. The community continuous to call it "predicative type 
theory", although some prefer to say "generalized predicative".

Thierry Coquand also sent the following list of references:

Feferman, Solomon. Iterated inductive fixed-point theories:
application to Hancock's conjecture.  Patras Logic Symposion
(Patras, 1980),  171--196, Stud. Logic Foundations Math.,
109, North-Holland, Amsterdam-New York, 1982.

Martin-Löf, Per. Constructive mathematics and computer programming.
Logic, methodology and philosophy of science, VI (Hannover, 1979), pp.
153--175

Palmgren, Erik. On universes in type theory. Twenty-five years of 
constructive type theory (Venice, 1995),  191--204,
Oxford Logic Guides, 36, Oxford Univ. Press, New York, 1998

Rathjen, Michael The strength of Martin-Löf type theory with a
superuniverse. I.  Arch. Math. Logic  39  (2000),  no. 1, 1--39.


Best regards,
Jesper Carlström