[FOM] Feferman-Schutte: response to Koskensilta

[Nik Weaver]

Aatu Koskensilta wrote (quoting me):

> > I think proponents of the F-S analysis definitely have a
> > burden to explain why (*) is predicatively acceptable, since
> > on its face it is not.
>
> I'm in the middle of writing a complete critique of your paper,
> but I think here we have hit one important point. Under the F-S
> analysis it is *not* claimed that (*) is predicatively acceptable,
> only that (*) is true. That is, what we need is
>
>  (*) It is true that if I(a) is predicatively acceptable, then
> uniform reflection for T_a is also predicatively acceptable

I apologize for the imprecision.  I should have said "why every
instance of (*) is predicatively acceptable" (and of course I was
referring to my (*), not your (*) which you are freshly introducing).
Elsewhere I stated this correctly.

My version of (*) was

(*)   from  I(a)  and  Prov_{S_a}(A(n)),   infer   A(n)

and I asked why every instance of this rule is predicatively
acceptable.  So Koskensilta's assessment of "what we need" is
in complete accord with my assessment.

The "we have hit one important point ... it is *not* claimed"
language bothers me since this suggests that I have been asking
the wrong question.  However, I have only myself to blame because
I did in this one instance refer to (*) being predicatively
acceptable rather than every instance of (*) being predicatively
acceptable.

> Now, it is true that (*) is a claim that needs to substantiated,
> and I won't have much to say about that just now (sorry!).

Well, I do think this is the key point.  So I look forward to
hearing your substantiation.

> What is clear, however, is that (*) in no way, logical or
> conceptual, implies that the implication
>
>   (**) I(a) --> uniform reflection for T_a
>
> should be predicatively acceptable.

Agreed, but I think that's a bit of a straw man.  My claims are
(1) instances of (*) are generally not predicatively acceptable
and (2) any coherent foundational stance that justifies acceptance
of every instance of (*) would justify (**).

All you need to do to defeat (2) is to produce some coherent set
of beliefs that would lead one to accept every instance of (*)
but not (**).  You don't even have to make a case that these
beliefs count as "predicative".  However, merely pointing out
that (*) doesn't imply (**) is not enough.

> One way to justify (*) is by appeal to infinitary proof trees.
> The idea is simply that you can convert proofs in T_a into
> infinitary proof trees, and apply cut elimination (which you
> read off the proof of I(a)) to these (primitive recursive) trees,
> and then for a proposition P apply the truth predicate restricted
> to sentences of complexity of P to obtain reflection for P.

That is essentially what Kreisel suggests in "Principles of proof
and ordinals implicit in given concepts".  However, he doesn't say
how to do it, he merely expresses confidence that it could be done.
("The principle problem is conceptual: to formulate properly just
what details are needed.")

> I think this is the idea behind using infinitary proof trees in
> analysing predicativity, but I'm not really sure. I'll come back
> to these issues in my longer reply to Weaver.

Okay, I look forward to seeing this.

Nik