[FOM] on Bas Spitters on "constructive impredicativity?"

[Nik Weaver]

Harvey Friedman wrote (quoting Bas Spitters):

> > "Predicativity" as used by Feferman-Schutte refers to a level of
> > proof-theoretic strength. By type theorists the term is used for
> > a kind of "non-circularity in definitions" ...
>
> I strongly recommend, for historical and other reasons, that people
> refrain from using "predicative" for anything not falling under the
> scope of the much much older and classically accepted analysis of
> Feferman/Schutte.

Friedman is way off here.  To the contrary, the idea that
generalized inductive definitions are predicative is actually
older than the Feferman-Schutte analysis.  I don't know if it's
"much much older" but it is clearly enunciated in, for example,
H. Wang, "The formalization of mathematics", JSL 19 (1954),
241-266 and in P. Lorenzen, "Logical reflection and formalism",
JSL 23 (1958), 241-249, both of which appeared well before
Feferman's first paper on predicativism in 1964.

Could Friedman describe his "other reasons" for insisting that the
term "predicative" be used not to refer to the actual foundational
stance of that name originally developed by Poincare and Russell,
but rather to a particular attempt at formalizing that stance which
has recently come under severe criticism (by me)?  Does he have
anything to say about that criticism, which I claim reveals a basic
flaw in the original Feferman-Schutte analysis involving a confusion
between induction and recursion?  How does he justify his continued
reference to Kruskal's theorem as being predicatively unprovable in
the face of my thorough analysis of predicativism which I claim
shows that Kruskal's theorem is in fact predicatively provable?


Nik