[FOM] on Bas Spitters on "constructive impredicativity?"
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
and at greater length on Section 2.5 of my paper "Predicativity
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.
More information about the FOM