firstname.lastname@example.org wrote: |It's still possible, of course, for someone---you mentioned Nik Weaver---to |come along and argue that our intuitive notion of predicativism, fuzzy |though it is, can't possibly be identified with the level Gamma_0. The |reason you can't seem to decide immediately whether Weaver's position is |nonsensical or not is probably because the critical questions are not |mathematical but philosophical, and of course it's usually harder to arrive |at definitive answers in philosophy than in mathematics.
My impression is that a lot of it has to do with Weaver's being interested in predicativism as a possible working philosophy, which is not quite the same as being interested in the concept of predicativity in the abstract.
There's a basic problem with relating a philosophy to formal systems, due to Goedel incompleteness. If we can exhibit a formal system S that allegedly captures all the reasoning acceptable to a given philosophy of mathematics, then it's a little hard to see how such a claim can be supported. If someone holding that philosophy can see that this is so, then how can they fail to see that S is consistent, which is unprovable in S? And if the formal system S captures all the reasoning they accept without their knowing it, how can this be established by anyone else?
Consider this for the prototypical "believer in ZFC". Proofs from ZFC tend to be accepted as proofs without the author feeling the need to include any of the axioms among the hypotheses, whereas proofs from large cardinal axioms and the like tend to be stated with the additional assumptions listed as explicit hypotheses. It's not very credible to say, however, that provability in ZFC represents the exact line between what can be accepted as proven and what can't, since, in particular, if one manages to prove that a theorem follows from the consistency of ZFC, this is as good a reason to believe it as its provability from ZFC.
Weaver and Feferman regard this situation in different lights in the case of predicativism. (And of course they differ on other issues.)
>From my point of view, we have to concede to the objection but only so far. I don't think we can reasonably ask a predicativist to agree that only the things that can be proven predicatively, in the sense of the famous analysis of predicativity, can be validly proven. That would be akin to asking the "ZFC believer" to agree not to believe that ZFC is consistent. On the other hand, however, I'm unpersuaded by any of the arguments that I've read that the predicativist is entitled to go "very far beyond" the formal sense of predicativity, where I'm just going to leave "very far beyond" as a vague idea here. I think we can concede that some amount of reflection upon the concept of predicative proof, taking the predicativist outside of the strict formal limits on it, is compatible with the overall philosophy, without having to concede that anything very "strongly impredicative" has been justified in a way compatible with their philosophy.
I don't think it's so hard to see that the way one ordinarily proves induction up to Gamma_0 is impredicative. It's not that it's impossible to define it predicatively. Each computable ordinal can be defined as an ordering on natural numbers, given by a primitive recursive relation on them. The existence of this ordering isn't the problem. The problem is proving induction up to it. The way that one ordinarily does it makes reference to sets of ordinals. That's the gist of it. To show that this is not a merely apparent obstacle to a predicative proof is a longer story.