[FOM] Friedman on predicativity

[Nik Weaver]

Harvey Friedman wrote (quoting me):

> > In my paper "Predicativity beyond Gamma_0" I have presented
> > predicatively valid formal systems which prove the well-ordering
> > of notations for all ordinals up to and beyond
> > theta_{Omega^omega}(0)...

> That is your dogmatic opinion on a rather suble topic with a long
> history, going back not only to the 60's with Shutte and Feferman,
> but also to Poincare and Weyl and Lorenzen (at least) ...
> there is also widespread doubt as to whether predicativity has a
> sufficiently clear meaning to support any definitive analysis -
> yours or anyone elses'.

I wonder what makes my opinion "dogmatic".  I have presented a
detailed analysis of the deficiencies of previously proposed
formal systems for predicativity and, supported by a rather
lengthly discussion of predicative principles, I have presented
new systems which support the well-ordering proofs mentioned
above.

Maybe you want me to say "formal systems which I believe are
predicatively valid" or something of that nature.  Well, fine.
Is this really worth arguing about.  If you have a substantive
criticism of the claim that my systems are predicatively valid
I think this discussion would be more interesting.  But your
comment about "any definitive analysis - yours or anyone elses"
makes me think you haven't actually looked at my analysis.  I
don't claim it is definitive, and indeed one of the central
points of my paper is that it is implausible that any definitive
analysis is possible.

Incidentally, I've now been called supercilious, reckless,
grandiose, dogmatic, and misleading.  Yet substantive criticism
of my views has been somewhat lacking.  So, that is kind of
disappointing.

I guess the "misleading" charge relates to my comments about
comparability of well-orderings:

> Comparability of well orderings is a standard set theoretic
> fact taught throughout the world in both the undergraduate
> and graduate mathematics curriculum ...
> I know of no natural formulations of the notion of well ordering
> of the integers, or of reasonable countable spaces, that are not
> provably equivalent in ACA0, and hence provably equivalent
> predicatively.

The following formulations of the notion of well-ordering of omega
are not predicatively equivalent:

(1)  Prog(X) --> (forall a)(a in X)

(2)  Prog(P) --> (forall a)P(a)

Here "Prog(X)" means: for all a, if every b less than a is in X
then a is in X; "Prog(P)" is defined similarly.  I am using X as
a set variable and P as a predicate variable in the way that
Feferman does in several of his systems with which I am sure you
are familiar.  It would be accompanied by a substitution rule which
allows us to replace P with any intelligible expression.

Now (2) cannot be expressed in the language of second order
arithmetic so provable equivalence in ACA_0 is not a question.
You may consequently regard it as not "natural".  However, it
is something like sense (2) that is actually used in ordinary
mathematics, not sense (1).  We don't just want induction for
subsets, we want it for arbitrary statements.  Indeed, even
simple facts like comparability of well-orderings go beyond (1).

Classically we can deduce (2) from (1) using a comprehension
axiom but predicatively this is not legitimate.  The two notions
are predicatively distinct.  So it really is misleading to say
that comparability of well orderings is not predicatively
provable.  Very little about well-ordered sets is predicatively
provable if you use "well-ordered" in sense (1), but that is
not the sense that is predicatively central.

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu