Navigation – Plan du site

AccueilNuméros26-1VariaPlural Frege Arithmetic

Résumés

Dans [Boccuni 2010], un fragment prédicatif du blv de Frege augmenté de la quantification plurielle illimitée de Boolos interprète pa2. Le principal inconvénient de cette axiomatisation est qu’elle ne récupère pas Frege Arithmetic (fa), en raison des restrictions imposées aux axiomes. Le but du présent article est de montrer comment [Boccuni 2010] peut être étendu de manière cohérente afin d’interpréter fa et par conséquent pa2 d’une manière qui soit parallèle à celle de Frege. Ce faisant, le système présenté sera mis en comparaison avec le système pe dans [Ferreira 2018] et quelques différences pertinentes entre les deux seront mises en évidence.

Haut de page

Texte intégral

1 Plural Grundgesetze

  • 1 See, for instance, the famous debate between Boolos and Dummett on the cause o (...)

1Frege’s Grundgesetze der Arithmetik is notoriously inconsistent. So-called Russell’s paradox arises from Frege’s Basic Law V (blv) and the impredicative second-order comprehension axiom that accompanies it. There may be no general agreement on which one of the axioms involved in the inconsistency is the real culprit.1 Nevertheless, as far as Frege’s Grundgesetze are concerned, the fact of the matter is that full second- or higher-order comprehension and full Basic Law V jointly lead to inconsistency.

  • 2 See [Burgess 2005, § 2.6], [Ferreira & Wehmeier 2002], [Heck 1996], and [Wehme (...)

2Quite recently, some fragments of Frege’s Grundgesetze were proved consistent, i.e., [Ferreira & Wehmeier 2002], [Heck 1996], [Wehmeier 1999]. Heck deploys predicative comprehension [Heck 1996], while both [Ferreira & Wehmeier 2002] and [Wehmeier 1999] adopt Image -comprehension. Their major shortcoming is that they interpret only very weak, though non-trivial, subsystems of arithmetic, like Robinson’s Q.2

3More recently, [Boccuni 2010] proposed to augment Heck’s predicative fragment of Frege’s Grundgesetze in [Heck 1996] by Boolos’ plural quantification—see e.g., [Boolos 1985]. The resulting axiomatic system, i.e., Plural Grundgesetze (pg), is shown to interpret pa2. The axioms of pg are a Plural Comprehension Principle

plc :xxx(x ≺ xx ↔ φx),

  • 3 In [Boccuni 2010] a different notation is used for plural formulæ, i.e., xηX, meaning “x(...)

where φx does not contain xx free;3 a Predicative Comprehension Principle

prc :Fx(Fx ↔ φx),

  • 4 See [Boccuni 2010] and [Boolos 1985] for considerations supporting the claim that (...)

where φx contains neither F free, nor free plural variables, nor bound second-order variables;4 and a schematic formulation of Basic Law V :

v :  {x : φx} = {x : ψx} ↔ ∀x(φx ↔ ψx).

  • 5 In pg, [Ferreira 2018], and in the system presented in this article, concepts (...)
  • 6 In [Ferreira 2018], the system pe is presented, which consists of two rounds o (...)

4The restrictions on the formulæ permitted in the extension-terms are exactly the same restrictions imposed on the right-hand side of prc. By this strategy, pg, in a rather Fregean spirit, guarantees that there is a one-to-one correspondence between concepts and extensions.5 This, nevertheless, cripples the system to the effect that, though it recovers pa2, it does not interpret Frege Arithmetic fa. This latter consists of full second-order logic and Hume’s Principle (hp) : ∀F, G(#F = #GF ≈ G) which says that the number of the Fs is identical with the number of the Gs just in case F and G are equinumerous. In fact, a Fregean definition of the number operator # in terms of extensions, which is crucial for recovering fa from blv, requires that bound second-order variables be allowed in the scope of the extension operator. This dictates that the very definition of # is not available in pg, let alone the derivation of so-called Frege’s Theorem, namely the derivation of appropriate formulations of second-order Peano axioms from fa. This is contested also in [Ferreira 2018] and [Hewitt 2018]. Thus, the aim of the present article is twofold: to provide a consistent extension of pg so as to recover fa, and, by that, to respond to [Ferreira 2018]’s and [Hewitt 2018]’s criticism, on the one hand; and, on the other, to highlight some interesting differences between the resulting system and [Ferreira 2018].6

  • 7 The same considerations mentioned in fn. 4 above apply also to prc in vimp.
  • 8 Modulo a translation of pe’s second-orderly impredicative fragment into vimp’s (...)

5pg’s limitation can be easily overcome by restricting the formulæ allowed within extension-terms only to those not containing free plural variables. The resulting system will be shown to be consistent and capable of interpreting fa. Now, the new version of axiom v, call it v*, will be schematic and such that the formulæ allowed within the abstraction operator {:} can contain (i) bound plural variables; (ii) both free and bound second-order variables; (iii) but no free plural variables at all. Call the resulting system vimp, since impredicative second-order formulæ are allowed in extension-terms. Also, vimp preserves pg’s axioms plc and prc, restricted as above.7 From this, it should be clear that [Boccuni 2010]’s pg and [Ferreira 2018]’s pe are subsystems of vimp.8

  • 9 Also in [Ferreira 2018] there is no one-to-one correspondence between (predicative, let (...)
  • 10 See [Tennant 2017] on these and other issues connected with logicism.

6The main aim of the present article is merely technical. On the one hand, it will be proved that one of the restrictions imposed on pg’s v and, other things being equal, on pe’s blv and predicative comprehension can be consistently lifted. On the other, it will be proved that fa can be interpreted in the resulting system. Nevertheless, it is interesting to mention a philosophical issue. There might be several desiderata a Fregean foundation of arithmetic based on blv might be expected to satisfy—consistency being an obvious pre-requisite. These might be, possibly among others: the preservation of a one-to-one correspondence between concepts and extensions; the interpretation of full second-order arithmetic; the interpretation of full second-order arithmetic on the basis of Frege’s definitions of the mathematical notions necessary to prove Frege’s Theorem. As said, in pg the one-to-one correspondence between concepts and extensions is preserved. Furthermore, pg has enough mathematical strength to interpret full pa2, in which natural numbers are defined à la Zermelo on the basis of the empty extension {x : x ≠ x} and the singleton operation. On the other hand, by lifting the restriction concerning bound second-order variables in v*, vimp loses the one-to-one correspondence between concepts and extensions. The up-side is that, unlike pg, vimp recovers pa via fa, i.e., by a Fregean definition of the number operator # and by deriving a formulation of hp from v*—which cannot be done in pg.9 With respect to the aforementioned desiderata, each approach has nice advantages and clear shortcomings. So, depending on which among the above desiderata is more fundamental, if any, one might prefer pg over vimp or the other way around. I am not going to take a stand on this here. But it is worth mentioning that a case can be made in favour of pg over vimp, if the one-to-one correspondence between concepts and extensions is deemed crucial, and one rests content with any derivation of second-order Peano axioms. On the other hand, vimp or pe would be preferable over pg, if pa2 were to be recovered in a way as faithful as possible to Frege’s, while at the same time the one-to-one correspondence between concepts and extensions were not deemed essential to a Fregean foundation of arithmetic.10

2 Consistency

  • 11 Recall that in vimp, just like in pg, bound second-order variables are not all (...)

7Being vimp an extension of pg and pe in which one or more restrictions on the axioms are lifted, and being both pg and pe consistent [see Boccuni 2011, Ferreira 2018], the first worry to address concerns the consistency of vimp. The consistency result in what follows, then, is the main result of this article. As a matter of convenience, I will rely on pg’s consistency proof, which implies the consistency of the fragment of vimp that is equivalent with pg. This fragment consists of all instances of v* not containing bound second-order variables, all instances of prc since the restrictions imposed by [Boccuni 2010] are the same imposed on prc in vimp, and all instances of plc not containing extension-terms containing bound second-order variables. What we need to prove is that: (i) all instances of v* containing bound second-order variables hold—i.e., the extension-terms introduced by those instances have denotations; (ii) and all instances of plc containing extensions-terms with bound second-order variables hold.11

8On the basis of this result, the overall strategy will be:

  1. to recap the consistency proof of pg—i.e., of the aforementioned fragment of vimp;
  2. to prove that all extension-terms containing bound second-order variables have denotations;
  3. to prove that all instances of v* containing extension-terms with bound second-order variables hold in the model;
  4. to prove that all instances of plc containing extension-terms containing bound second-order variables hold in the model.

2.1 The consistency of pg’s twin theory

9Let us consider the fragment of vimp that is equivalent with pg. The model of pg in [Boccuni 2011] will also be a model for such a fragment:

  1. First, [Boccuni 2011] fixes the first-order domain, namely ω, and the domain for plural variables, namely ℘(ω); and provides denotations for the extension-terms not containing second-order variables at all, but possibly containing bound plural variables, in § 4.1 and § 4.1.1. In line with [Heck 1996], this is accomplished by the definition of a function J0(m,n) as 2J(m,n), where J(m,n) is a pairing function assigning a natural number to each ordered pair of natural numbers (m,n). Recall that free plural variables are not allowed in extension-terms both in pg and in vimp.12
  2. Secondly, [Boccuni 2011, § 4.2] fixes the domain for the second-order variables, namely a set π(ω) containing all subsets of the first-order domain whose defining formula contains no free variables of any kind nor bound second-order variables (it may contain bound plural variables).
  3. Thirdly, [Boccuni 2011, § 4.2.1] provides denotations for extension-terms containing free second-order variables in line with [Heck 1996, § 3.2].
  4. Then, [Boccuni 2011, § 4.3] shows that all instances of blv containing no bound second-order variables hold in this model—the same holds for all instances of v* containing no bound second-order variables.
  5. Then, [Boccuni 2011, § 4.4] shows that all instances of prc hold in this model.
  6. Finally, [Boccuni 2011, § 4.5] shows that all instances plc hold in this model.

10This model is also a model for the fragment of vimp corresponding to pg. We need to extend this interpretation so that all instances of v* containing extension-terms with bound second-order variables hold—i.e., the corresponding extension-terms have denotations; and all instances of plc containing these latter extension-terms hold—still, as a matter of convenience I will prove that plc holds.

2.2 Extension-terms containing bound second-order variables

11This section closely follows [Heck 1996, § 3.4]. Let an interpretation I be as above, i.e., the domains for first-, second-, and plural variables are ω,π(ω), ℘(ω), respectively.

12Let the degree of an extension-term {x : Ax} be 0 if, and only if, Ax is a formula of the language of vimp containing no bound second-order variables at all. It is of degree 1 if, and only if, it does, but it contains no extension-terms containing bound second-order variables. In general, an extension-term {x : Ax} is of degree n if, and only if, the greatest degree of any extension-term contained in it is n − 1.

13Let us arrange the extension-terms by degree in an ω × ω-sequence, where the extension-terms of each degree form an ω-sequence and, for each extension-term t, each term preceding it is of degree less than or equal to that of t itself. Let K(m,n) be a function defined as 4J(m,n) + 1, where J(m,n) is as above. Previously, the consistency proof for the fragment of vimp corresponding to pg has assigned denotations to all extension-terms of degree 0. Let us assume we have done the same for all terms preceding a term t = {x : Ax} of degree greater than 0, and let us assume that, for any extension-terms {Bx} and {Cx} preceding t in the sequence, those terms have the same denotation just in case Bx and Cx are equivalent under I with respect to x. We assign to t, as its denotation, that of any preceding term {Dx} such that Dx is equivalent to Ax under I with respect to x, if there is such a term; if there is no such term, we assign to t as its denotation K(m,n), where m is the rank of t, n is the degree of t, and, for all nK(m,k) has already been assigned as denotation to some extension-term, but K(m,n) has not.

14Check now that, if {Bx} and {Cx} precede or are identical with t, then Bx and Cx are equivalent under I with respect to x if, and only if, {Bx} and {Cx} have been assigned the same denotation. The case in which {Bx} and {Cx} precede t in the sequence is covered by the previous assumption. Now, let = {Bx}. Since t is {Ax} by previous assumption, the denotations of the terms {Ax} and {Bx} are identical. Then, Ax and Cx are equivalent if, and only if, {Ax} and {Cx} have been assigned the same denotation by construction via the function K(m,n).

2.3 All instances of v* containing bound second-order variables are true in this model

15This section closely follows [Boccuni 2011, § 4.3], and [Heck 1996, § 3.5].

Theorem 1. Every instance of v* containing bound second-order variables holds in this model.

Proof. v* : {x : φx} = {x : ψx} ↔ ∀x(φx ↔ ψx),

  • 13 Instances containing free second-order variables and bound plural variable (...)

where φ and ψ are restricted as above.13

  • 14 Where x is their sole free variable.
  • 15 The proof goes analogously if {Bx} precedes {Ax} in the ω × ω-sequence.

Let {Ax} and {Bx} be extension-terms, such that Ax is equivalent to φx and Bx is equivalent to ψx.14 Let us assign the denotations of {Ax} and {Bx} respectively to {φx} and {ψx} as their denotations. From the previous section, in the ω×ω-sequence either {Ax} is prior to {Bx}, or conversely. Suppose {Ax} precedes {Bx}, then they have the same denotation just in case Ax ↔ Bx under I with respect to x. So, if Ax ↔ Bx, then φx ↔ ψx as well. Finally, the right-hand side of v*, i.e., x(φx ↔ ψx), is true just in case φx and ψx are equivalent.15

  • 16 Since pe is a subsystem of vimp, the consistency of vimp impli (...)

16Given that also all instances of plc are true in this model, since plural variables vary over the full power set of ω, from the previous constructions it follows that vimp is consistent.16

3 Frege Arithmetic and Frege’s Theorem

17The aim of this section is twofold. First, we need to prove that Frege Arithmetic fa can be interpreted in vimp; secondly, that Frege’s Theorem is implied by vimp. Both goals can be easily achieved. As mentioned earlier, [Ferreira 2018]’s pe is a subsystem of vimp. Since pe interprets fa and derives Frege’s Theorem, so does vimp.

  • 17 The Weak Reducibility Theorem in [Ferreira 2018] states that, if x is a natural number, (...)

18Still, there are two issues worth investigating. First, it is instructive to see how vimp recovers fa, given the balance between plural and second-order resources in order to retain consistency. Secondly, the derivation of Frege’s Theorem in vimp relies on the Weak Reducibility Theorem by [Ferreira 2018],17 which is crucial to prove the Successor Axiom in pe and vimp. The recovery of fa will be investigated in § 3.1. In § 3.2, the Successor Axiom will be derived, in order to make clear where weak reducibility is at work and why it is necessary, and highlight some differences with [Ferreira 2018]; whereas, for the sake of brevity, all other Peano axioms will not be derived, since they follow in pe and therefore in vimp.

3.1 fa

  • 18 Given its formulation, in vimp hp is restricted to prc-definable concepts. We’ll see this poses (...)

19First of all, it has to be shown that an axiomatic formulation of hp, i.e., #F = #G ↔ F ≈ G, is a theorem of vimp. As a matter of fact, in [Heck 1996] hp follows in a predicative system for Frege’s blv. Since [Heck 1996] is a subsystem of vimp, hp follows also in this latter theory.18

20In a standard Fregean setting with extension-terms, the definitions of the equinumerosity relation ≈ and of the number operator # require second-orderly impredicative resources. Also other notions necessary for recovering fa require such resources: i.e., predecessor, ancestral, and the concept of natural number.

  • 19 Boolos’ plural logic is monadic, so as it stands it cannot be used to define the equin (...)

21In vimp, the delicate balance between plural and second-order resources, mirrored by the restrictions on the axioms, requires that some definitions are provided in terms of second-order quantification, while others are defined in terms of plural quantification. This has to be done, because, on the one hand, free plural variables are not allowed in the scope of the extension operator: so, for instance, # cannot be defined by plural resources, since this would require allowing for plural parameters within extension-terms. On the other hand, second-orderly definitions in vimp are restricted to prc-definable concepts and relations. Suppose we define ≈ in terms of an existentially quantified second-order formula ∃R… as it is usually done. That would be a formula indeed allowed in extension-terms in vimp, but at the same time the relations quantified over would be, on the basis of the restrictions imposed on prc, only the predicatively definable ones, so the definition of ≈ would not involve the class of all bijections, but only the class of predicative bijections. But if equinumerosity is defined in terms of plural quantification, then the equinumerosity notion can be defined in terms of all pluralities, since plc has no restrictions at all:19 for any formulæ φ, ψ of the language of vimp,

Definition 1 (≈)

φ ≈ ψ ≔ ∃ xx(∀ y(ϕy → ∃!x(ψx ∧ (x,y) ≺ xx)) ∧ ∀y(ψy → ∃!x(ϕx ∧ (y,x) ≺ xx)))

Also, for any second-order variable F, the #-operator is defined as follows:

Definition 2 (#)

#F ≔ {x : ∃ G(x = {y : Gy} ∧ G ≈ F)}.

From the definitions provided so far, the axiomatic formulation of hp from above follows in vimp.

22The other three fundamental notions to recover fa are the notions of zero, predecessor, and natural number. The first one is straightforward, since it utilises a valid instance of prc, i.e., ∃Fx(Fx ↔ x ≠ x). Call this concept Empty, and provide the definition of zero: 0  #Empty.

23Since prc alone, due to the restrictions concerning bound second-order variables, cannot define the notions of predecessor, ancestral and natural number because of their irreducible impredicativity, plc will have to do the job. In what follows, I will focus on the first and the third.

  • 20 For the sake of clarity, I will use the following notational convention : (...)

24The notion of predecessor, provided by a valid instance of plc, is given in terms of pluralities and #-terms:20

Definition 3 (Predecessor)

x precedes y: (x,y) ≺ pp ≔ ∃Fu(Fu ∧ y = #F ∧ x = #[z.Fz ∧ z ≠ u])

25In order to move on to the definition of natural number, also the definitions of the notions of hereditary, ancestral, and weak ancestral are needed. Those are easily obtained by plural quantification. In particular, Hereditary: The plurality ss is hereditary in the plurality rr: Her(ss,rr) ≔ ∀x,y ((x,y) ≺ rr → (x ≺ ss → y ≺ ss)); Ancestral: x comes before y in the rr-series: (x,y) ≺ rr*≔ ∀ss(∀z ((x,z) ≺ rr → z ≺ ss) ∧ Her(ss,rr) → y ≺ ss); Weak Ancestral: (x,y) ≺ rr≔ (x,y) ≺ rr* ∨ x = y.

26Finally, the notion of natural number is defined by a valid instance of plc in terms of the weak ancestral pp+ of the predecessor:

Definition 4 (ℕ). x ≺ ℕ ≔  (0,x) ≺ pp+

3.2 Frege’s Theorem

27The above definitions are sufficient for deriving Frege’s Theorem, namely a derivation of second-order Peano axioms in vimp that mirrors Frege’s. Of course, in vimp second-order Peano axioms are proved in the following plural formulations:

(PA1) 0 ≺ ℕ

(PA2)x,y(x ≺ ℕ ∧ (x,y) ≺ ppy ≺ ℕ).

(PA3)x,y,z(x ≺ ℕ ∧ y ≺ ℕ ∧ z ≺ ℕ ∧(x,y) ≺ pp ∧ (x,z) ≺ ppy = z)

(PA4)x,y,z(x ≺ ℕ ∧ y ≺ ℕ ∧ z ≺ ℕ ∧(x,z) ≺ pp ∧ (y,z) ≺ ppx = y)

(PA5) ¬ ∃x (x ≺ ℕ ∧(x,0) ≺ pp)

  • 21 The Successor Axiom.

(PA6)x(x≺ ℕ → ∃ y(y ≺ ℕ ∧ (x,y) ≺ pp)).21

  • 22 The Principle of Mathematical Induction.

(PA7)xx (0 ≺ xxHer(xx,pp) → ∀ x(x ≺ ℕ → xxx)).22

28As mentioned, in what follows, I will focus only on pa6, since in pa6 the application of [Ferreira 2018]’s weak reducibility comes into play.

Theorem 2. PA6. The Successor Axiom: ∀ x(x ≺ ℕ → ∃ y(y ≺ ℕ ∧ (x,y) ≺ pp)).

29A standard strategy to prove the Successor Axiom in fa requires the proof of the so-called Lemma on Successors, i.e., ∀x((x,#[z.(z,x) ≺ pp+]) ≺ pp), which states that every number x precedes the number of the individuals z in the weak precedessor-series ending with x. Still, the existence of numbers is delivered by hp. This latter is restricted to prc-definable concepts, to the effect that the supposed #-term “#[z.(z,x) ≺ pp+]” is impermissible by the definition of # and by prc. Thus, in vimp  hp cannot prove the existence of the number #[z.(z,x) ≺ pp+], since the term “#[z.(z,x) ≺ pp+]”, on the basis of the definition of the notion of predecessor pp, contains bound second-order variables and thus is hp-impermissible—see Definition 3.

  • 23 This can be accomplished by a definition of Fregean finitude, which mirror (...)
  • 24 In order to prove the Successor Axiom, [Ferreira 2018] proves a stronger theorem, i.e. (...)

Still, [Ferreira 2018]’s pe implies a Weak Reducibility Theorem, stating that, if x is a natural number, there is a (predicative) concept that is co-extensive with the formula y ≤ x—where ≤ is defined impredicatively. The Weak Reducibility Theorem, in turn, is implied by a Finite Reducibility Theorem.23 In pe, it is indeed the Weak Reducibility Theorem that underlies the proof of the Successor Axiom.24 And that is also what will be used in vimp.

Proof. By Mathematical Induction.

First of all, for the sake of convenience but without loss of generality, let us define:

  • 25 The right-hand side formula is a valid instance of plc.

Definition 5 (≤): xyx ≺ ℕ ∧ y ≺ ℕ ∧ (x,y) ≺ pp+25

We can then show by induction that every natural number x precedes the number of the plurality ≤ x, by the plural analogue of what Zalta calls the Lemma on Successors [see Zalta 2017]:

  • 26 Recall that, by definition, ≤-formulæ stand for pp+-formulæ. That pp+, while appearing (...)

Lemma 1 (Lemma on Successors). ∀ x ((x,#[z.z ≤ x]) ≺ pp).26

Since x and z are natural numbers by the definition of ≤, by weak reducibility the formula z ≤ x is co-extensive with a prc-definable concept, which is hp-permissible. We can then prove the Lemma on Successors by induction. Consider the condition (y,#[z.z ≤ y]) ≺ pp contained in the Lemma. This condition can be stated by plc, and defines the plurality containing ordered pairs whose first member is a natural number y that precedes the number of the plurality defined by the condition “z ≤ y”. By plugging that condition in the right-hand side of plc, we get a further plurality, call it qq, containing all individuals y that satisfy the condition (y,#[z.z ≤ y]) ≺ pp (i.e., being in the plurality of predecessors of the number of all individuals z such that z ≤ y). The strategy is to instantiate the plurality xx in the principle of mathematical induction by qq : 0 ≺ qq ∧ Her(qq,ℕ) → ∀x(x ≺ qq).

30Since the consequent is the reconfigured Lemma on Successors, we can prove this Lemma by proving both that 0 ≺ qq and that qq is hereditary on ℕ [see Heck 2012, §  6.6.]:

Theorem 3. Inductive Base: 0 ≺ qq.

  • 27 This can be easily proved by induction on the basis of basic facts about the (...)

Proof. From PA5 and the fact that, for any plurality xx, (x,y) ≺ xx* → ∃z((z,y) ≺ xx),27 which by substitution implies (x,0) ≺ pp* → ∃z((z,0)≺ pp), it follows that (x,0) ⊀ pp*. By definition of pp+, (x,0) ≺ pp* ∨ x = 0, which by (x,0) ⊀ pp* implies that x = 0. Thus, 0 is the only member of the plurality (x,0) ≺ pp+.

  • 28 Lemma Concerning Zero : #F = 0 ↔ ¬∃xFx. See [Zalta 2017].

By these two latter and PA1, it follows that x ≺ ℕ ∧ 0 ≺ ℕ ∧ (x,0) ≺ pp+, which, by definition of ≤, implies ≤ 0. Thus, by weak reducibility and hp, #[x.x ≤ 0] exists. By the Lemma Concerning Zero and ∃x(x ≤ 0),28 it follows that #[x.x ≤ 0] ≠ 0, which by substitution implies that x ≠ 0. By ≤ 0, ≠ 0, weak reducibility, and hp, it follows that #[x.x ≤0 ∧ x ≠ 0] exists. But such a number is 0 itself, since there is no x such that x is less than or equal to 0 and x ≠ 0, by definition of ≤, (x,0) ⊀ pp* from above, and the Lemma Concerning Zero. By ≤ 0, the existence of #[x.≤ 0], and #[x.x ≤ 0 ∧ x ≠ 0] = 0, it follows that x ≤ 0 ∧ x = # [x.x ≤ 0] ∧ #[x.x ≤ 0 ∧ x ≠ 0] = 0, which implies, by definition of pp, that (0,#[x.x ≤ 0]) ≺ pp, i.e., 0 ≺ qq. □

Theorem 4 Inductive Step: qq is hereditary on ℕ.

Proof. In order to prove the inductive step, we need to prove (y,#[z.z ≤ y]) ≺ pp by assuming that (1) (x,y) ≺ pp, and (2) (x,#[z.z ≤ x]) ≺ pp, for any natural numbers x,y. In particular, by the definition of pp, we have to show that, for some concept F, there is a u such that (a) Fu; (b) #[z.z ≤ y] = #F; (c) y = #[z.Fz ∧ z ≠ u]. Let us assume that F is ≤ y, by weak reducibility, and y. So (a) becomes (a') ≤ y, which holds, since by its definition, ≤ is reflexive; (b) becomes (b') #[z.z ≤ y] = #[z.z ≤ y] which is true since it is an instance of the identity principle; (c) becomes (c') y = #[z.z ≤ y ∧ x ≠ y].

  • 29 By hp, it suffices to show [z.z ≤ x] ≈ [z.z ≤ y ∧ z ≠ y], on the basis of the definiti (...)

By assumptions (1) and (2), and by PA3, it follows that y=#[z.zx], which by (c') becomes #[z.z ≤ yz ≠ y] = #[z.z ≤ x]. This latter claim is what we have to prove. This can be done by the Lemma on the Weak Predecessor, i.e., x ≺ ℕ ∧ (y,x)≺ pp →#[z. (z,y) ≺ pp+] = #[z. (z,x) ≺ pp+z ≠ x], from which, since x and y are natural numbers and by the definition of ≤, it follows that y ≺ ℕ ∧ (x,y) ≺ pp →#[z. z ≤ x] = #[z. z ≤ y ∧ z ≠ y], where the consequent is what we had to show in the first place.29

  • 30 Notice that the proof of the Lemma on Successors, in order to introduce the (...)

31Given the inductive proof of the Lemma on Successors and the proof of pa, pa6 follows.30

32pe recovers fa via a predicative notion of equinumerosity, i.e., F ≈ := ∃R(∀y(Fy → ∃!x(Gx ∧ R(x,y)) ∧ ∀y(Gy → ∃!x(Fx ∧ R(y,x))))). In pe, this is not a matter of choice, since otherwise the very definition of the cardinality operator would be blocked on the basis of the ban on impredicative variables in pe’s blv [see Ferreira 2018, § 4]. Mathematically, this is not a severe issue, since impredicative bijections will be finite, as soon as they are restricted to finite concepts F and G, and thus co-extensive with predicative ones by finite reducibility. Still, it shows that in pe the import of finite reducibility is more pervasive than in vimp. All in all, what vimp really needs is only a way to prove the Successor Axiom, and that is achieved by a weaker result than finite reducibility, namely by weak reducibility; whereas, without finite reducibility, pe would not even start to recover fa for the just aforementioned reason. Unlike vimp where the definition of the cardinality operator takes advantage of the (plural) impredicative definition of equinumerosity, pe requires finite reducibility to correct a limitation the axioms suffer from because of the restrictions imposed on them. But, as shown in this article, some of those restrictions are unnecessary, so there is no apparent reason for banning impredicative bijections from the definition of the cardinality operator.

  • 31 See for instance [Boolos 1986-1987], [Cook 2003], and [Jané & Uzquiano 200 (...)
  • 32 Though, it is likely that pe and vimp have the same mathematical strength. This claim (...)

33Furthermore, pe and vimp are on a par as long as finite cardinals are concerned. As long as one agrees with [Ferreira 2018] that so far no satisfactory set theory has been based on consistent fragments of blv and likely there will never be one, the fact that by blv we cannot move up from the finite into the transfinite should not be troublesome at all. But some may be disappointed that we should stop at pa2, especially since some fragments of ZFC have been interpreted in consistent fragments of blv.31 At the very least, it would be nice to leave the possibility open. To this extent, upon further investigation, vimp might prove useful for the purpose of going beyond pa2. After all, in vimp, unlike pe, the extension containing all natural numbers {x.x ≺ ℕ} is delivered by v*.32 It might be worrisome that, once the definition of ℕ is unravelled, its extension-term seems to contain a free plural variable, namely pp+. Still, this is not problematic: in fact, every single instance of pp+ can be substituted by its defining formula, which contains no free plural variables at all, as it is clear once the definition of pp+ is unfolded:

x≺ ℕ ≔ (0,x) ≺ pp+≔ 0 = x ∨ (0,x) ≺ pp* ≔

  • 33 Where Her(xx,∃Fu(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u])) Her(xx,∃Fu(Fux=#F∧0=#[z.Fzzu])) means ∃F(...)

0 = x ∨ ∀xx(∀y(∃Fu(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u]) → y ≺ xx) ∧ Her(xx,∃Fu(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u])) → x ≺ xx).33

  • 34 For instance, we might consider adding further consistent formulations of blv to vimp, (...)

34The more liberal restrictions imposed on vimp’s axioms than the restrictions imposed on pe’s axioms might be used as a basis to extend vimp to a theory of infinite extensions aimed at recovering larger fragments of set theory.34

4 Closing remarks

35In [Boccuni 2010], the system pg is presented, which recovers pa2. Due to the predicative restriction both on the second-order comprehension axiom prc and on axiom v, pg cannot interpret Frege Arithmetic fa. Consequently, pg cannot prove Frege’s Theorem, and thus pa2, though interpretable in pg, cannot be recovered in a way that resembles Frege’s. In this paper, it is shown that the predicative restriction on axiom v can be lifted. By consistently extending axiom v to axiom v*, the resulting system vimp recovers fa and pa2 in a way that parallels Frege’s. This advantage is due to the fact that vimp allows for any formula not containing free plural variables to appear within the extension-terms governed by v*, thus delivering, first and foremost, a Fregean notion of number by the definition of #, which is necessary to deliver fa and Frege’s Theorem.

36At the same time, vimp is also a consistent extension of the system pe in [Ferreira 2018]. Though likely the two systems are mathematically equivalent, it was argued that vimp has some nice advantages over pe. First of all, vimp requires a somewhat weaker logico-mathematical machinery to carry out its main goal: vimp requires [Ferreira 2018]’s weak reducibility to prove the Successor Axiom, but on the basis of more liberal restrictions than pe it can interpret fa without further ado. Meanwhile, pe necessarily relies upon not only weak reducibility to prove the Successor Axiom, but also on finite reducibility, a stronger result than the former, in order to interpret fa to begin with. By its consistency proof, vimp shows that the restrictions that prevent pe from interpreting fa without appealing to finite reducibility can be lifted. Secondly, on the basis of those same restrictions, unlike vimp, pe cannot collect the totality of finite cardinals in the extension of the concept natural number, because of the irreducible impredicativity of this latter. This is not to say that vimp is stronger than pe, but at least vimp might provide a starting point to recover larger fragments of set theory.

Acknowledgements

37I would like to sincerely thank an anonymous reviewer for their valuable comments.

Haut de page

Bibliographie

Boccuni, Francesca [2010], Plural Grundgesetze, Studia Logica, 96(2), 315–330, doi: 10.1007/s11225-010-9281-3.

Boccuni, Francesca [2011], On the consistency of a plural theory of Frege’s Grundgesetze, Studia Logica, 97(3), 329–345, doi: 10.1007/s11225-011-9311-9.

Boccuni, Francesca & Panza, Marco [2021], Frege’s theory of real numbers: A consistent rendering, The Review of Symbolic Logic, 1–44, doi: 10.1017/S175502032000026X.

Boolos, George [1985], Nominalist Platonism, The Philosophical Review, 94(3), 327–344, doi10.2307/2185003.

Boolos, George [1986-1987], Saving Frege from contradiction, Proceedings of the Aristotelian Society, 87(1), 137–151.

Burgess, John P. [2005], Fixing Frege, Princeton: Princeton University Press.

Cook, Roy T. [2003], Iteration one more time, Notre Dame Journal of Formal Logic, 44(2), 63–92.

Cruz-Filipe, Luís & Ferreira, Fernando [2015], The finitistic consistency of Heck’s predicative Fregean system, Notre Dame Journal of Formal Logic, 56(1), 61–79.

Ferreira, Fernando [2018], Zigzag and Fregean arithmetic, dans The Philosophers and Mathematics: Festschrift for Roshdi Rashed, édité par H. Tahiri, Cham: Springer International Publishing, t. 43, 81–100, doi: 10.1007/978-3-319-93733-5_4.

Ferreira, Fernando & Wehmeier, Kai F. [2002], On the consistency of the Δ¹₁-CA fragment of Frege’s Grundgesetze, Journal of Philosophical Logic, 31(4), 301–311, doi: 10.1023/A:1019919403797.

Ganea, Mihai [2007], Burgess’ PV is Robinson’s Q, Journal of Symbolic Logic, 72(2), 619–624, doi: 10.2178/jsl/1185803626.

Hale, Bob [2005], Real numbers and set theory – Extending the neo-Fregean programme beyond arithmetic, Synthese, 147(1), 21–41, doi: 10.1007/s11229-004-6205-7.

Heck, Richard K. [1996], The consistency of predicative fragments of Frege’s Grundgesetze der Arithmetik, History and Philosophy of Logic, 17(1–2), 209–220, doi: 10.1080/01445349608837265, originally published under the name “R. G. Heck, Jr.”.

Heck, Richard K. [2012], Reading Frege’s Grundgesetze, Oxford: Oxford University Press, originally published under the name “R.G. Heck, Jr.”.

Hewitt, Simon T. [2018], Tuples all the way down?, Thought: A Journal of Philosophy, 7, 161–169.

Jané, Ignacio & Uzquiano, Gabriel [2004], Well- and non-well-founded Fregean extensions, Journal of Philosophical Logic, 33(5), 437–465, doi: 10.1023/B:LOGI.0000046129.22633.96.

Linnebo, Øystein [2004], Predicative fragments of Frege arithmetic, The Bulletin of Symbolic Logic, 10(2), 153–174, doi: 10.2307/3176758.

Panza, Marco [2016], Abstraction and epistemic economy, dans Early Analytic Philosophy – New Perspectives on the Tradition, édité par S. Costreie, Cham: Springer International Publishing, 387–428, doi: 10.1007/978-3-319-24214-9_17.

Paseau, Alexander C. [2015], Did Frege commit a cardinal sin?, Analysis, 75, 379–3.

Tennant, Neil [2017], Logicism and neologicism, dans The Stanford Encyclopedia of Philosophy, édité par E. N. Zalta, Metaphysics Research Lab, Stanford University, Winter 2017 éd., https://plato.stanford.edu/archives/win2017/entries/logicism/.

Wehmeier, Kai F. [1999], Consistent fragments of Grundgesetze and the existence of non-logical objects, Synthese, 121(3), 309–328, doi: 10.1023/A:1005203526185.

Zalta, Edward N. [2017], Frege’s Theorem and Foundations for Arithmetic, dans The Stanford Encyclopedia of Philosophy, édité par Edward N. Zalta, Metaphysics Research Lab, Stanford University, Summer 2017 éd.

Haut de page

Notes

1 See, for instance, the famous debate between Boolos and Dummett on the cause of the inconsistency in Frege’s Grundgesetze. Dummett ascribes the inconsistency to the underlying second-order logic, in particular to the indefinite extensibility of the very notion of concept. On the other hand, Boolos ascribes the contradiction to the violation of Cantor’s theorem embodied in the one-to-one correspondence Frege’s blv poses between concepts and objects. But see [Paseau 2015] in this respect.

2 See [Burgess 2005, § 2.6], [Ferreira & Wehmeier 2002], [Heck 1996], and [Wehmeier 1999]. Famously, Robinson’s Q lacks a (first-order) induction principle, i.e., φ0∧∀x(φxφsx)→∀xφx. In the above consistent subsystems of Frege’s Grundgesetze, the concept being a natural number cannot be defined in such a way that any interesting class of inductions can be proved, because of its irreducible impredicativity—e.g., this is pointed out by [Heck 1996] with regards to their predicative subsystem of Grundgesetze. Also, it has to be mentioned that the extension operator governed by (fragments of) blv can either be functional and take second-order variables as arguments, or variable-binding and take first-order variables as arguments. For instance, [Ganea 2007] proves the equi-interpretability of the predicative fragment of blv with a functional operator with Robinson’s Q. See also [Cruz-Filipe & Ferreira 2015] for a thorough discussion of these issues.

3 In [Boccuni 2010] a different notation is used for plural formulæ, i.e., xηX, meaning “x is one of the xs”. In the present article, I will rephrase [Boccuni 2010]’s plural notation in the standard notation, i.e.,  xx. Other things being equal, these two notations imply neither a deductive nor a semantic difference.

4 See [Boccuni 2010] and [Boolos 1985] for considerations supporting the claim that prc is indeed predicative, even though it allows for bound plural variables on its right-hand side. Also, the aim of this article is merely technical, so I will not delve into philosophical issues. Still, for philosophical considerations on the difference between plural and second-order quantification, see [Boccuni 2010].

5 In pg, [Ferreira 2018], and in the system presented in this article, concepts are the values of second-order variables.

6 In [Ferreira 2018], the system pe is presented, which consists of two rounds of second-order variables , 𝒢, , and F,G,H,… respectively governed by an impredicative comprehension axiom ∃x( x ↔ φx), where φ is unrestricted; a predicative comprehension axiom ∃Fx(F x ↔ φx) where φ contains neither bound predicative variables nor impredicative variables at all; and a formulation of blv, i.e., .Ax .Bx ↔ ∀x(Ax ↔ Bx) with a variable-binding operator , where A and B contain no impredicative variables at all, but can contain predicative variables both free and bound. pe is consistent and strong enough to recover fa. More remarks on pe will be provided later on.

7 The same considerations mentioned in fn. 4 above apply also to prc in vimp.

8 Modulo a translation of pe’s second-orderly impredicative fragment into vimp’s plural fragment. Notice that both in vimp and in [Boccuni 2010], as also in [Ferreira 2018] and [Heck 1996], the extension operator is variable-binding. Both in vimp and in [Ferreira 2018], this is crucial, since complex formulæ are needed in the scope of the extension operator for recovering fa.

9 Also in [Ferreira 2018] there is no one-to-one correspondence between (predicative, let alone impredicative) concepts and extensions, and fa is recovered.

10 See [Tennant 2017] on these and other issues connected with logicism.

11 Recall that in vimp, just like in pg, bound second-order variables are not allowed on the right-hand side of prc, so that also formulæ containing extension-terms with bound second-order variables are not allowed on the right-hand side of prc in either theories. Also, it goes without saying that extension-terms can contain free and bound first-order variables.

12 As mentioned, extension-terms can contain free first-order variables. The values of these are provided by [Boccuni 2011] in line with [Heck 1996], namely by substituting with numerals free first-order variables other than the designated first-order variable.

13 Instances containing free second-order variables and bound plural variables are proved to hold by [Boccuni 2011]’s construction.

14 Where x is their sole free variable.

15 The proof goes analogously if {Bx} precedes {Ax} in the ω × ω-sequence.

16 Since pe is a subsystem of vimp, the consistency of vimp implies that in pe the ban on bound impredicative second-order variables in pe’s predicative second-order comprehension axiom and pe’s blv can be consistently lifted. Analogously as for v in pg.

17 The Weak Reducibility Theorem in [Ferreira 2018] states that, if x is a natural number, there is a (predicative) concept that is co-extensive with the formula y ≤ x, where ≤ is defined impredicatively. This theorem is implied by a Finite Reducibility Theorem in pe, which states that every finite impredicative concept (relation) is co-extensive with a (finite) predicative concept (relation). Since pe is a subtheory of vimp, these theorems follow in vimp as well, though in a plural formulation.

18 Given its formulation, in vimp hp is restricted to prc-definable concepts. We’ll see this poses some issues as for the proof of Frege’s Theorem, which, nevertheless, can be easily overcome. See § 3.2.

19 Boolos’ plural logic is monadic, so as it stands it cannot be used to define the equinumerosity relation. This issue can be easily circumvented by defining the notions of singleton, unordered pair, and (Wiener-Kuratowski) ordered pair in vimp— {x} ≔ {y : x = y}; {x,y} ≔ {z : z = x ∨ {z = y}}, and (x,y) ≔ {{x},{x,y}}, respectively. On the basis of the definition of ordered pairs, the set of the well-formed plural formulæ of the language of vimp contains formulæ of the form (x,y)  xx, so that also the plural fragment of the language of vimp is polyadic.

20 For the sake of clarity, I will use the following notational convention : if a complex prc-permissible formula, e.g., x ≠ x ∧ ∃xx(x ≺ xx), is co-extensive with a concept that has a number, I will construe the corresponding number-term as “#[x.x ≠ x ∧ ∃xx(x ≺ xx)]”, namely the number of all individuals x such that x ≠x ∧ ∃xx(x ≺ xx).

21 The Successor Axiom.

22 The Principle of Mathematical Induction.

23 This can be accomplished by a definition of Fregean finitude, which mirrors Frege’s definition as in [Heck 2012, § 8.1], according to which a plurality xx is finite if, and only if, “x belongs to the xx-series running from a to b”, i.e., xx is functional, and is such that (b,b) ⊀ xx*, (a,x) ≺ xx+, and, (x,b) ≺ xx+.

24 In order to prove the Successor Axiom, [Ferreira 2018] proves a stronger theorem, i.e., ∀x(ℕx → ∃F(∀u(Fuux)∧ S(x, #F))), where S is the Successor relation, by taking advantage of weak reducibility.

25 The right-hand side formula is a valid instance of plc.

26 Recall that, by definition, ≤-formulæ stand for pp+-formulæ. That pp+, while appearing to be a free plural variable, is contained in #-terms is not problematic: in fact, every single instance of it can be substituted by its defining formula, which contains no free plural variables at all. See also below.

27 This can be easily proved by induction on the basis of basic facts about the ancestral, i.e., for any xx, yy (a,b) ≺ xx* ∧ ∀x,y(x ≺ yy ∧ (x,y) ≺ xx → y ≺ yy) ∧ ∀x((a,x) ≺ xx → x ≺ yy) →  yy. See [Heck 2012, § 6.6.2, fn. 29].

28 Lemma Concerning Zero : #F = 0 ↔ ¬∃xFx. See [Zalta 2017].

29 By hp, it suffices to show [z.z ≤ x] ≈ [z.z ≤ y ∧ z ≠ y], on the basis of the definition of ≤ and weak reducibility. Since it’s a fact about equinumerosity that co-extensive conditions are equinumerous, we have that ∀z(z ≤ x) ≡ ∀z(z ≤ yz ≠ y), which, by the definition of ≤, is provable from facts about the weak ancestral. See [Zalta 2017]. Notice, though, that the proof of the Lemma on the Weak Predecessor in [Zalta 2017] follows from a further lemma, i.e., the lemma that no number strongly precedes (i.e., pp*) itself : ∀x(x ≺ ℕ → (x,xpp*).

30 Notice that the proof of the Lemma on Successors, in order to introduce the plurality qq, requires an instance of plc containing bound second-order variables in the condition (y,#[z.z ≤ y]) ≺ pp once #, ≤ and pp are unfolded. As pointed out by [Heck 1996] and [Linnebo 2004], in order to follow Frege’s proof of the Successor Axiom via his definitions, we need to apply a fragment of impredicative reasoning. This, along with the requirement that pp and ℕ should be plugged in the principle of Mathematical Induction in order to recover full pa2, are the passages of the proof of Frege’s Theorem where impredicative reasoning is necessary, whether plural or second-order.

31 See for instance [Boolos 1986-1987], [Cook 2003], and [Jané & Uzquiano 2004].

32 Though, it is likely that pe and vimp have the same mathematical strength. This claim would require a proof that goes beyond the aim of this article, so I shall just state it as a (reasonable) conjecture.

33 Where Her(xx,∃Fu(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u])) Her(xx,∃Fu(Fux=#F∧0=#[z.Fzzu])) means ∃Fu(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u]) → (0  xxx  xx).

34 For instance, we might consider adding further consistent formulations of blv to vimp, in order to recover real analysis starting from the extension of all natural numbers—see, e.g., [Hale 2005] or [Panza 2016]. But see also [Boccuni & Panza 2021] for a critical view of this strategy, and an alternative.

Haut de page

Pour citer cet article

Référence papier

Francesca Boccuni, « Plural Frege Arithmetic »Philosophia Scientiæ, 26-1 | 2022, 189-206.

Référence électronique

Francesca Boccuni, « Plural Frege Arithmetic »Philosophia Scientiæ [En ligne], 26-1 | 2022, mis en ligne le 25 février 2022, consulté le 18 juin 2026. URL : http://journals.openedition.org/philosophiascientiae/3394 ; DOI : https://doi.org/10.4000/philosophiascientiae.3394

Haut de page

Auteur

Francesca Boccuni

Vita-Salute San Raffaele University (Italy)

Articles du même auteur

Haut de page

Droits d’auteur

CC-BY-NC-ND-4.0

Le texte seul est utilisable sous licence CC BY-NC-ND 4.0. Les autres éléments (illustrations, fichiers annexes importés) sont susceptibles d’être soumis à des autorisations d’usage spécifiques.

Haut de page
Rechercher dans OpenEdition Search

Vous allez être redirigé vers OpenEdition Search