THE CONSISTENCY OF PREDICATIVE FRAGMENTS OF FREGE'S GRUNDGESETZE DER ARITHMETIK RICHARD G HECK JR As is well-known, the formal system in which Frege works in his Grundgesetze der Arithmetik (Gg) is formally inconsistent, Russell's Paradox being derivable in it. This system is, except for minor differences, full second-order logic, augmented by a single non-logical axiom, Frege's Basic Law V, which we may take to be:1 ∀F∀G [x(Fx) = x(Gx) ≡ ∀x(Fx ≡ Gx)] Reading 'x(Fx)' as 'the value-range of the concept F ', Basic Law V thus states that, for every F and G, the value-range of the concept F is the same as the value-range of the concept G just in case the F s are exactly the Gs. In Frege: Philosophy of Mathematics, Michael Dummett (1991, pp. 217–22) raises the question how the serpent entered Eden, that is, how we should understand the genesis of the contradiction in Frege's system. The standard view is that the inconsistency is simply to be blamed on Basic Law V. The problem, seen this way, is that Basic Law V requires for its truth that there be as many objects in the domain of the theory as there are concepts true or false of those objects, i.e., that the firstand second-order domains should be of the same cardinality: And that, as Cantor showed us, is quite impossible. Note, however, that this reflection shows only that the theory is unsatisfiable, that is, that it does not have a standard model. And one might wonder whether this explanation really answers Dummett's question, since it does not, or at least does not obviously, say why the theory ought to be inconsistent: why a contradiction should be derivable from Basic Law V. These two questions are not only different, but may need different answers, since the completeness theorem fails for second-order logic. Dummett's own view is that the blame is to be ascribed, not so much to Basic Law V, as to the impredicative character of Frege's theory, in particular, to his acceptance of an unrestricted comprehension schema. In his paper 'Whence the Contradiction?', George Boolos (1998) questions Dummett's view and argues in favor of the more standard line. In the course of doing this, Boolos raises a number of technical questions Published in History and Philosophy of Logic 17 (1996), pp. 209–20. 1Basic Law V in fact concerns the value-ranges of functions in general, not just the extensions of concepts, but we shall ignore this point here. 1 PREDICATIVE FRAGMENTS 2 which, he suggests, would need to be answered before the issue can be resolved. The first question is, quite simply, whether the predicative fragment of Frege's theory is consistent: Dummett's claim would obviously be untenable if it were not. The second is how strong this theory is, assuming that it is consistent: For only if it is a reasonably strong theory, only if, say, some reasonable fragment of arithmetic can be developed within it, will it be plausible to place the blame on impredicative comprehension, rather than on Basic Law V. My goal in the present paper is to answer the first of these two questions, by showing that both the simple and ramified predicative fragments of Frege's theory are indeed consistent. At present, the second question remains open. Though I shall show that 'bounded arithmetic', I∆0, is relatively interpretable in the simple predicative fragment (and that somewhat stronger theories are, too), it is as yet unknown just how strong it might be.2 1. SOME REMARKS ON SECOND-ORDER LOGIC Terence Parsons (1995) has shown that the first-order fragment of Frege's formal theory is consistent. The first-order fragment of Frege's theory is axiomatized by the single axiom schema: x(A(x)) = x(B(x)) ≡ ∀x(A(x) ≡ B(x)) Here, A(x) and B(x) are (first-order) formulae which may contain arbitrarily many free variables other than 'x'. The proof to be given of the main result of the present note is a straightforward extension of Parsons's argument. There are some niceties concerning the formulation of the systems we intend to study. Let us begin with matters syntactic. The language of the first theory we shall be discussing is that of simple predicative second-order logic: We have the usual logical symbols (including identity) and individual constants and variables. We also allow predicate constants of each number of argument-places, but, for simplicity, we restrict ourselves to second-order variables of one argument-place.3 The notions of a term and formula of the language are defined by simultaneous induction. Object-variables are terms; sentential constants are formulae. If P is an n-place variable or predicate constant, and if t1, . . . , tn 2The probelm was open when this paper was written but has now been answered definitively (Visser, 2009). 3The extension to richer languages poses no difficulties of principle. Adding variables of more argument-places requires almost no change to the proof given below: The domain, for n-ary variables, is to contain all sets denoted by formulae A(x1, . . . , xn) containing no variables other than the xi free. A richer language still allows the formation of terms of the form ' x1, . . . , xn(A(x1, . . . , xn))', governed by analogues of Basic Law V. Such terms can be assigned references simply by being included in the inductive stipulation used in the proof below. PREDICATIVE FRAGMENTS 3 are terms, then pPt1, . . . , tnq is a formula; and, if A(x) is a formula, not containing 'x' bound, then px(A(x))q is a term. And, as usual, if A and B are formulae, then so are their truth-functional compounds and quantifications with respect to any variable not already bound in them. Only such things are terms and formulae. Terms of the form px(A(x))q we call value-range terms or, for short, vr terms. We now need an axiomatization of simple predicative second-order logic. As axioms and rules, we may take any complete set of axioms and rules for first-order logic with identity and add, first, an axiom-schema of universal instantiation for second-order variables: ∀uA(u)→ A(v) Here u and v are second-order variables; A(u), some formula in which u is free for v. Also, we need a rule of universal generalization that is entirely analogous to the usual first-order rule. (Note that we may, if we like, merely state the axioms and rules of universal instantiation and generalization so as not to distinguish firstfrom second-order variables. It is in this that the strong analogy between firstand secondorder logic consists.) Versions of second-order logic differ in strength according to the strength of their respective comprehension axioms. In full, or standard, secondorder logic, every instance of the following is an axiom: ∃F∀x[Fx ≡ A(x)] Here, A(x) may be any formula not containing 'F ' free. In simple predicative second-order logic, on the other hand, only instances in which A(x) contains no bound second-order variables are axioms. Note that A(x) may contain arbitrarily many free second-order variables.4 Note also, importantly, that A(x) may contain arbitrarily many value-range 4Frege's formulation of second-order logic is somewhat different from this: He gets the effect of comprehension by means of a rule of substitution. In such a formulation of standard second-order logic, the rule of substitution states that, if A(v) is a theorem, then the result of substituting any formulaB(x) for v inA(v) is also a theorem-subject, of course, to the usual sorts of restrictions. In such a formulation of simple predicative second-order logic, one requires the formulae B(x) not to contain bound second-order variables. PREDICATIVE FRAGMENTS 4 terms, so long as those terms do not contain bound second-order variables.5,6 The sole 'non-logical' axiom of the theories we shall be considering is to be, as has been said, a version of Frege's Basic Law V, which may, in the context of a second-order theory, be formulated either as the axiom schema x(A(x)) = x(B(x)) ≡ ∀x(A(x) ≡ B(x)) or as the single, universally quantified axiom ∀F∀G [x(Fx) = x(Gx)) ≡ ∀x(Fx ≡ Gx)] As additions to standard second-order logic, the scheme and axiom are, as it is easy to see, equivalent. In the context of predicative secondorder logic, however, the schematic version of Basic Law V is stronger than the single, quantified axiom. One instance of the schema is, of course, x(Fx) = x(Gx)) ≡ ∀x(Fx ≡ Gx) from which the single axiom follows by universal generalization. However, there is no apparent way to derive, say, the instance x(∃F (ẑ(Fz) = x ∧ ¬Fx) = x(Hx) ≡ ∀x [(∃F (ẑ(Fz) = x ∧ ¬Fx) ≡ Hx] 5It is for this reason that the consistency of the theory under discussion here was not already settled by John Bell (1999). Bell proves, following Parsons, that the 'Fregean extension' of any first-order theory that has infinite models is consistent. The Fregean extension of a theory is the result of adding all instances of Basic Law V and closing. (I should emphasize that the following reasoning is not due to Bell and that his result is slightly more general.) One might think, at first glance, that this result proves more than it does. Predicative second-order logic can be treated as if it were a certain first-order theory, and that first-order theory certainly has infinite models. Hence, its Fregean extension is consistent, by Bell's result. But, and here is the important point, this does not imply that the theory under discussion in the text is consistent. To see that there is a problem, note that standard second-order logic can also be treated as if it were a certain first-order theory that has infinite models. Its Fregean extension is, by Bell's result, consistent. But standard second-order logic plus Basic Law V is not formally consistent, as Russell showed. What then is going on? The Fregean extension of a theory, in this sense, is merely the result of adding Basic Law V to it, and here one is to think of the variable-binding, termforming operator '^' as an addition to the language of the theory. What this means, in the case of second-order logic, is that the comprehension axioms are in no way altered, so no comprehension axiom contains a value-range term. The Fregean extension of second-order logic is thus a weaker theory than what I am here calling 'second-order logic augmented by Basic Law V'. 6Oddly enough, comprehension axioms that contain second-order quantifiers within value-range terms will be theorems of the predicative fragment being described. Consider, for example, the concept: ξ = ẑ(∃F (z = ŵ(Fw)). By comprehension: ∃F∀x[Fx ≡ x = y]. So, by universal generalization: ∀y∃F∀x[Fx ≡ x = y]. But then, by universal instantiation: ∃F∀x[Fx ≡ ẑ(∃F (z = ŵ(Fw)). The trick is thus to replace the value-range terms by variables, generalize, and then instantiate. PREDICATIVE FRAGMENTS 5 from the universally quantified axiom without appeal to impredicative comprehension. What we shall be proving here is thus that simple, predicative secondorder logic, augmented by the schematic version of Basic Law V, is consistent. Before proceeding with the proof of this theorem, however, it is worth considering why Russell's Paradox is not derivable in this theory. Following Frege, membership may be defined as follows: An object x belongs to a value-range y if, and only if, y is the value-range of a concept under which x falls. Formally: x ∈ y df ≡ ∃F [y = ẑ(Fz) ∧ Fx] For any formula A(x), we can prove:7 (i) y ∈ x(A(x))→ A(y) We can also prove a restricted version of the converse of (i): (ii) A(y)→ y ∈ x(A(x)) for formulae A(y) not containing bound second-order variables. Thus: 1. A(y) 2. ∃F∀x[Fx ≡ A(x)] Comprehension 3. ∀x[Fx ≡ A(x)] 4. Fy ≡ A(y) 5. x(Fx) = x(A(x)) (3), Law V 6. x(Fx) = x(A(x)) ∧ Fy (1,4,5) 7. y ∈ x(A(x)) The reason (ii) is not provable in full generality is that (2) is an instance of predicative comprehension only if A(x) does not contain second-order quantifiers. So (ii) is provable only for such formulae.8 So naïve abstraction (iii) y ∈ x(A(x)) ≡ A(y) is provable only for formulae A(x) not containing second-order quantifiers. 7Thus: y ∈ x(A(x)) ∃F [x(A(x)) = x(Fx) ∧ Fy] Def ∈ x(A(x)) = x(Fx) ∧ Fy ∀x[A(x) ≡ Fx] Law V A(y) ≡ Fy A(y) Note that the proof uses no instances of comprehension and so goes through even in the most trivial of second-order theories. 8If we adopt the alternate definition of membership x ∈ y df ≡ ∀F [y = ẑ(Fz)→ Fx] precisely the opposite situation obtains. We can prove (ii) for all formulae A(x), but can prove (i) only for formulae not containing second-order quantifiers. PREDICATIVE FRAGMENTS 6 Now, consider the Russell class x(x /∈ x). By (i), we can prove x(x /∈ x) ∈ x(x /∈ x)→ x(x /∈ x) /∈ x(x /∈ x) But we can not prove x(x /∈ x) /∈ x(x /∈ x)→ x(x /∈ x) ∈ x(x /∈ x) since 'x 6∈ x' (abbreviates a formula that) contains a second-order quantifier.9 It is worth emphasizing a few points about the foregoing discussion. First, the term denoting the Russell class is well-formed: There is no restriction upon the formation of value-range terms in the theory we are considering. Second, the Russell class exists, and it provably does not belong to itself. Third, the instances of Basic Law V needed in the derivation of the Paradox are axioms of this theory; more generally, all instances of Basic Law V are axioms of this theory, and so all valuerange terms are governed by Basic Law V. What prevents the derivation of the Paradox is precisely the lack of a particular instance of comprehension.10 2. PROOF OF THE MAIN THEOREM The main result of the present note is thus the Theorem. Simple, predicative second-order logic, augmented by the schematic version of Basic Law V, is consistent. To prove this, we provide a model whose domain is the natural numbers. To complete the specification of the model, we must (1) fix denotations for all value-range terms and (2) fix a domain for the second-order quantifiers. The proof will proceed in five stages. First, following Parsons's original construction (Parsons, 1995), we shall fix denotations, relative to every interpretation of free variables contained in them, for all valuerange terms that contain no second-order variables. Second, we shall fix 9Indeed, given the relevant instance of comprehension: ∃F∀x[Fx ≡ x /∈ x] a contradiction is forthcoming. So the negation of this formula is provable. More generally, this shows that second-order logic with comprehension for Σ11 formulas is inconsistent. Adopting the alternative definition of membership mentioned in the previous note, one can also reproduce Russell's paradox, if we have comprehension for Π11 formulas. Since this paper was published, it has been shown, by Fernando Ferreira and Kai Wehmeier that this is best possible: It is consistent to assume comprehension for ∆11 formulas (Ferreira and Wehmeier, 2002). 10These remarks are intended to facilitate comparison between the present system and those obtained by Nino Cocchiarella (1992). The systems he studies are related to, but quite different from, those investigated here. His restrictions on comprehension, i.e., his various restrictions on his prinicple CP∗λ, also restrict what 'nominalized predicates' (value-ranges) exist. PREDICATIVE FRAGMENTS 7 the domain of the second-order quantifiers and show that this suffices to fix denotations for all value-range terms containing free, but no bound, second-order variables. Third, we shall show that all instances of comprehension are true. Fourth, we shall fix denotations for the remaining value-range terms, those containing bound second-order variables. Finally, we shall check that the construction verifies all instances of the schematic version of Basic Law V. Fix the interpretations of any constants. We shall assume, for convenience, that among the constants are denumerably many numerals n each of which denotes the corresponding natural number.11 The assumption allows us to disregard free first-order variables in what follows. For example, the denotation of a term 'x(A(x, y1, . . . , yk))', under the assignment of n1, . . . , nk to the variables may simply be taken to be the denotation of the term: x(A(x, n1, . . . , nk)). 2.1. Value-range terms not containing second-order variables. Define the rank of a vr term as follows: If A(x) contains no vr terms, let the rank of px(A(x))q be 0. If A(x) contains a vr term and the term of greatest rank that it contains is of rank n, let the rank of px(A(x))q be n+ 1. Order all vr terms in an ω×ω sequence, where the value-range terms of each rank form an ω-sequence, and, for any vr term t, each term preceding it is of a rank less than or equal to that of t itself. Let J(m,n) be some pairing function. Define J0(m,n) = 2× J(m,n). To the first vr term, assign the natural number J0(0, 0) as its denotation. For induction, let t be some vr term in the ordering and assume that we have assigned denotations to all prior terms. Assume, further, that, if px(C(x))q and px(D(x))q precede t, then px(C(x))q and px(D(x))q have been assigned the same denotation if, and only if: For every term n, C(n) is true iff D(n) is. (If so, say that C(x) and D(x) are equivalent.) For our inductive stipulation, we must assign some denotation to t, and we must show that, if px(C(x))q and px(D(x))q precede or are identical with t, then C(x) and D(x) are equivalent if, and only if, px(C(x))q and px(D(x))q have been assigned the same denotation. Let t be px(A(x))q. We intend to assign t, as its denotation, the denotation assigned to the term u, if u is some prior term px(B(x))q such that B(x) is equivalent to A(x). (By hypothesis, the denotations of all such terms are the same.) If there is no such term, we assign to t the number J0(m,n), where m is the rank of t and n is the smallest number k such that J0(m, k) has not already been assigned as the denotation of some vr term. (Note that there will always be such a number k.) The acceptability of the definition depends only upon our having specified enough to 11If the predicative second-order theory in this language, whose axioms are the instances of the schematic version of Basic Law V, is consistent, so is the corresponding theory in the original language. PREDICATIVE FRAGMENTS 8 determine, for any term px(B(x))q prior to t, whether A(x) and B(x) are equivalent. But that we have. For only value-range terms contained in A(x) and B(x) could possibly be problematic, all such terms are of rank less than that of t, and hence all such terms have been assigned a denotation. We must now check that, if px(C(x))q and px(D(x))q precede or are identical with t, then C(x) andD(x) are indeed equivalent if, and only if, px(C(x))q and px(D(x))q have been assigned the same denotation. The crucial case is that in which one of these terms is t. Suppose that the former is: Thus, it is px(A(x))q. But then A(x) is equivalent to D(x) if, and only if, px(A(x))q is co-referential with px(D(x))q, by construction. 2.2. The domain of the second-order quantifiers. We fix the domain of the second-order quantifiers as follows. A set α is to belong to the domain if, and only if, it is the extension of some formula A(x) that contains no free variables other than 'x' and that contains no secondorder variables at all. The extensions of all such formulas have been fixed by the assignment of denotations to closed value-range terms in the last section. We now fix denotations for all value-range terms containing free, but no bound, second-order variables. We make use here of the following fact. Fact. Given any interpretation I of the free variables contained in a formula A(x), there is a formula A′(x), containing no free second-order variables and no bound second-order variables not contained in A(x), to which A(x) is equivalent, under that interpretation of the second-order variables. (Say that A(x) and A′(x) are I/x-equivalent, if so.)12 Proof. Fix an interpretation I. Suppose that A(x) contains free variables V1, . . . , Vn, and let αi be assigned to Vi by I. Since the αi are in the domain, there are formulae αi(x), containing no free variables other than 'x' and no bound second-order variables at all, whose extensions are the αi. Let A′(x) be the result of substituting the αi(x) for the V i in A(x). Then A′(x) is I/x-equivalent to A(x).  Now, if px(A(x))q is a vr term containing free, but no bound, secondorder variables, there is a formula A′(x), containing neither free nor bound second-order variables, that is I/x-equivalent to A(x). Assign to px(A(x))q, as its denotation relative to I, that already assigned to px(A′(x))q. 12Carefully note the order of the quantifiers: The claim is not that there is a fixed formula A′(x) to which A(x) is I/x-equivalent for all I, but that, for each I, there is a corresponding such formula. PREDICATIVE FRAGMENTS 9 2.3. All comprehension axioms are true. The comprehension axioms are all instances of ∃F∀x[Fx ≡ A(x)] where A(x) contains neither free 'F ' nor any bound second-order quantifier. Say that α is the I-extension of A(x) if for every n, n ∈ α iff A(n) is true under I. To show that all comprehension axioms are true under every interpretation, we must show that, for every interpretation I of its free variables, the I-extension of A(x) is contained in the second-order domain. As above, let A′(x) be a formula containing neither free nor bound second-order variables that is I/x-equivalent to A(x) and therefore has the same I-extension as A(x). But the extension of A′(x) is in the domain, by definition. Since every set in the second-order domain is the extension of some formula, we can henceforth ignore terms containing free second-order variables, as we have been ignoring terms containing free first-order variables: The value, under an interpretation I, of a term or formula containing free second-order variables will just be the value under I of the formula or term resulting from substituting formulas whose extensions are the sets I assigns to the respective free variables. 2.4. Value-range terms containing second-order quantifiers. Due to obvious analogies with 2.1, we merely sketch this part of the proof. Say that a vr term px(A(x))q is of degree 0 if it contains no secondorder quantifiers. Say that it is of degree 1 if it does, but contains no vr terms that themselves contain bound second-order quantifiers; otherwise, let the degree of px(A(x))q be one greater than the greatest degree of any vr term contained in it. Order the vr terms by degree in an ω× ω sequence. Let K(m,n) be 4 × J(m,n) + 1. The foregoing has assigned denotations to all terms of degree 0. Assume we have done the same for all terms prior to some term t, i.e., px(A(x))q, of degree greater than 0 and assume, as above, that, for any terms px(C(x))q and px(D(x))q prior to t, those terms have the same denotation just in case C(x) and D(x) are equivalent. As before, we assign to t, as its denotation, that of any prior term px(B(x))q such that B(x) is equivalent to A(x), if there is such a term, and we assign as denotation K(m,n), where m is the rank of t and, for all k < n, K(m, k) has already been assigned as denotation to some vr term. That enough has been stipulated to determine, for each term px(B(x))q prior to px(A(x))q, whether B(x) and A(x) are equivalent may be shown as in 2.1. The demonstration that, for any terms px(C(x))q and px(D(x))q prior to or the same as t, those terms have the same denotation just in case C(x) and D(x) are I/x-equivalent, is also similar to the proof of the corresponding result in 2.1. PREDICATIVE FRAGMENTS 10 2.5. Every instance of Basic Law V is true. Let px(C(x))q and px(D(x))q be value-range terms. In the ω × ω ordering of all the vr terms, either px(C(x))q is prior to px(D(x))q or conversely. Suppose the former. Then, as just said, px(C(x))q and px(D(x))q have the same denotation just in case C(x) and D(x) are equivalent. But p∀x[C(x) ≡ D(x)]q is true just in case C(x) and D(x) are equivalent. 3. THE CONSISTENCY OF THE RAMIFIED PREDICATIVE FRAGMENT OF FREGE'S SYSTEM In the language of ramified second-order logic, we have, besides our familiar variables 'F ', 'G', and the like, also variables of denumerably many other types, 'F 1', 'G1', etc., 'F 2', 'F 3', and the like. We say that variables superscripted with the numeral n are of type n, and we re-describe our previous variables as having been of type 0. Ramified second-order logic has, as comprehension axioms, all instances of ∃Fn∀x[Fnx ≡ A(x)] where A(x) contains no bound variables of type greater than or equal to n, and no free variables of type greater than n. By iterating the construction given above, the consistency of ramified predicative second-order logic, augmented by Basic Law V,13 may be proven. As the proof is very similar in spirit to that just given, we merely sketch it here. Assume that we have so far specified a model that assigns domains to variables of types less than or equal to n and that: (i) Consistently with Basic Law V, assigns denotations to all vr terms containing arbitrarily many bound and free variables of types less than or equal to n, relative to any interpretations of those variables; (ii) Verifies all comprehension axioms for types less than or equal to n. (The base case is then that of simple predicative second-order logic.) We then: (1) Take as the type-n+1 domain the extensions of all formulasA(x) containing no bound variables of type higher than n and no free variables other than 'x'. (2) Show, as in 2.2, that this suffices to fix denotations for all vr terms containing bound variables of types less than or equal to n and free variables of types less than or equal to n+ 1, i.e., that it allows us to take care of free variables of type n+ 1. (3) Show, as in 2.3, that all comprehension axioms for type n + 1 hold. (4) Show, as in 2.4 and 2.5, how denotations can be assigned, consistently with Basic Law V, to all vr terms containing bound and free variables of type n+ 1 and below. 13Note that Basic Law V is again to be formulated as a schema: We make no typerestrictions upon what may occur in the formulae occuring in Basic Law V, other than that they be well-formed. PREDICATIVE FRAGMENTS 11 4. INTERPRETING Q IN THE PREDICATIVE FRAGMENT It is, in retrospect, not so surprising that, without impredicative instances of comprehension, no contradiction is forthcoming from Basic Law V. One might wonder, however, just where the proof given above would break down were we to attempt to extend it to a proof of the consistency of standard second-order logic, augmented by Basic Law V. The answer is that it breaks down at the second stage, when we attempt to assign a domain to the second-order variables which will both verify all comprehension axioms and allow us to fix denotations for value-range terms containing free but no bound second-order variables. In the first part, we had assigned denotations to terms containing no second-order variables: In the extension to terms containing free second-order variables, it was crucial that, for every set which might interpret such a variable, there was a formula of the language whose extension it was. It is tempting to suppose that the difficulty is that, if the first-order domain is infinite, then, in a model of standard second-order logic, there should simply be too many sets in the second-order domain for there to be, for each of them, a formula whose extension it is. However, this is mistaken:14 To prove the consistency of standard second-order logic, plus Basic Law V-i.e., to prove that no contradiction can be proven in the theory-it would suffice to show that there was a non-standard model of second-order logic that validated Basic Law V. Non-standard models of second-order logic need not have, as their second-order domains, the full power set of the first-order domain, only a second-order domain that verifies the comprehension axioms. (These are the so-called Henkin models.) In the predicative case, we stipulated that the domain was to contain exactly the extensions of formulae which appear in comprehension axioms and that contain no second-order variables at all. The proof that all comprehension axioms are true in the model then depended upon our substituting the formula defining a given set in the second-order domain for the free variable to which that set had been assigned. But no similar trick will work in the case of standard second-order logic: If the domain contains only classes defined by first-order formulae, that will not verify all instances of comprehension, for the formulae appearing in those axioms may contain bound second-order quantifiers. Nor can we just say that the second-order domain is to contain the extensions of all formulae appearing in the comprehension axioms. If we have not said what the second-order domain is to be, not enough has 14It would be better to remark that Cantor's theorem is provable in second-order logic. But the situation here is complicated: A version of the theorem can, in fact, be proven in predicative second-order logic, and yet the predicative fragment, which associates a unique object with every 'concept' is consistent. The reason is that the relation the theorem asserts not to exist is definable only impredicatively. PREDICATIVE FRAGMENTS 12 been said to determine the extensions of such formulae; we do not know what the extension of '∃F (. . . F . . . )' is unless we already know what the domain of the second-order quantifiers is to be. Perhaps this adds some force to Dummett's claim that Russell's Paradox arises in Frege's system because of a circularity inherent in impredicative second-order quantification. As Boolos points out, however, this should not lead us to claim, without additional argument, that the impredicativity of second-order logic is responsible for the contradiction: Unless the resulting theory is reasonably strong, it will be hard to blame the contradiction on the impredicativity of Frege's logic. The predicative fragment is at least non-trivial: The axioms of Robinson arithmetic, Q, can be relatively interpreted in it, which implies that all recursive functions can be represented in the predicative fragment and that it is essentially incomplete and undecidable. Since Edward Nelson has proved that I∆0, and even somewhat stronger theories, are interpretable in Q, it follows that these theories are also interpretable in the predicative fragment.15 It may well be that one can do a little better still, but I do not now know how much better.16 Nonetheless, the predicative fragment is a natural theory for someone with strongly finitist inclinations. The initial goal is to intepret a version of Q formulated, not with function-symbols 'Sξ', 'ξ+η', and 'ξ×η', but with relation-symbols 'Pξη', 'A(ξ, η, τ)', and 'M(ξ, η, τ)'. Once this theory has been interpreted, we can interpret Q in its usual form by means of Russell's theory of descriptions. The axioms of this version of Q, which we might call QR, are: P1 ∀x∃y(Pxy) P2 Pxy ∧ Pxz → y = z A1 ∀x∀y∃z(A(x, y, z)) A2 A(x, y, z) ∧A(x, y, w)→ z = w 15For formulations and proofs of the relevant results, see Hájek and Pudlák (1993, pp. 366–71). I∆0 is Q with induction for 'bounded' formulae, that is, formulae all quantifiers contained in which are of the form '∃x < y' or '∀x < y'. The stronger theories in question have axioms asserting the totality of, so to speak, fragments of exponentiation whose totality is not provable in I∆0. The really hard part of Nelson's proof, that the theory Q+ is interpretable in Q, can be skipped here, since the proof to be given shows directly that Q+ is interpretable in the predicative fragment. 16Shortly after this paper was published, John P. Burgess and Allen Hazen (1998) showed that the fragment of primitive recursive arithmetic with function-symbols only for addition, multiplication, and exponentiation is also interpretable in ramified predicative second-order logic with the axiom of infinity and so is interpretable in the predicative fragment. For this result and more, see Burgess's book Fixing Frege (Burgess, 2005). More recently, Albert Visser (2009) settled the question of the strength of the predicative fragment definitively. Basically: It is very weak, far weaker than primtive recursive arithmetic (aka, IΣ1). But it does interpret a perfectly reasonable fragment of arithmetic. PREDICATIVE FRAGMENTS 13 M1 ∀x∀y∃z(M(x, y, z)) M2 M(x, y, z) ∧M(x, y, w)→ z = w Q1 Pxz ∧ Pyz → x = y Q2 ¬Px0 Q3 x 6= 0→ ∃y(Pyx) Q4 A(x, 0, x) Q5 A(x, y, z) ∧ Pzz′ ∧ Pyy′ ∧A(x, y′, w)→ w = z′ Q6 M(x, 0, 0) Q7 M(x, y, z) ∧A(x, z, w) ∧ Pyy′ ∧M(x, y′, v)→ w = v Q1-Q4 and Q6 are self-explanatory. The first six axioms express existence and uniqueness conditions for the predicates 'Pξη', 'A(ξ, η, τ)', and 'M(ξ, η, τ)' and so guarantee that they serve to define total functions. Q5 says that, if z′ is the successor of the sum of x and y, and if w is the sum of x and the successor of y, then z′ is w: That is, it expresses what 'x+Sy = S(x+y)' expresses in the more usual formulation of Q. Similar remarks apply to Q7. One striking fact about the interpretation of the axioms of QR in the predicative fragment is that it can be given in terms of Frege's own definition of number. Let 'Eqx(Fx,Gx)' abbreviate the usual formula expressing that F and G are equinumerous, i.e.: ∃R[∀x∀y∀z∀w(Rxz ∧Ryw → x = y ≡ z = w)∧ ∀x(Fx→ ∃y(Rxy ∧Gy) ∧ ∀y(Gy → ∃x(Rxy ∧ Fx)] Then we define: Nx :Fx df= x(∃G[x = ŷ(Gy) ∧ Eqy(Fy,Gy)]) Thus, the number of Fs is the extension of the concept: ξ is the extension of a concept equinumerous with F (Gg, v. I, §40). The idea is then to prove relativizations of the axioms of QR to the formula 'Num(x)', expressing that x is a number, which we define, again following Frege, as follows: Num(x) df ≡ ∃F [x = Ny :Fy] The definitions of '0' and 'Pξη' are then, again, just Frege's: 0 df = Nx :x 6= x Pmn df ≡ ∃F∃y[n = Nx :Fx ∧ Fy ∧m = Nx : (Fx ∧ x 6= y)] The definitions of 'A(ξ, η, τ)', and 'M(ξ, η, τ)' require a definiton of ordered pairs, for which we can use a version of the usual definition:17 <a, b> df = x(x = ŷ(y = a) ∨ x = ŷ(y = a ∨ y = b)) 17Frege does define ordered pairs Gg, v. I, §144, though differently (and impredicatively). PREDICATIVE FRAGMENTS 14 The proof of the ordered pair axiom <a, b> = <c, d> ≡ a = c ∧ b = d is then straightforward. We then define addition and multiplication as the cardinality of the disjoint union and Cartesian product, respectively: A(a, b, c) df ≡ ∃F∃G{a = Nx :Fx ∧ b = Nx :Gx∧ c = Nx : [∃y (Fy ∧ x = <ẑ(z 6= z), y>) ∨ ∃y (Gy ∧ x = <ẑ(z = z), y>)]} M(a, b, c) df ≡ ∃F∃G[a = Nx :Fx ∧ b = Nx :Gx ∧ c = Nx :∃y∃z(Fy ∧Gz ∧ x = <y, z>] This last definition is not Frege's: In fact, he never defines multiplication in Grundgesetze. Nor does he offer a formal definition of addition, though it is clear he had something like the present definition of addition in mind (Gg, v. II, §33). The proofs of the axioms then proceeds as follows. First, we prove Hume's Principle (HP): Nx :Fx = Nx :Gx ≡ Eqx(Fx,Gx) The proof is essentially Frege's proof (Gg, v. I, §§54–69),18 which does not use impredicative axioms of comprehension. It is worth rehearsing the proof. Basic Law V and the definition of number give us: Nx :Fx = Nx :Gx ≡ ∀x{∃H[x = ŷ(Hy) ∧ Eqy(Fy,Hy)] ≡ ∃H[x = ŷ(Hy) ∧ Eqy(Gy,Hy)]} The work is to show that the right-hand side is equivalent to: Eqy(Fy,Gy). All we really need to know is that equinumerosity is an equivalence relation. The proof is straightfoward-Frege outlines it already in Die Grundlagen-so one need only check that no appeal to impredicative comprehension is needed. So suppose that Eqy(Fy,Gy). We want to show: ∀x{∃H[x = ŷ(Hy) ∧ Eqy(Fy,Hy)] ≡ ∃H[x = ŷ(Hy) ∧ Eqy(Gy,Hy)]} Left-to-right: Suppose ∃H[x = ŷ(Hy) ∧ Eqy(Fy,Hy)], e.g., x = ŷ(Zy) ∧ Eqy(Fy, Zy). We need to show that ∃H[x = ŷ(Hy)∧Eqy(Gy,Hy)]. But we have both Eqy(Fy,Gy) and Eqy(Fy, Zy), so the symmetry and transivity of equinumerosity give us Eqy(Gy,Zy). So x = ŷ(Zy)∧Eqy(Gy,Zy), and existential generalization completes the proof. The other direction is obviously similar. Suppose, then, that: ∀x{∃H[x = ŷ(Hy) ∧ Eqy(Fy,Hy)] ≡ ∃H[x = ŷ(Hy) ∧ Eqy(Gy,Hy)]} 18The two directions of HP are Theorems 32 and 49. For discussion of their proofs, see my paper "Frege's Principle" (Heck, 1995). PREDICATIVE FRAGMENTS 15 We want to show that Eqy(Fy,Gy). By the reflexivity of identity and equinumerosity: ŷ(Fy) = ŷ(Fy) ∧ Eqy(Fy, Fy) so, generalizing: ∃H[ŷ(Fy) = ŷ(Hy) ∧Eqy(Fy,Hy)]. By the supposition, then, ∃H[ŷ(Fy) = ŷ(Hy) ∧ Eqy(Gy,Hy)]. Fix such an H. Then, by Law V, ∀x(Fx ≡ Hx), and we already know that Eqy(Gy,Hy). But it is easy to show, predicatively, that equinumerosity is extensional, in the sense that: ∀x(Fx ≡ Hx) ∧ Eqy(Gy,Hy)→ Eqy(Gy, Fy) So Eqy(Gy, Fy), and symmetry completes the proof.. With HP in hand, we can then prove relativizations of axioms P2 and Q1–Q3. Again, the proofs are just Frege's proofs of Theorems 71, 89, 108, and 107 of Groundgesetze, respectively, which do not use impredicative comprehension. Proofs of axioms A1, A2, Q4, and Q5, concerning addition, are in the appendix: The proofs of those concerning multiplication are similar and are omitted. The last remaining axiom is P1, whose relativization asserts that every number has a successor: Num(x)→ ∃y[Num(x) ∧ Pxy] Frege's proof of this claim will not work, since it appeals to impredicative comprehension.19 However, there is a much easier proof, as follows. The proof depends upon the two facts: Eqx[Fx,∃z(Fz ∧ x = <w, z>)] ¬Fy → P [Nx :Fx,Nx : (Fx ∨ x = y)] To prove the former, note that the relation Rξη that correlates these two concepts one-to-one will just be: Fξ ∧ η = <w, x>, which exists by comprehension. The latter follows immediately from the definition of 'Pξη'. Now suppose that a is a number, a = Nx :Fx. By comprehension, for some G, Gx ≡ ∃y(Fy ∧ x = <ẑ(z 6= z), y>). By the mentioned fact, G is equinumerous with F . So, by HP, a = Nx :Fx = Nx :Gx. But ¬G(ẑ(z 6= z), since, for any x and y, <x, y> 6= ẑ(z 6= z). So P [Nx :Gx,Nx : (Gx∨x = ẑ(z 6= z)) and so P [a,Nx : (Gx∨x = ẑ(z 6= z)). And Nx : (Gx∨x = ẑ(z 6= z)) is a number, by comprehension. That, then, completes the interpretation of QR in the predicative fragment. I have argued elsewhere that it was important to Frege that he not rely upon Basic Law V in his proofs of the basic laws of arithmetic, that those proofs should appeal only to Hume's Principle, but for inessential 19That said, it turns out that the existence of successor can be proven in a ramified predicative version of Frege arithmetic, and, modulo the need to prove various versions of reducibility, the proof is essentially Frege's (Heck, 2011). PREDICATIVE FRAGMENTS 16 uses of value-ranges for technical convenience (Heck, 1993, 1995, 2005). What we have just seen is that, had Frege been willing to appeal to Basic Law V in his proof that every natural number has a successor, he could have given a much simpler proof than he did and, moreover, proven that every number has a successor, not just that every natural number has one. If one refuses to appeal to Basic Law V, the proof of the more general claim has to wait until later; Frege's proof depends upon his Theorem 483, that Nx :x = x is Dedekind infinite, whereas the proof given above appeals only to HP and the definitions of ordered pairs and predecession. The existence of the proof discussed above, which is hardly so difficult that Frege could not be expected to have seen it, thus constitutes additional evidence for the claim mentioned.20 APPENDIX I shall here sketch proofs of the axioms of QR concerning addition. As said above, the proofs of the axioms concerning multiplication are similar-although rather more tedious. Write '∅' for 'ẑ(z 6= z)' and 'V ' for 'ẑ(z = z)'. Write, e.g., '<∅, F>x' for: ∃y(Fy ∧ x = <∅, y>). For A1, let a and b be numbers, a = Nx :Fx, b = Nx :Gx. Let c = Nx : (<∅, F>x ∨ <V,G>x). By comprehension, for some H, ∀x[Hx ≡ <∅, F>x∨<V,G>x)]; and so, by HP, Nx :Hx = Nx : [<∅, F>x ∨<V,G>x)]. So c is a number and A(a, b, c), by definition. For Q4, let a be a number, say, Nx :Fx. By A1, for some z, A(a, 0, z), so there are F and G such that: a = Nx :Fx ∧ 0 = Nx :Gx ∧ z = Nx : [<∅, F>x ∨<V,G>x] It follows from HP and the definition of '0' that ¬∃x(Gx). By logic, then, ¬∃x∃y(Gy∧x = <V, y>), that is, ¬∃x(<V,G>x) and so<∅, F>ξ∨<V,G>ξ is (co-extensional with and so) equinumerous with <∅, F>ξ which is, by a fact used earlier, equinumerous with Fξ. Hence, by HP, a = Nx :Fx = Nx :<∅, F>x = z. A2 is a relatively trivial consequence of this fact: ¬∃x(Fx ∧Gx) ∧ ¬∃x(F ′x ∧G′x) ∧ Eqx(Fx, F ′x) ∧ Eqx(Gx,G′x)→ Eqx(Fx ∨Gx,F ′x ∨G′x) The proof is straightforward and is, in fact, given by Frege (Theorem 469): Just put the maps that establish thatEqx(Fx, F ′x) andEqx(Gx,G′x) together. 20Thanks to John Burgess and Allen Hazen for discussion, and to Michael Resnik for comments that much improved the paper. Special thanks to George Boolos, for inspiring my interest in this problem and for helping me to understand Parsons's proof. PREDICATIVE FRAGMENTS 17 Now, suppose that A(a, b, c) and A(a, b, d). Then, by the definition of A(ξ, η, τ), there are F and G, and H and J , such that: a = Nx :Fx ∧ b = Nx :Gx ∧ c = Nx : [<∅, F>x ∨<V,G>x] a = Nx :Hx ∧ b = Nx : Jx ∧ c = Nx : [<∅, H>x ∨<V, J>x] Now <∅, F>ξ is equinumerous with Fξ and so, by HP, with Hξ and so with <∅, H>ξ; <V,G>ξ is equinumerous with Gξ and so with Jξ and so with <V, J>ξ. Since <∅, F>ξ and <V,G>ξ are disjoint, as are <∅, H>ξ and<V, J>ξ,<∅, F>ξ∨<V,G>ξ is equinumerous with<∅, H>ξ∨<V, J>ξ, and then HP implies that c = d. For Q5, suppose that A(a, b, c), Pcc′, Pbb′, and A(a, b′, d). It will suffice to show that Pcd, since then it will follow from P2 that c′ = d. By the various definitions, we have: a = Nx :Fx ∧ b = Nx :Gx ∧ c = Nx : [<∅, F>x ∨<V,G>x] a = Nx :F ′x ∧ b = Nx :Hx ∧ d = Nx : [<∅, F ′>x ∨<V,H>x] b′ = Nx :H ′x ∧H ′y ∧ b = Nx : (H ′x ∧ x 6= y) Define: Jx df ≡<∅, F ′>x ∨<V,H ′>x z df =<V, y> I claim that: d = Nx : Jx ∧ Jz ∧ c = Nx : (Jx ∧ x 6= z) from which it follows, by the definition of 'Pξη', that Pcd. Note that Jz, since H ′y. Now, d = Nx : [<∅, F ′>x ∨ <V,H>x]; so, by HP, it is enough to establish the first conjunct to show that <∅, F ′>ξ ∨ <V,H ′>ξ is equinumerous with<∅, F ′>ξ∨<V,H>ξ. And since<V,H ′>ξ and <∅, F ′>ξ are disjoint, as are <V,H>ξ and <∅, F ′>ξ , it is enough to show that <V,H>ξ is equinumerous with <V,H ′>ξ. But, as above, <V,H ′>ξ is equinumerous withHξ and so withH ′ξ and so with<V,H>ξ. Since c = Nx : [<∅, F>x ∨ <V,G>x], it will suffice to establish the third conjunct to show that <∅, F>ξ ∨ <V,G>ξ is equinumerous with Jξ ∧ ξ 6= z. Now, 'Jx ∧ x 6= z' just means: [<∅, F ′>x ∨<V,H ′>x] ∧ x 6= z If <∅, F ′>z, then for some y, F ′y∧<V, y> = <∅, y>, which is impossible, so Jx ∧ x 6= z iff: <∅, F ′>x ∨ [<V,H ′>x ∧ x 6= z] Since H ′y ∧ z = <V, y>, <V,H ′>z, <V,H ′>ξ is equinumerous with H ′ξ, and b = Nx :H ′x, we have: b′ = Nx :<V,H ′>x∧H ′z∧Nx : (<V,H ′>x∧x 6= z) = Nx : (<V,H ′>x∧x 6= z) PREDICATIVE FRAGMENTS 18 Thus, P [Nx : (<V,H ′>x ∧ x 6= z), b′], by definition; but then, by Q1, Nx : (<V,H ′>x∧x 6= z) = b = Nx :Gx. But then, by HP, <V,H ′>ξ∧ξ 6= z is equinumerous with Gξ. And <∅, F ′>ξ is equinumerous with <∅, F>ξ, so<∅, F>ξ∨<V,G>ξ is equinumerous with<∅, F ′>ξ∨[<V,H ′>ξ∧ξ 6= z] and so to Jξ ∧ ξ 6= z. REFERENCES Bell, J. (1999). 'Finite sets and Frege structures', Journal of Symbolic Logic 64: 1552–6. Boolos, G. (1998). 'Whence the contradiction?', in R. Jeffrey (ed.), Logic, Logic, and Logic. Cambridge MA, Harvard University Press, 220–36. Burgess, J. P. (2005). Fixing Frege. Princeton NJ, Princeton University Press. Burgess, J. P. and Hazen, A. (1998). 'Arithmetic and predicative logic', Notre Dame Journal of Formal Logic 39: 1–17. Cocchiarella, N. (1992). 'Cantor's power-set theorem versus Frege's double correlation thesis', History and Philosophy of Logic 13: 179–201. Dummett, M. (1991). Frege: Philosophy of Mathematics. Cambridge MA, Harvard University Press. Ferreira, F. and Wehmeier, K. F. (2002). 'On the consistency of the ∆11CA fragment of Frege's Grundgesetze', Journal of Philosophical Logic 31: 301–11. Frege, G. (1964). The Basic Laws of Arithmetic: Exposition of the System, ed. and tr. by M. Furth. Berkeley CA, University of California Press. (1970). Translations from the Philosophical Writings of Gottlob Frege, Geach, P. and Black, M., eds. Oxford, Blackwell. (1997). The Frege Reader, Beaney, M., ed. Oxford, Blackwell. (Gg). Grundgesetze der Arithmetik. Hildesheim, Georg Olms Verlagsbuchhandlung. Translations of Part I are in Frege 1964, and of portions of Part III, in Frege 1970. Extracts appear in Frege 1997, 194–223. Hájek, P. and Pudlák, P. (1993). Metamathematics of First-order Arithmetic. New York, Springer-Verlag. Heck, R. G. (1993). 'The development of arithmetic in Frege's Grundgesetze der Arithmetik', Journal of Symbolic Logic 58: 579–601. (1995). 'Frege's Principle', in J. Hintikka (ed.), From Dedekind to Gödel. Dordrecht, Kluwer, 119–42. (2005). 'Julius Caesar and basic law V', Dialectica 59: 161–78. (2011). 'Ramified Frege arithmetic', Journal of Philosophical Logic 40: 715–35. Parsons, T. (1995). 'On the consistency of the first-order portion of Frege's logical system', in W. Demopoulos (ed.), Frege's Philosophy of Mathematics. Cambridge MA, Harvard University Press, 422–31. PREDICATIVE FRAGMENTS 19 Visser, A. (2009). 'The predicative Frege hierarchy', Annals of Pure and Applied Logic 160: 129–53.