[FOM] Impredicativity of Kruskal's Theorem

[Jesper Carlström]

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.

Best,
Jesper Carlström