- 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
-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 : ∃xx∀x(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 : ∃F∀x(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 = #G ↔ F ≈ 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 pa2 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
- 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:
- to recap the consistency proof of pg—i.e., of the aforementioned fragment of vimp;
- to prove that all extension-terms containing bound second-order variables have denotations;
- to prove that all instances of v* containing extension-terms with bound second-order variables hold in the model;
- to prove that all instances of plc containing extension-terms containing bound second-order variables hold in the model.
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:
- 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
- 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).
- Thirdly, [Boccuni 2011, § 4.2.1] provides denotations for extension-terms containing free second-order variables in line with [Heck 1996, § 3.2].
- 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.
- Then, [Boccuni 2011, § 4.4] shows that all instances of prc hold in this model.
- 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.
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 {x : Bx} and {x : 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 {x : 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 k < n, K(m,k) has already been assigned as denotation to some extension-term, but K(m,n) has not.
14Check now that, if {x : Bx} and {x : Cx} precede or are identical with t, then Bx and Cx are equivalent under I with respect to x if, and only if, {x : Bx} and {x : Cx} have been assigned the same denotation. The case in which {x : Bx} and {x : Cx} precede t in the sequence is covered by the previous assumption. Now, let t = {x : Bx}. Since t is {x : Ax} by previous assumption, the denotations of the terms {x : Ax} and {x : Bx} are identical. Then, Ax and Cx are equivalent if, and only if, {x : Ax} and {x : Cx} have been assigned the same denotation by construction via the function K(m,n).
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 {x : Bx} precedes {x : Ax} in the ω × ω-sequence.
Let {x : Ax} and {x : Bx} be extension-terms, such that Ax is equivalent to φx and Bx is equivalent to ψx.14 Let us assign the denotations of {x : Ax} and {x : Bx} respectively to {x : φx} and {x : ψx} as their denotations. From the previous section, in the ω×ω-sequence either {x : Ax} is prior to {x : Bx}, or conversely. Suppose {x : Ax} precedes {x : 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
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.
- 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., ∃F∀x(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 ≔ ∃F∃u(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+
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) ≺ pp → y ≺ ℕ).
(PA3) ∀ x,y,z(x ≺ ℕ ∧ y ≺ ℕ ∧ z ≺ ℕ ∧(x,y) ≺ pp ∧ (x,z) ≺ pp → y = z)
(PA4) ∀ x,y,z(x ≺ ℕ ∧ y ≺ ℕ ∧ z ≺ ℕ ∧(x,z) ≺ pp ∧ (y,z) ≺ pp → x = y)
(PA5) ¬ ∃x (x ≺ ℕ ∧(x,0) ≺ pp)
(PA6) ∀x(x≺ ℕ → ∃ y(y ≺ ℕ ∧ (x,y) ≺ pp)).21
- 22 The Principle of Mathematical Induction.
(PA7) ∀xx (0 ≺ xx ∧ Her(xx,pp) → ∀ x(x ≺ ℕ → x ≺ xx)).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 (≤): x ≤ y ≔ x ≺ ℕ ∧ y ≺ ℕ ∧ (x,y) ≺ pp+25
We can then show by induction that every natural number x precedes the number of the plurality z ≤ 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 x ≤ 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 x ≤ 0, x ≠ 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 x ≤ 0, the existence of #[x.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 z ≤ y, by weak reducibility, and u = y. So (a) becomes (a') y ≤ 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.z≤x], which by (c') becomes #[z.z ≤ y∧z ≠ 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 ≈ G := ∃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,∃F∃u(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u])) Her(xx,∃F∃u(Fu∧x=#F∧0=#[z.Fz∧z≠u])) means ∃F(...)
0 = x ∨ ∀xx(∀y(∃F∃u(Fu ∧ x = #F ∧ 0 = #[z.Fz ∧ z ≠ u]) → y ≺ xx) ∧ Her(xx,∃F∃u(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
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.
37I would like to sincerely thank an anonymous reviewer for their valuable comments.