[FOM] "Refutation" of the Feferman-Schutte analysis of predicativism
Aatu Koskensilta
aatu.koskensilta at xortec.fi
Sat Apr 15 05:35:09 EDT 2006
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
More information about the FOM
mailing list