[FOM] "Refutation" of the Feferman-Schutte analysis of predicativism

[Aatu Koskensilta]

On Apr 14, 2006, at 10:53 PM, Nik Weaver wrote, initially quoting 
Friedman:

>> 5. Weaver believes that Feferman/Schutte must give explicit
>> reasons for explicitly denying **). [NOTE: Weaver believes
>> that Feferman/Schutte cannot rely on the fact that there is
>> no implication from *) to **). Weaver believes that If they
>> don't, then Feferman/Schutte has been REFUTED by Weaver.]
>
> No, I wouldn't say this.  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

and not

  (*') It is predicatively acceptable that if I(a) is predicatively 
acceptable, then uniform
      reflection for T_a is also 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!). 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. (*') in some sense does, at least 
if we give the second order part of the theories intuitionistic reading 
as Weaver does. The reason *we* can know (*) is that we have a uniform 
picture, based on our understanding of the set of ordinal notations O 
or the set of well-founded countable trees, of how to proceed from a 
particular proof I(a) to a proof of uniform reflection for T_a (or the 
existence of a well-determined totality of sets R_a of order a). This 
uniform picture is not available for the predicativist, since it relies 
on impredicative concepts and reasoning.

Similar considerations apply to the modus ponens example Weaver gives 
in his paper. It's entirely possible for it to be true of someone 
called A that

  (+)  If A accepts A and A-->B then A accepts B

without A accepting

  (++) If A and A-->B then B

The presence of the inference rule A |- B in a formal system given as 
an analysis of acceptability based on some stance does not, and in 
general cannot, mean that "from A infer B" is acceptable based on that 
stance.

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. For a particular instance (for a given a and 
P) of reasoning like this you need not understand the general notion of 
a well-founded tree, but to see the uniformity in instances of (*) for 
different a and P you do need the general notion of a well-founded tree 
(and truth). 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.

I'd like to thank Weaver for having made at least me think harder about 
the conceptual justification of the Feferman-Schütte analysis, even if 
I remain as yet convinced that it is basically correct.

Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus