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

[Nik Weaver]

Bas Spitters wrote:

> "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 wonder how
> this is connected to Weaver's definition of "predicative".

I appreciate the acknowledgement of my work on predicativism, but
I have to insist that I have not introduced a new definition.  I
have criticized the Feferman/Schutte analysis as being incoherent
and I have proposed a new analysis *of the same concept*.

As to the idea that "non-circularity in definitions" (in the sense
of generalized inductive definitions) is predicative, this was
certainly rejected by Feferman, although I don't know if he has
ever detailed his reasons.  Kreisel apparently considered it
plausible.  If intuitionistic logic is used the issue is rather
subtle but I believe there is a clear impredicativity.  In order
to affirm the minimality condition on a class defined by a
generalized inductive definition we need a sufficiently strong
concept of well-ordering, but the necessary concept is not
available until after the class has been defined.  There is a
clear circularity here, and as is often the case, the problem
arises from a failure to attend to predicative distinctions among
classically equivalent versions of the well-ordering concept.
I explained this in more detail in the message
http://www.cs.nyu.edu/pipermail/fom/2006-February/009724.html
and at greater length on Section 2.5 of my paper "Predicativity
beyond Gamma_0".

Nonetheless, on my analysis Kruskal's theorem is in fact
predicatively provable.  This comes out of a sophisticated
analysis of predicatively acceptable systems involving
hierarchies of Tarskian truth predicates, also described in
my Gamma_0 paper.

Nik