[FOM] Friedman on predicativity
Nik Weaver
nweaver at dax.wustl.edu
Tue Dec 13 11:08:52 EST 2005
Harvey Friedman, in a message that may or may not have been
a response to my recent posts on predicativism, wrote:
> I know how to adjust numerical parameters in Kruskal's theorem and hit
> just about any reasonable ordinal < the Ackermann ordinal (Theta sub
> Omega to the omega, at 0), so that unless one settles on an exact
> characterization of predicativity, one cannot settle on a verdict
> as to whether or not these adjustments of Kruskal's theorem are
> predicatively provable or not.
I disagree with this conclusion. 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). So all such adjustments of Kruskal's
theorem are predicatively provable.
I don't know about the graph minor theorem, but I believe that my
well-ordering proof techniques can be substantially extended and
this may very well lead to a predicative proof of results even of
this degree of strength. There is something for experts in proof
theory to work on here.
The rest of the message was basically a review of some of Friedman's
impressive contributions to reverse mathematics, work which I hold
in the highest regard. However, I do have a point to make about
the following sequence of assertions:
> Experience shows that standard mathematical statements *generally*
> have the following properties.
[snip]
> 2. Provably equivalent to ATR0, and so definitely not predicatively
> provable on anything like current views.
[snip]
> Case 2 includes such statements as comparability of well orderings ...
First of all, I should mention that since Gamma_0 is predicatively
provable and this implies the consistency of ATR_0, statements of this
degree of strength can be predicatively proven consistent. But more
important here is the fact that "comparability of well orderings" in
the sense used here is not a standard mathematical statement. I would
characterize it as a specialized proof-theoretical statement.
We must remember that the well-ordering concept has classically
equivalent versions which are not predicatively equivalent. For
example, classically we can define a linear ordering < on omega to
be a well-ordering if
(*) for every subset X of omega, if X is progressive with respect
to < then X = omega
holds. ("Progressive" means: for all a, if every element less than
a belongs to X then a belongs to X.) And then using a comprehension
axiom we can prove for any predicate P that if P(.) is progressive
then P(a) holds for all a in omega. Predicatively we cannot do this
in general, so "well-ordered for sets" does not provably imply
"well-ordered for predicates".
But it is the latter version of well-ordering which is significant in
ordinary mathematics, not the former. The value of well-ordering to
the working mathematician is that one can use it to prove a statement
is true for all values of some parameter when that parameter ranges
over a well-ordered set. And when we use the term "well-ordered" in
this sense there is no problem in predicatively proving comparability.
It is only when "well-ordering" is used in the weaker, specialized
sense (*), the sense that is not central to mainstream mathematics,
that comparability becomes a problem.
Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu
http://www.math.wustl.edu/~nweaver/conceptualism.html
More information about the FOM
mailing list