[FOM] Friedman on predicativity

[friedman@math.ohio-state.edu]

I am responding to this posting of Nik Weaver because of its misleading
nature and needless dogmatic tone.

Nik Weaver wrote:

> Harvey Friedman, in a message that may or may not have been
> a response to my recent posts on predicativism, wrote:

I was spurred to thinking again about predicativity by your postings, but
I was not trying to respond to your postings.
>
>> 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.

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). It is obviously at the minimum,
extremely controversial to assert that even Gamma_0 can be predicatively
proved to be well ordered. The classic analysis of Feferman and Schutte is
at the moment currently the most adhered to analysis worldwide - among
those who accept any analysis. Furthermore, there is also widespread doubt
as to whether predicativity has a sufficiently clear meaning to support
any definitive analysis - yours or anyone elses'.
>
>> 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

again, this is unwarranted dogmatism.

> 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.

Whatever comparability of well orderings is, as a statement, it certainly
is not specialized, and it certainly is not proof theoretic.

Comparability of well orderings is a standard set theoretic fact taught
throughout the world in both the undergraduate and graduate mathematics
curriculum. Often it is proved simply as an easy Corollary of Zorn's
Lemma, another mainstay of the curricula.

You could of mentioned that I also referred to my work with Hirst and also
some of my own work that gives various equivalent forms of comparability
of well orderings, that are more mathematically interesting. In
particular, the continuous comparability of countable sets of real
numbers. I.e., let A,B be countable sets of real numbers. Either there is
a pointwise continuous embedding from A into B or there is a pointwise
continuous embedding from B into A. This is provaly equivalent to ATR0
over RCA0, and so under the Feferman Shutte analysis, is not predicatively
provable and not predicatively reducible.

> We must remember that the well-ordering concept has classically
> equivalent versions which are not predicatively equivalent.

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.

>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".

This definition is equivalent under the standard mathematical meaning of
predicate used in mathematics. If you are using the word "predicate" in a
nonmathematical way - i.e., in a proof theoretic way - then you are not
talking about mathematical statements anymore, but rather proof theoretic
schemes.
>
> But it is the latter version of well-ordering which is significant in
> ordinary mathematics, not the former.

Just the opposite is the case. The one normally used is of great
significance for ordinary mathematics, especially historically - starting
from the time of Cantor with his analysis of closed sets of real numbers.
(Cantor-Bendixson decomposition). The proof theoretic scheme becomes
important when moving to proof theoretic studies.

Harvey Friedman