[FOM] Impredicativity of Kruskal's Theorem
jesper_fom at math.su.se
Sun Apr 9 13:32:34 EDT 2006
> 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
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.
More information about the FOM