[FOM] Feferman-Schutte: response to Tait

[Nik Weaver]

Bill Tait wrote (quoting me):

> > If a predicativist trusts some formal system for second order
> > arithmetic, then he should accept not only the theorems of the
> > system itself but also additional statements such as the assertion
> > that the system is consistent.
[snip]
> It can happen that each deduction in a formal system is valid
> under a given conception, without the general statement of the
> validity of *all* deductions in the system being valid under
> that conception ... So I think that what is described above
> under the heading "The accepted justification for the claim"
> is wrong. But I also don't recall it as a justification anyone
> gave for the claim that Gamma_0 is the ordinal of predicative
> analysis.

Possibly I was unclear.  I agree that we can't a priori rule out
the possibility of someone being able to accept every deduction
within some system yet not being able to globally accept the
validity of all deductions in the system.

What I was referring to was the set-up for the F-S analysis,
where we start with a system that we believe a predicativist
*can* globally accept.  We then start adding reflection
principles and see how far we can go.  As I understand it,
the standard justification for the claim that Gamma_0 is the
ordinal of predicative analysis is framed in these terms.
At least, this is how Feferman presents it in "Systems of
predicative analysis".

> Note that this is fundamentally Nic's objection, but relocated
> where I think it belongs: If ramified analysis is locked into
> talking only about sets of given orders, then how can it prove
> meaningfulness of propositions of some order beta+1, where this
> seems to require well-foundedness with respect to all descending
> sequences from beta, and not just those of some specific order.

I think you are talking about infinitary (semiformal) ramified
systems, while I am talking about finitary unramified systems.
Both approaches (actually, all four approaches: infinitary or
finitary, ramified or unramified) are considered in Feferman's
"Systems of predicative analysis".  But it does seem like our
objections are basically equivalent.

William Howard made some similar points in "Some proof theory in
the 1960's".

> What is the F-S response to it?  (I haven't looked for one from
> them.  I do remember this point occurring to me a long time ago.
> But I wasn't sufficiently interested in predicativity to pursue
> it.)

Feferman's response to my paper is posted here:
http://www.math.wustl.edu/~nweaver/response1.html
(See also
http://www.math.wustl.edu/~nweaver/response2.html
for my reply.)

However, he doesn't directly answer this point.  I got the impression
that he felt that the autonomous progressions idea had been superseded
by more recent ideas of his and that this is where the debate should
take place.  (In my Gamma_0 paper I also criticize these more recent
systems.)

Nik