[FOM] Martin-Lof predicativity
wwtx at earthlink.net
Tue Apr 11 10:58:12 EDT 2006
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.
More information about the FOM