[FOM] Impredicativity of Kruskal's Theorem
hendrik@topoi.pooq.com
hendrik at topoi.pooq.com
Mon Apr 3 09:16:32 EDT 2006
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
More information about the FOM
mailing list