[FOM] on Bas Spitters on "constructive impredicativity?"
Nik Weaver
nweaver at math.wustl.edu
Fri Mar 31 18:12:52 EST 2006
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
More information about the FOM
mailing list