[FOM] Feferman-Schutte: summary

[Nik Weaver]

I will try to summarize my reasons for saying that the ordinal
Gamma_0 has *nothing* to do with predicativism.  I hope people
interested in predicativism pay attention, because the statement
that Gamma_0 is the limit of predicative reasoning is routinely
asserted as a known fact.  In my opinion, this is a severe,
pervasive error long overdue for correction.

First of all, it is argued by Friedman and Taranovsky that
irrespective of the success of the analysis put forward by
Feferman and Schutte, it is evident that Gamma_0 corresponds
well with our informal concept of predicativism.  This is a
relatively weak claim, but anyway it is simply false: Gamma_0
goes far beyond anything that would be recognized as predicative
reasoning in ordinary mathematical practice.  When you look at
predicative reasoning in ordinary mathematical practice you're
talking about ordinals like phi_{epsilon_0}(0).  There's no way
you could come up with Gamma_0 as a measure of bread-and-butter
predicative reasoning.

No, the case for Gamma_0 as a measure of predicative reasoning in
any sense cannot come from examining mathematical practice.  The
only hope is to get it from a formal analysis.

I have discussed my objections to the Feferman-Schutte analysis
of autonomous progressions in previous posts.  Feferman has also
("A more perspicuous formal system for predicativity"; "Reflecting
on incompleteness"; with T. Strahn, "The unfolding of non-finitist
arithmetic") presented several formal systems (P + exists/P;
Ref*(PA(P)); U(NFA)) which do not involve autonomous progressions
but are still supposed to model predicative reasoning, and still
have proof-theoretic ordinal Gamma_0.

In all of these systems (including the systems based on autonomous
progressions) the ability to access all ordinals less than Gamma_0
comes from the following basic fact:

** relative to a weak base system, arithmetical recursion up to
alpha implies induction up to phi_alpha(0). **

So, if we have some way of inferring arithmetical recursion
from induction then we can get from gamma_n to gamma_{n+1} =
phi_{gamma_n}(0), and the supremum of this sequence (with
gamma_0 = 1) is Gamma_0.

However, each of these allegedly predicative systems employs an
impredicative feature whose function is precisely to enable that
inference from induction to recursion:

--- the autonomous systems impredicatively infer a transfinite
iteration of reflection principles from a statement of transfinite
induction

--- P + exists/P allows predicate substitution for Sigma_1^1
formulas

--- Ref*(PA(P)) makes truth claims about schematic predicates which
do not make sense unless one assumes an impredicative comprehension
axiom

--- U(NFA) allows predicate substitutions which do not make sense
unless one assumes an impredicative comprehension axiom.

For details, see my paper "Predicativity beyond Gamma_0".  In
addition, there are several other impredicative aspects to these
systems.  Both Ref*(PA(P)) and U(NFA) employ impredicatively
self-referential predicate variables.  Ref*(PA(P)) employs an
impredicatively self-referential truth predicate.  U(NFA) employs
an impredicative least fixed point operator.

These systems are impredicative in so many different ways, I find
it astounding that they would be taken by anyone as definitive
formalizations of predicative reasoning.  Are they?

There is, secondly, the objection that if one could somehow
convince oneself that the assertion "induction up to alpha implies
recursion up to alpha" is predicatively acceptable, this would
allow predicativists to get beyond Gamma_0.  The only way to have
Gamma_0 be a precise limit is to express the inference from induction
to recursion as a deduction rule each instance of which is taken to
be predicatively acceptable, but whose global correctness is not
predicatively knowable.  While there are situations where one can
accept a deduction rule but not the corresponding implication, it
is rather baffling to try to imagine why anyone would think the
present situation is one of them.  Of course, in order to discuss
this question we first need to understand why people think each
instance of the deduction rule is predicatively acceptable, which,
unless I missed something, no one has yet even attempted to explain.
So far the only coherent argument posted on the FOM list against my
objections is the argument that there exist situations in which a
deduction rule is valid but the corresponding implication is not.
This is hardly an adequate response, but then I doubt there is any
adequate response.  I think the case against the Feferman-Schutte
analysis is overwhelming and irrefutable.

In fact I believe that one can get up to Gamma_0 in a predicatively
legitimate way, not through ordinary mathematical reasoning but by
using hierarchies of Tarskian truth predicates.  However, this
process does not naturally stop at Gamma_0.  It takes one much
further.  I will post a message about this next.

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu
http://www.math.wustl.edu/~nweaver/