[FOM] Impredicativity of Kruskal's Theorem

[hendrik@topoi.pooq.com]

On Sun, Apr 02, 2006 at 04:22:30PM -0400, Harvey Friedman wrote:
> On 4/1/06 8:25 PM, "Nik Weaver" <nweaver at math.wustl.edu> wrote:
> 
> > 
> > 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.
> 
> I know of no one who doesn't have a special analysis of predicativity that
> they promote who believes that there is a single coherent notion of
> predicativity that has any kind of uniqueness to it.

Might it be that there is a coherent but vague idea of predicativity?
That is it a slippery concept that has no business having its 
definition set in stone and formalized?

> This is in sharp
> contrast to effectivity, where the vast majority of people who don't have
> any special analysis (very few do), believe that there is a single coherent
> notion (modulo the proviso that one is not talking about physical processes,
> and one is talking about no limitations on resources, etc.).

Does acceptance -- or not -- of the axiom of choice, the continuum 
hypothesis, the large cardinal axioms affect which processes one 
considers effective?

> 
> If people want to talk about
> 
> Weaver predicativity

> Feferman/Schutte predicativity.

Nik, perhaps it would further the discussion to have a presentation 
of Wang/Lorenzen predicativity.

      Hendrik Boom



P.S. My personal view is that predicativity means that predicates must 
be defined in terms of ground concepts, and further that unravelling a 
definition must be, at the very least, some kind of a process that 
terminates.

The problem with the Russell set (the paradigm for impredicativity) is 
not that it has a recursive definition, but that the recursion doesn't 
terminate.

The vagueness here lies in the the word *process* above.  For example, 
if a definition yielded a process generating an infinitary well-founded 
and/or tree, would that be sufficient to consider it predicative?

Or am I all wrong?  Should the word "predicativity" refer to the 
actual nonrecursive syntactic form of the definition rather than its 
computational properties?

-- Hendrik