Many thanks for your detailed and thoughtful criticism of my paper, "Predicativity beyond Gamma0". I give below a point-by-point response to your comments. However, this gets into a variety of issues of varying degrees of importance, so perhaps I should first summarize what I see as the key points of interest.
The three central assertions of my paper are the following:
1. All previously proposed formal systems for predicativity are too weak in the sense that anyone who accepted the informal principles motivating any of these systems would be able to grasp the global validity of that system and then move beyond it.
2. All previously proposed formal systems for predicativity are also too strong, because they all permit a predicatively illegitimate inference of an assertion of transfinite recursion from an assertion of transfinite induction --- and the ability to make such inferences is crucial for the well-ordering proofs which are alleged to establish predicative provability of all ordinals less than Gamma0.
3. Using transfinite hierarchies of Tarskian truth theories it is possible to legitimately establish the predicative provability of all ordinals less than Gamma0, and indeed of ordinals significantly larger than Gamma0.
I think the success of my paper as a whole essentially comes down to the success of these assertions, and you do contest all three of them, though in a rather cursory fashion in the first two cases. Indeed, your response to the first assertion does little more than reiterate an idea which I have extensively criticized (about A coming to accept each member of S step by step, requiring a new exercise of reasoning at that step), with no further explanation and without even acknowledging my critique of this idea. You very briefly answer the second assertion in a way that fails to address the key distinction between (in my terminology) meaningfulness and intelligibility.
It is only to the third assertion that you offer a substantial response, with your criticism of the semantics of my systems Tarski<(S). I don't completely understand this criticism, but it seems to rest on the premise that predicativists are not capable of reasoning about the concept of intelligibility. This is a bit puzzling because you evidently do agree that predicativists can reason about such concepts as truth and second order existence. So I wonder what basis you have for denying predicativists the ability to reason about intelligibility, if that actually is your position.
Now to the specific points you raise.
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 ...
That's a different question: I was commenting on the fact that virtually nobody is a predicativist nowadays. I suspect the F-S characterization has made it unacceptable to be one. After all, although predicativism was always a minority view, there was a definite tradition in the subject going from Poincare and Russell to Weyl to Wang and Lorenzen. It is hard to find anyone who openly advocated predicativism after the work on Gamma0 came out in the early 1960's. A likely reason for this is that "Gamma0 is sufficiently tame that it is simply hard to take seriously any approach to foundations that prevents one from recognizing ordinals at least this large" (p. 1).
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 ... 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.
Certainly it has to be taken on its own merits. I wonder where you get the idea that I think otherwise --- the paragraph from which you have quoted merely makes the point that if the Gamma0 thesis is false, this fact would have significant philosophical consequences, such as opening up the possibility that statements like the Cantor-Bendixson theorem and Kruskal's theorem may turn out to be predicatively provable. That is entirely separate from my actual criticism of the Gamma_0 thesis. I completely agree that the predicative unprovability, on the F-S characterization, of these statements is no argument against the F-S characterization.
p.2, sec.1, 3d par. ... 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.
I don't think my statement is "not fair" --- you did defend it, forcefully and at length --- but I'll be happy to add a qualification to the effect that you have raised critical questions (which is also true) if you wish. I already do indicate this in the last paragraph on page 11, the second paragraph on page 13, and extensively in footnote 11, but I don't mind saying it here too.
p.4, 2nd par. up, "U(NFA) employs a patently impredicative least fixed point operator". This is completely wrong.
(See below, discussion on page 15(b).)
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 ...
I don't think you read this sentence carefully enough --- the ambiguity you ascribe to it is not present. The premise is not that A sees that he has accepted every member of S, the premise is that we can see that he would accept every member of S; and the objection is that if we can see this then he ought to be able to see it too, which would then allow him to use a reflection principle to go beyond S.
... 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.
Well, that is essentially what I say immediately following the cited passage: "There are a variety of ways in which this objection could be overcome ... it may be possible to identify some special limitation in A's belief system which prevents him from grasping the validity of all of S at once despite his ability to accept each statement in S individually." But I then go on to explain why this would be a quite extraordinary claim, particularly in the case of the Gamma0 thesis. You offer no comment on this analysis and make no attempt to justify the claim.
The objection is, as you note that I note, not novel. Howard states it very persuasively in [24], for instance. Kreisel attempts to refute it in several places, in highly cryptic passages which, once one deciphers them, are clearly fallacious; I treat these attempts at some length in sections 1(a), (b), and (c) of my paper. In [11] you dispense with the issue with the comment "The most obvious objection to (1)* was discussed and answered by Kreisel", followed by a reference to [32]. But that answer of Kreisel was abandoned by him in his later paper [33], in favor of a highly speculative suggestion that also does not stand up to scrutiny.
It would be quite remarkable if there were some straightforward sequence of well-ordering proofs such that we could see that a predicativist would accept each proof in the sequence but he could not see this himself. I extensively refute all serious attempts to justify this kind of claim of which I am aware. This is one of the central arguments of my paper and your brief response does not seem to do justice to it.
If one follows your line on this, it would appear that no foundational stance can be characterized by a formal system S ...
This isn't really accurate; I explicitly list several ways in which the objection might be overcome. Whether this can actually be done depends on the details of the case at hand. My "line" is that it has never been convincingly done in the case of predicativism. I haven't thought about finitism.
p.7, you say that if one accepts the rule of inference (*) one should accept the corresponding generalized implication (**).
Actually, I say that a predicativist should not accept (*) because of the induction versus recursion problem, and I then ask if one did believe he could accept (*) why one would not also believe he could accept (**). This is followed by two pages of discussion, which you do not address, in which I analyze and refute three separate attempts of Kreisel to justify the (on its face, quite incredible) claim that predicativists can accept (*) but not (**). Your example from modal systems seems not very relevant to this discussion.
There are lots of situations where a deduction rule is valid but the corresponding implication is not. The fact that such cases exist does not go very far toward showing that this particular case is one of them.
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.
I wrote: "Feferman nowhere openly repudiates the earlier systems, and I read his remark in [14] as implying that the later systems are merely more `perspicuous' than the earlier ones because they do not assume that predicativists have any understanding of ordinals."
I am unclear as to whether you are complaining that this statement misrepresents you, and if so, how my characterization differs essentially from your own ("On the contrary, I said ...").
I also don't see why, if you do not repudiate the earlier work, my critiques of it are moot. Historically, the autonomous ramified progressions were a major step forward in that they introduced the important distinction between predicative definability and predicative provability of well-orderings. But they are fundamentally unsound in not respecting the predicative distinction between well-ordering in the sense of admitting induction and well-ordering in the sense of admitting recursion.
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 ...
This helps explain the intuitive motivation for P + Ex/P but does not answer the numerous detailed criticisms I made of that system. For example, why are we able to introduce a function symbol when the functional's uniqueness has been proven in P but not when its uniqueness has been proven in Ex/P?
You say that "Ex/P only serves to show how things may be established to exist". Does this mean that theorems of Ex/P which are not existence assertions are not to be belived? What if in the course of proving some existence statement I incidentally prove that some functional is unique --- should I believe it then? What if this step is essential to the proof of the existence statement?
I also argued that the predicate substitution rule of P + Ex/P is clearly impredicative and that your justification of this rule, if accepted, would in fact justify full second order comprehension. Your reponse to this point was the following comment:
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.
Of course not. But if one were to accept a substitution rule allowing one to infer B(X/C) from B(X) in the context of, say, pure second order arithmetic, this would imply full comprehension. So you somehow have to explain why such substitutions are legitimate when B(X) is a formula of P but not when B(X) is Sigma-1-1. Your one-sentence justification for the rule ("it may be argued that the (predicative) provability of B(X) establishes its validity also for properties whose meaning is not understood", [13], p. 92) is not satisfying because it does not explain why this should be the case only when B(X) is a formula of P and not more generally.
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.
Well, if P is taken to be definite then I suppose I can guess what you meant by "relativizing T and F to P". But then the substitution rule of Ref*(PA(P)) would be invalid since you allow substitutions for P which are not definite.
The use of open-ended schematic systems is very interesting, but it is also impredicative on its face in the fact that the schematic predicate symbol P is taken to range over formulas which may themselves contain P. This comment also applies to U(NFA).
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 problem is that elsewhere you use P as a schematic predicate symbol, with the interpretation that statements involving P are to be understood as schemas of true statements, one for each intelligible substitution instance. Ax 7 is not consistent with this interpretation.
On the other hand, if we interpret P in the way you suggest here, as ranging over definite predicates, this would render the substitution rule invalid. The same problem appears in [14], and you mention it there as a difficulty (if somewhat obliquely: "this may involve some equivocation between the notions of being definite and being determinate", with no further explanation, [14], p. 42), so I am surprised that you now feel it is "completely unproblematic". Essentially the same problem also occurs with regard to the substitution rule in [13]. ("In P we think of `X' as ranging over predicates recognized to have a definite meaning; this would not seem to admit the properties expressed by formulas of LEx", [13], p. 92.)
This is the central impredicativity which appears in some form in all of your systems. In every case you build a hierarchy over an arbitrary set (or, if you prefer, "definite predicate") and then infer that such hierarchies exist over arbitrary predicates. Yet the construction of the hierarchy is not valid for arbitrary predicates. In [13] you deal with this problem by essentially saying that anything provable for arbitrary sets can also be accepted for arbitrary predicates ([13], p. 92), and in [14] you say that "this substitution [of predicates for sets] accords with ordinary informal reasoning" ([14], p. 41). In [19] you pass over the difficulty without comment.
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 I go on to indicate that this impredicativity could be removed by dropping the minimality condition and switching to intuitionistic logic. As it stands, however, the system is impredicative in this respect.
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.
I don't understand this comment. The approximation from below for partial recursive functions involves a simple induction on omega; for your least fixed point operator it involves a generalized inductive definition, and that is impredicative.
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".
You now seem to be saying that U(NFA) can be modified so as to remove this impredicative aspect without sacrificing the well-ordering proof. I think that is true, as I said myself in footnote 10. It would not seem to justify your earlier comment that my assessment of the least fixed point operator as patently impredicative is "completely wrong".
I stand on my comment that the system U(NFA) as presented in [19] is patently impredicative in its use of a least fixed point operator (in addition to its other impredicative aspects).
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.
The distinction between "intelligible" (the statement's sense is understood) and "meaningful" (it has a definite truth value) is crucial. In your well-ordering proofs you derive a statement about P(t) under the assumption that P(t) is meaningful, then substitute a formula B(t) which is merely known to be intelligible.
If we could generally substitute intelligible formulas for meaningful formulas then we could infer (exists Y)(forall n)(n in Y <--> A(n)) for any formula A of second order arithmetic, i.e., full second order comprehension, from the predicatively valid statement (forall X)(exists Y)(forall n)(n in Y <--> n in X). A predicativist cannot accept this inference precisely because he cannot generally substitute intelligible formulas (A(n)) for meaningful ones (n in X).
This example is not artificial; it is exactly substitutions of this type which are used in all three systems to pass from induction to recursion.
p.16, last par. Really! This reckless, grandiose statement is offensive and should be stricken.
I know that saying "the community as a whole did not function in the way that it should have" will not make me any friends. However, the Gamma0 thesis has been the received view for forty years, and this despite not only slightly subtle problems like the induction versus recursion issue, but also the obvious problem, never satisfactorily answered, of being able to go beyond any given characterization --- as well as the numerous other difficulties I identify in my paper. Why did it require an outsider like me to point all of this out? Is there any explanation other than the failure of the foundations community to function properly in this case? If in saying this I come across as supercilious, or reckless and grandiose, I am genuinely sorry, but I felt it would have been disingenuous of me to say nothing.
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.
The criticism itself is vague. Can you give a specific example of a choice I make which is not dictated by the basic principles? Or can you suggest a way in which they could be made more precise?
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) ... 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.
Tarski<(S) involves a hierarchy of symbols which are not initially accepted as intelligible. However, the symbol Ta cannot actually be reasoned with in Tarski<(S) until a criterion convincing us of its intelligibility is satisfied. In other words, we have available a pool of potentially usable truth predicates about whose intelligibility we are able to reason.
Thus, in order to accept Tarski<(S) I do not first have to give meaning to all the symbols involved; I only need to recognize that any symbol will be given meaning before it is used.
You rhetorically ask "What justifies this?" but may not have noticed that I give a fairly detailed answer to that question on pages 29 and 30.
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.
I'm not sure what you mean by "we don't know what Ta is". Ta is a truth predicate referring to a well-defined family of formulas. If you mean that Ta is not (initially) intelligible, because some of the formulas to which it applies are not (initially) intelligible, that is true. So if you take the position that a predicativist has to give meaning to all of the symbols of Tarski<(S) before he can start using it, then I agree, he couldn't do this. However, as I just explained, that requirement is too strict because the system is set up in such a way that Ta cannot be used until it is recognized as intelligible.
Perhaps your point is just that we have to understand the predicate Acc before we can start using Tarski<(S). That is quite true. But if you are saying that we don't understand Acc until every Ta is intelligible, then again the requirement is too strict because it is supposed to be through Acc that we reason about the intelligibility of the Ta. It seems that your real claim is that predicativists cannot formally reason about intelligibility. But that seems strange because you evidently do agree that predicativists can reason formally about such concepts as truth and second order existence, and you do not explain why you think reasoning about intelligibility would be impredicative.
(I should add that if your objection were successful this wouldn't save the Gamma0 thesis --- if we can't even use Tarski<(S) then we seem to be stuck around gamma3, where (gamman) is the canonical sequence whose supremum is Gamma0.)
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.
I'm not sure what to do with this comment. An essential feature of my argument is the fact that I prove, in a higher system, the statement TI(A,an) for all formulas A of a lower system. I don't merely prove TI for sets, I prove it for statements that explicitly refer to the acceptability of Ta, so there is no step from transfinite induction to transfinite recursion. I don't know what it means to say that Acc(a) is "just a stand-in" for I(a).
Tarski<(S) is indeed analogous to a ramified theory, but this is not where the well-ordering proof takes place. It takes place in Tarski<omega(S), which has no analog in the analysis of autonomous ramified progressions.
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.
No. There's an important difference between your statement and what is actually needed. Yours ("the general proposition: `If S is acceptable ...') is indeed impredicative, as it refers to the general concept of acceptability and this is not a predicatively legitimate concept. If we could formally discuss acceptability of theories in general, we could set up a system which refers to its own acceptability in a circular fashion. (See the end of sections 2.3 and 2.8 for discussion of this point.)
What is actually needed is the ability to discuss, from the outside, the acceptability of a circumscribed family of theories. In my case I have an omega sequence of theories, Sn = TarskiGamma0n(Z1i), and I must be able to recognize that for any n, if Sn is acceptable then so is Sn+1. I suppose this is a "higher order notion" in some sense but I do not see what is impredicative about it nor why it is not justified by my interpretations. The alternative, that for each n a predicativist can separately infer the acceptability of Sn+1 from that of Sn via an unformalizable leap of intuition, but he is unable to grasp that passage from Sn to Sn+1 is generally valid, seems to me quite unbelievable.
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.
You seem to have read this footnote hastily. It explicitly refers to the J2 paper, not to the systems in the Gamma0 paper. The latter are obviously not intended to be used in formalizing core mathematics (what would a hierarchy of Tarskian truth theories have to do with that).
You interpret my comment about awkwardness as referring specifically to systems you developed, but that is not what I had in mind. As you know, predicative systems intended to be used to formalize core mathematics have been developed by many people, including Chihara, you, Grzegorczyk, Kondo, Lorenzen, Takeuti, Wang, Weyl, and Zahn. I was referring to all of these systems generally. (See line -4 on page 1 of my J2 paper for references.)
I do agree that the systems in my Gamma0 paper, especially the two later ones, are too complicated. I believe that further progress in predicatively proving stronger well-ordering statements will involve substantially simplifying my approach in some way.
Sincerely,
Nik Weaver