I have only just been able to return to your critical examination of the extent of predicativity in this paper. I welcome your extensive and detailed consideration of the issues involved and am impressed by your absorption of the extant literature and your strong philosophical motivations allied to predicativity to see whether existing analyses are satisfactory or require us to go beyond them. But I can do without the supercilious attitude manifested here and there, especially in the last paragraph on p. 16 (of which, more below). Here are some points in response. I did not have time to go over your other two related papers [47] and [48]; it appears that your critique here is largely independent of those.
p.1, last par. I disagree completely with the statement that "the limitation identified by Feferman and Schütte is probably now a primary reason, possibly the primary reason, for predicativism's nearly universal unpopularity." I think the reasons that it has not achieved the status of the other big foundational schemes, especially constructivism and set-theoretical platonism, have nothing to do with its formal characterization and in fact well predated the work that began in the 1950s in that direction. The main reasons are given in my survey article "Predicativity" [44] in the section "Predicativity sidelined: 1920-1950," and I shall not repeat them here. More to the point is, as you remark, the predicative unprovability, on the F-S characterization, of such statements as the Cantor-Bendixson theorem or the (Extended) Kruskal Theorem or the recognition of Gamma0 as an ordinal, which working mathematicians (do or would) accept without qualm. But that does not cut any ice one way or another regarding our characterization. If it is correct, so much the worse for predicativity. If it is incorrect, and something like what you propose in sec. 2 is correct, then there will surely be other examples of mathematical theorems unprovable in such a characterization that working mathematicians would readily accept and would lead them to ignore your foundational scheme too. Mathematicians for the most part simply don't like to have their hands tied and are not persuaded on philosophical grounds to abandon reasoning that is totally justified on the face of it, such as, to begin with, the use of the lub principle in analysis. The situation with constructivism is a bit different; though not accepted as a foundation for mathematics by 99.99% of working mathematicians, they can see the point of doing mathematics in a way that leads systematically to computable results, even if in principle only. But the outcome of the Polya-Weyl wager showed that, for mathematicians, the rejection of impredicative definitions in analysis is not at all compelling in the same way. So the issue of whether the F-S characterization, or as you put it, "the Gamma0 thesis" is correct has to be taken on its own merits, if one is interested in it at all.
p.2, sec.1, 3d par. You say that the Gamma0 thesis "has been repeatedly and forcefully defended by its two major figures, Feferman and Kreisel. Many current authors simply assert it as a known fact." There are two "facts" at issue here: (UB) Gamma0 is an upper bound for the proof-theoretical strength of predicativity. (LB) It is a lower bound. Both Kreisel and I have raised critical questions about the proposed characterization at different stages, so it is not fair to say without qualification that we forcefully defended it. And others have raised questions, as you note here and there. And, after all, few logicians have been concerned with the characterization. We're not talking about the "passive" involvement of a big "scientific community" here (p.16). I think most people who have looked at it are persuaded by the autonomy picture and the result (UB) on the face of it. It has nothing to do with the complexity of the argument, which is now what one learns in straightforward Schütte-style infinitary proof theory after Epsilon0 as an upper bound to PA. That's just the bread and butter of the subject. Your objections to the (UB) result are not novel, as you yourself note. At the same time (curiously) you object to (LB) not as a result but for the way it has been proved. Of those thinkers on the subject who have accepted (UB) as patently correct, few have thought about (LB). I brought attention to the question of its justification in "A more perspicuous system for predicativity" [13].
p.4, 2nd par. up, "U(NFA) employs a patently impredicative least fixed point operator". This is completely wrong. The point is brought up again on p. 15 and I will address it there.
p.5, 1.3, par.1, "If we could show that A [a rational actor who has accepted some foundational stance] would accept every member of some set of statements S, then A should see this too and then be able to go beyond S, e.g. by asserting its consistency." There is a basic ambiguity here. It goes without saying that if A sees that it has accepted every member of S, then it should accept Con(S)--that's just an instance of the reflection principle for S. But this will not be the case if A comes to accept each member of S step by step, requiring a new exercise of reasoning at that step, and does not have a single act of reasoning that allows it to accept all of S. If one follows your line on this, it would appear that no foundational stance can be characterized by a formal system S, because if one makes it convincing that A ought to accept "all" of S, then A can go beyond S. So, there will be no complete characterization of finitism, no complete characterization of predicativity, etc. There will be no ordinal bound that can be established for predicativity.
p.7, you say that if one accepts the rule of inference (*) one should accept the corresponding generalized implication (**). A simple example where this kind of argument fails occurs in modal systems that have a rule of inference A/NA, where NA (or "box"A) says that A is necessary, but we don't have A->NA. Or take NA to be Prov('A') in arithmetic.
p.9(d), re my position on the characterizations of predicativity in "A more perspicuous..." using the systems P + Ex/P, "Reflecting on incompleteness" using the system Ref*(PA(P)), and "The unfolding of non-finitist arithmetic" using the system U(NFA), vs. the earlier characterization via progressions: you say that I nowhere openly repudiate the earlier systems. On the contrary, I said in the first of these that the latter make use of the prima-facie impredicative concepts of ordinal or well-ordering in their description, and the point of the work in [13] as in the succeeding papers is to show how that can be avoided. I did not repudiate the results of the earlier work which made the (UB) to predicativity plausible in the context of the history of the subject which led to the consideration of autonomous ramified progressions.
In view of this, your critiques of the earlier systems are moot, and I shall not deal with them.
pp.10-11, sec.1.6, the linked systems P + Ex/P. The reason for taking P to be the primary system and Ex/P an auxiliary system is that the existential quantifier over functions and predicates is not to be given first class status as a logical operator. Ex/P only serves to show how things may be established to exist, either directly or by construction from a prior existent. This is analogous to the notion of existence in finitism. See Gödel's early understanding of this in his Collected Works vol. III, p. 51: "Negatives of general propositions (i.e., existence propositions) are to have a meaning in our systme only in the sense that we have found an example but, for the sake of brevity, do not state it explicitly. I.e., they serve merely as an abbreviation and could be entirely dispensed with if we wished." In our case, these were dispensed with in the unfolding paper via the use of definedness as a basic pre-logical notion.
p.11, last par. Your proposed inference to Sigma-1-1 comprehension (and thence Pi-1-1 comprehension) can't be carried out in P, because analytic formulas are not in the language of P.
pp.12-14, sec. 1.7, the critique of Ref*(PA(P)). This approach was a way station in trying to see predicativity as one instance of the more general explanation of what one ought to accept if one has accepted given principles, and was not completely satisfactory conceptually through its use of a Kripkean partial truth predicate. But it was important for stressing the use of open-ended schematic systems and for illustrating the general program. It was superseded by the unfolding concept, so I shall not defend it further. But you have not understood (p. 13) how T and F are to be construed relative to an arbitrary definite predicate P.
p.15(b), "Way too strong. U(NFA) is flatly impredicative in two ways." The first is supposed to be Ax 7 (p.82) of the unfolding paper. This axiom simply says that we have a name for each basic predicate symbol P; our operations on names serve to generate names of expressions built up from P, and that are definite if P is definite, so this is completely unproblematic. The second way you criticize, "the really striking impredicativity...is its use of a least fixed point operator". But as you point out yourself in fn.10, the leastness is never used by us, and in any case, the apparent impredicativity here is completely eliminable, as it is in general for partial recursive functions by approximation from below; the standard proof is given op.cit. p. 80. In notes, Strahm and I have also reworked our approach using an untyped partial combinatory calculus instead; that is both formally simpler, yields the needed fixed points in a trivial way, and never requires the leastness condition. So there is no impredicativity here either, let alone "flatly".
p.16, 2nd full par. Your principal objection to the three systems is "a basic impredicativity involving the ability to substitute possibly meaningless formulas for free set variables." (And this is your objection to the way (LB) is established.) The essential applications of the substitution rule rule, to infer from A(P) the result of substituting B(t) for P(t) are those where B(t) simply says that t is defined and of a given type. This is not meaningless. Or at least you ought to grant it as being "intelligible" in your sense (sec. 2.3 ff) as distinct from being "meaningful", and thus something we can reason about.
p.16, last par. "...a properly functioning scientific community should be expected to debate and criticize major ideas, not to passively accept them, regardless of the stature of their author and the complexity of the argument. That this was not done in a serious way in the present case suggests that the community as a whole did not function in the way that it should have." Really! This reckless, grandiose statement is offensive and should be stricken. I don't know of any one who passively accepted the (UB) result for either reason, nor did the few who thought about the (LB) result and raised questions about it.
p.17. The "three basic principles" of your "mathematical conceptualism" are very vague and do not by themselves dictate the choices you make in developing your own proposal for what it is predicatively acceptable in the following pages.
p.18, 1st par, "...we do not expect to be able to fully formalize exactly how far we can go." My comment on p.5 above applies here too.
p.18, 2.2, "...intuitionistic logic [is] the appropriate took for general predicative reasoning." It was pointed out in "A more perspicuous..." and the unfolding paper, that the results hold equally well for the intuitionistic versions of the systems introduced there having Gamma0 as both upper and lower bound. I think your argument for the use of intuitionistic logic for reasoning about formulas which are not recognized in advance to have a definite meaning is a reasonable one, and so is your step to marry this to the numerical omniscience scheme (p. 19). Obviously, our own arguments hold for this logic intermediate between the classical and strictly intuitionistic logics.
pp. 25-26. Given any recursive total order < on omega and an extension S of pure 2nd order arithmetic in this logic, you define the iterated Tarskian truth theory of S along the < relation, Tarski<(S) to have a basic predicate symbol Acc and for each a in omega a symbol Ta for an a-times iterated truth predicate. Acc(a) is interpreted as: Ta is accepted and you have a rule of inference that allows you to pass from the provability of Acc(a) for any specific a to axioms for Ta that assert closure of the earlier axioms and rules of inference under Ta and in addition the Tarski T-scheme for it. Finally, Prog(Acc) is assumed. You say that if a predicativist accepts S he should also accept Tarski<(S). What justifies this? The predicativist must give meaning to all the symbols involved. With your interpretation, there is a circularity involved: Acc(a) means that Ta is accepted, but we don't know what Ta is until we know which b's are accepted. In fact, Acc(a) is just a stand-in for: the initial segment of the < relation determined by a is well-ordered, i.e. I(a). And then in order to say what Ta is, we need to say what all the Tb's are for b<a. And in order to do that we need to carry out a definition by transfinite recursion up to a. But one of your main objections to our analysis of predicativity (e.g. p.4, last par.) is that the step from transfinite induction up to an ordinal notation does not justify transfinite recursion up to that notation. As we know, iterated truth theories are equivalent to ramified theories, and so you are in effect working with here is an autonomous ramified progression, just what you railed against in an earlier section of the paper. The only difference seems to be that the logic is weakened to intuitionistic logic plus the NOS scheme, but we have already noted that that is an inessential restriction.
pp.26-30, sec. 2.8. Here you iterate the passage from a < relation to Tarski<(S) omega times, taking the < relation to be a standard one for the ordinals up to Gamma0. Taking an as a standard fundamental sequence for Gamma0, you prove TI(A,an) for successive n in the iterated theory by showing (Lemma 2.4, p. 27) how to go from n to n+1. You claim that the argument "finesses the induction versus recursion issue" by proving a stronger result, namely that TI applies to all formulas A not just sets. But that is only because, as I just noted, the induction => recursion is hidden in the semantics justifying your Tarski theories.
p.30. Finally you say that the omega iteration of Tarski theories just described ought to be accepted as a single theory, and that kind of step will allow you to capture the ordinal Gamma0 itself and far beyond. But that assumes that the predicativist accepts the general proposition: "If S is acceptable then for any recursive ordering < of omega, so also is Tarski<(S)." This is a higher order notion of acceptability which is not justified by your interpretations.
p.34, fn. 1. I had to laugh when I came to this after trying to wade through your systems, since here you also blame the failure of the mathematical community to go predicative on "the awkwardness of predicative systems [of the kind I have developed] in practice". Wait till they see these systems of yours! The informal system J2 of your paper [48] seems to me to be hardly more attractive, but any specific remarks I might want to make about that will have to wait for another day.
p.37, [17] and [23], 'Review' -> 'Revue'
p.37, the Shapiro volume has appeared, "The Oxford Handbook of the Philosophy of Mathematics and Logic", Oxford University Press 2005. My chapter, "Predicativity" is on pp. 590-624.
A final general point. You may not believe that informal notions of proof such as those of finitism and predicativity can be characterized formally. But if you do, the case of finitism is instructive. Kreisel characterized it by a system of strength PA and Tait characterized it by a system of strength PRA. What accounts for such different results? I have an informal explanation, namely that Kreisel accepts a concept of finitist ordinal (or well-ordering) that Tait does not accept. Strahm and I have set up a basic system FA of finitist arithmetic whose unfolding is equivalent in strength to PRA. I believe there should be a corresponding basic system for FA plus a finitist notion of well-ordering, whose unfolding is equivalent to PA. It may be that our notions of predicativity differ in much the same way, and that if you explain more clearly what mathematical conceptualism consists in, one can characterize it formally as the unfolding of a suitable system, of course much stronger than U(NFA).
Sincerely,
Solomon Feferman