Dedekind's Proof
by Andrew Boucher
v2.0 Last updated: 10 Dec 2001 Created: 1 Sept 2000
Please send your comments to abo

In "The Nature and Meaning of Numbers," Dedekind produces an original, quite remarkable proof for the holy grail in the foundations of elementary arithmetic, that there are an infinite number of things. It goes like this. [p, 64 in the Dover edition.] Consider the set S of things which can be objects of my thought. Define the function phi(s), which maps an element s of S to the thought that s can be an object of my thought. Then phi is evidently one-to-one, and the image of phi is contained in S. Indeed, it is properly contained in S, because I myself can be an object of my thoughts and so belong to S, but I myself am not a mere thought. Thus S is infinite.

Now Dedekind's proof is not well respected by philosophers of mathematics (e.g. see Boolos' "The Standard of Equality of Numbers"). The appeals to me myself and to thoughts take the proof out of what Anglo-Saxons anyway would consider the proper domain of logic. There is also the assumption that, if s is a thought, then there always exists the thought that s can be an object of my thoughts. This may be defensible, but it obviously depends on one's perspectives on thoughts, which again do not seem strictly logical.

These criticisms aside, Dedekind's proof in its essence is nonetheless not really so bad as all that. On the contrary, the technique which it employs, building a hierarchical chain of pseudo-logical things, is of fundamental importance. It uses thoughts--constructing a thought of a thought of a thought...--, but one might equally have used sets--a set of a set of a set...--or predicates--a predicate of a predicate of a predicate...

The major competition to Dedekind comes from Frege. This technique, which can be called the "bootstrap" approach, proceeds by showing the natural numbers themselves are infinite, since the existence of 0 implies there is 1 thing, the existence of 0 and 1 that there are 2, the existence of 0, 1, and 2 that there are 3 things, and so forth, and in general the existence of the natural number n implies that there are n+1 things (namely the natural numbers 0 through n).

Boolos (again in "The Standard of Equality of Numbers") asserts that "infinity is cheap." By this he means that theories with weak assumptions must have infinite models. So in his eyes the interesting question is not whether a theory must have infinite models, but whether a logically true theory is such. (He answers no.)

I would like to suggest that there is another interesting question: whether one can prove the infinity of objects in the theory itself. Boolos did not ask this question, because he was a logician, and modern logicians don't as a rule think much of interpreted systems. In their eyes syntax and semantics are to be kept separate, theories are syntax, and so forth. Nonetheless, despite the modern bias against such an approach, it has sense. The idea is to fix one's eyes on proving a particular proposition, such as that there are an infinite number of things, and ask what axioms one must make in order to prove it. In an interpreted system, the quality of the axioms can be judged: would one really want to assume such-and-such about the concepts in question? Is it--because it is in the context of the foundations of elementary arithmetic--fundamental, or can we do better?

It is a different question from Boolos', but probably the one Frege wanted to resolve, and one which in any case Boolos in his analysis of Frege essentially answers.

Now there are two different ways of stating that there are an infinite number of things--if you will, the potential and the actual version. Let

Nx mean "x is a natural (finite) number",
Mn,P mean "P is n in number", and
Sn,m mean "m succeeds n".
Potential infinity means that the number of things are unbounded, i.e. for any natural number n, there are more than n things, or formally
(n) (Nn => [X][a] (Mn,X & ~Xa)) (POTINF)
Here, for those who haven't seen this notation yet, [..] is used to mean "there exists". (This is analogous to (..) being used to represent the universal quantifier, which is standard notation.)

Actual infinity asserts that there is a set or predicate which is infinite. Formally,

[X](n) ~(Nn & Mn,X) (ACTINF)

Boolos worked in what is called Frege Arithmetic (FA), which is second-order logic (two types of entities, lower- and upper-case, which must be kept separate) plus the axiom known as Hume's Principle (HP), which says that P and Q have the same number precisely when there is a 1-1 function from P onto Q. The name "Frege Arithmetic" obviously is suggestive, and Frege can be thought of having used FA to derive elementary arithmetic, although of course he did not assume HP, and indeed proved it from his now infamous, because inconsistent, Axiom V. In the perspective of an interpreted system, definitions which are not abbreviations become axioms, so Boolos following Frege made these assumptions (here P == Q abbreviates there is a 1-1 function from P onto Q):

B1 (x)( {x : phi}x <=> phi), where phi is any formula
B2 (x)(y) ( {x,y : phi}x,y <=> phi ), where phi is any formula
B3 (P)[n] Mn,P
B4 (P)(Q)(n) ( Mn,P => (P == Q <=> Mn,Q) )
B5 (P)(n)(m) (Mn,P & Mm,P => n = m)
B6 M0,{x : ~x = x}
B7 (m)(n) (Sm,n <=> [P][a] (~Pa & Mm,P & Mn,{x : Px V x = a}))
B8 (n) (Nn <=> n = 0 V (P) [ (a)(b) ( [(a = 0 V Pa) & Sa,b] => Pb) => Pn ]

Remark that Pa says that "a satisfies P" or "a belongs to P," according to one's interpretation of big-letters as predicates or classes (or properties or sets...). So {x : x = x}a for instance says that a satisfies {x : x = x}, i.e. a = a. Also, {x : x = x}x if and only if x = x, which is an instance of B1. (I would like to think this is a clever use of scope, but perhaps people just find it confusing.)

Remark as well that {x : phi} is considered a "big" letter, and may only be substituted for a universal quantifier of a big letter. E.g. from B3 we may conclude that [n] Mn,{x : x = x}.

Proceed as follows to prove POTINF and ACTINF. Proofs are not given up to P12, since they can be found at the end of "The Standard of Equality of Numbers":

P1 (P) (M0,P <=> (x) ~Px)

P2 (m)(n)(m')(n') (Sm,n & Sm',n' => (m = m' <=> n = n'))

P3 (n) ~Sn,0

Abbreviate (P) [ (a)(b) ( [(a = n V Pa) & Sa,b] => Pb) => Pm ] with (S*)n,m. Note that:

P3a (n) (Nn <=> n = 0 V (S*)0,n)

P4 (n)(m) (Sn,m => (S*)n,m)

P5 (n)(m)(p) ((S*)n,m & (S*)m,p => (S*)n,p)

P6 (n)(x) ((S*)x,n => [m]Sm,n & (m) (Sm,n => ((S*)x,m V x = m)))

P7 (n) ((S*)0,n => ~(S*)n,n)

Abbreviate n = m V (S*)m,n by m <= n. Note that:

P7a (n) (Nn <=> 0 <= n).

P8 (n)(m) (Sn,m & (S*)0,m => (x) (x <= n <=> x <= m & ~x = m).

P9 (n)(m)(p)(q) (Sn,m & (S*)0,m & Mp,{x : x <= n} & Mq,{x : x <= m} => Sp,q)

P10 (n)(m)(p)(q) (Sn,m & Nn & Mp,{x : x <= n} & Mq,{x : x <= m} & Sn,p => Nm & Sm,q)

P11 [p] Mp,{x : x <= 0} & (p)(Mp,{x : x <= 0} => S0,p)

P12 (n)(Nn => [p] Mp,{x : x <= n}) & (n)(p)(Nn & Mp,{x : x <= n} => Sn,p)

P13 ~(S*)0,0.
Pf: This contradicts P7.

P14 (n) (Nn => ~(S*)n,n).
Pf: By P3a, Nn => n = 0 V (S*)0,n. So use P7 and P13.

P15 (n)(m) (Nn & Sn,m => Nm)
Pf: Suppose Nn & Sn,m. By P4, (S*)n,m. By P3a, n = 0 V (S*)0,n. If the former, then (S*)0,m. If the latter, then by P5, (S*)0,m. So in both cases, using again P3a, Nm.

P16 (n)(Nn & ~n = 0 => [m] (Nm & Sm,n))
Pf: By B8, (P) [ (a)(b) ( [(a = 0 V Pa) & Sa,b] => Pb) => Pn ]. Let P = {x : [m] (Nm & Sm,x)}. Suppose [(a = 0 V Pa) & Sa,b]. By P3a, a = 0 implies Na. On the other hand, so does Pa, using P15. Hence Na & Sa,b, so evidently [m] (Nm & Sm,b). Thus Pb. Hence Pn.

P17 (n)(m) (Nm & Sm,n => ~ n <= m)
Pf: Suppose Nm & Sm,n & n <= m. The second conjunct and P4 implies (S*)m,n. The third implies m = n V (S*)n,m. By P14, ~m = n. So (S*)n,m. By P5, (S*)m,m. But this contradicts P14.

P18 POTINF
Pf: Let Nn. M0,{x : ~x = x} & ~{x : ~x = x}0. So true for n = 0. Assume then ~n = 0. By P16, Nm & Sm,n for some m. By P12, Sm,q, where Mq,{x : x <= m}. By P2, n = q, i.e. Mn,{x : x <= m}. By P17, ~{x : x <= m}n.

P19 ACTINF
Pf: Suppose Nn & Mn,N. But S is a 1-1 function from N onto {x : Nx & ~x = 0}. (It is a 1-1 function by P2, it is onto by P16.) That is, N == {x : Nx & ~x = 0}. By B4, Mn,{x : Nx & ~x = 0}. By B7, Sn,n. By P4, (S*)n,n. But this contradicts P14.

A version of Dedekind's proof can't go through in Frege Arithmetic, because numbers are the only first-order entities guaranteed to exist. (Evidently this supposes numbers don't count as "pseudo-logical".) The second-order entities, which are pseudo-logical--properties, classes, or whatever you choose to call them--cannot themselves be counted, so of course cannot be proven infinite in the theory. (Remark that looked at from the exterior, of course, they can be counted, and of course must be infinite since numbers are. After all, {x : x = a} must be different from {x : x = b} if ~a = b, because of B1.)

So we cannot stay in pure second-order logic, in order to express Dedekind's proof. Consider instead the following logical system. Like second-order logic, use big- and small-letters. Big-letters, however, may be substituted for small-letters. It is possible as well to let small-letters be substituted for big-letters, in which case there is no difference between the two types, and the system becomes a standard first-order theory. Nonetheless, this is stronger than what is needed, and the solution to the paradoxes advocated in "A Comprehensive Solution to the Paradoxes" supports a distinction between big- and small-letters.

Just to give a small feel for the system, here are some simple examples. From (x)(x = x), one may infer both 0 = 0, P = P, and {x : ~x = 0} = {x : ~x = 0}. On the other hand, one has a choice about allowing the substitution of 0 in for P in "(P) (M0,P <=> (x) ~Px)". If one allows it, then the system makes no distinction between big- and little-letters, as these become interchangeable. The system is therefore standard first-order. If one doesn't, then little-letters subsume big-.

Remark that {x : x = P} is now a legitimate term, and indeed by comprehension {x : x = P}P. (Again, big-letters may be substituted for little.) It is this facility which will allow the system to construct a hierarchy of predicates (or sets or classes, depending on your interpretation).

Full-scale comprehension isn't of course consistent in such a system, but only very simple comprehension is justified and anyway needed, and one can and should stop with ACA, that is arithmetic comprehension (i.e. no bound variables allowed in the predicate place).

F1 (x)({x : phi}x <=> phi) where phi does not contain any bound variables or free x in the predicate position
F2 (x)(y)({x,y : phi}x,y <=> phi) where phi does not contain any bound variables or free x or y in the predicate position
F3 (n)(m)(P) ( Nn & Mn,P & Mm,P => n = m)
F4 (P) (M0,P <=> (x) ~Px)
F5 (n)(m)(P)(Q)(a) ( Nn & Sn,m & ~Pa & (x)(Qx <=> Px V x = a) => (Mn,P <=> Mm,Q) )
F6(rule of induction: phi any formula, (x\y) means x substituted for free instances of y, supposing that x does not become bound in any of these occurences)

phi(0\n)
(n)(m) ( Nn & Sn,m & phi => phi (m\n) )
-------------------------------------------------
(n) ( Nn => phi )

Now probably the first thing to note in this system is that there may not even be any natural numbers! There are no axioms, for instance, like
N0,
(n)(P)(a) ( ~Pa & Mn,P => [m]Mm,{x : Px V x = a} ),
or B3, which state that certain natural numbers exist. Nonetheless, both POTINF and ACTINF are provable. Indeed, both become more "easily" true if there is a paucity of natural numbers; in the extreme, if there are no natural numbers whatsoever, both POTINF and ACTINF are trivially true.

Secondly note that it is a metatheorem that induction may be replaced by (F6*):

phi(0\n)
(n)(m) ( Nn & Nm & Sn,m & ~ m = 0 & phi => phi (m\n) )
-------------------------------------------------
(n) ( Nn => phi )

Q1 (P)(Q) (M0,P & (P == Q <=> M0,Q))
Pf: Assume M0,P. By F4, (x) ~ Px. Suppose P == Q, i.e. there is a 1-1 relationship from P onto Q. Then (x) ~Qx. By F4, M0,Q. On the other hand, suppose M0,Q. Then (x) ~Qx by F4. So the empty relationship proves that P == Q.

Q2 (P)(n) (Nn & Mn,P & ~n = 0 => [a] Pa)
Pf: Assume Nn & Mn,P and ~n=0, and suppose (a)~Pa. By F4, M0,P. By F3, n = 0, a contradiction.

Q3 (P)(Q)(n) (Nn & Mn,P => (P == Q <=> Mn,Q))
Pf: By induction. Q1 proves the case n = 0. Suppose Nn & Nm & Sn,m & ~ m = 0 & (P)(Q) (Nn & Mn,P => (P == Q <=> Mn,Q)). Suppose further that Mm,P. By Q2, Pa for some a. Consider P' = P \ {a}. Obviously, ~P'a and (x)(Px <=> P'x V x = a). By F5, Mn,P'.
Now suppose P == Q. Let R be a 1-1 relationship from P onto Q. Then Rab for a unique b s.t. Qb. Consider Q' = Q \ {b}. R \ {(a,b)} is 1-1 from P' onto Q', so P' == Q'. By the induction hypothesis, Mn,Q'. ~Q'b and (x)(Qx <=> Qx' V x = b), so by F5, Mm,Q.
Suppose Mm,Q. Since ~ m = 0, Qb for some b by Q2. Consider again Q' = Q \ {b}. Of course, ~Q'b and (x)(Qx <=> Q'x V x = b). So by F5, Mn,Q'. By induction, P' == Q'. Let R' be the 1-1 relationship from P' onto Q'. Then R' + {(a,b)} is 1-1 from P onto Q. That is, P == Q.

Abbreviate (x)(Px <=> Qx) by P eqv Q. Remark that

Q3' (n)(P)(Q) ( Nn & Mn,P & P eqv Q => Mn,Q )

follows from Q3, since P eqv Q implies P == Q.

Abbreviate (x)(Px => Qx) by P cnt Q (P "contained in" Q).

Abbreviate P cnt Q & ~ P eqv Q by P pcn Q (P "properly contained in Q").

Abbreviate (x) (Px => x pcn P) by H P.

Q4 (P) (H P => ~PP)
Pf: Suppose H P. Then PP => P pcn P. Since ~P pcn P, we conclude that ~PP.

Q5 (P) (M0,P => H P)
Pf: Suppose M0,P. By F4, (x) ~Px. So (x) (Px => x pcn P) vacuously.

Abbreviate {x : Px V x = P} by (P+).

Q6 (P)(x)((P+)x <=> Px V x = P)
Pf: By F1. Remark that phi is "Px V x = P", so that the only variable in a predicate position, namely "P", is free.

Q7 (P) (H P => ~ P eqv (P+))
Pf: Suppose HP and P eqv (P+). (P+)P by Q6, so PP by equivalence. This contradicts Q4.

Q8 (P) (H P => P pcn (P+))
Pf: Suppose H P. By Q7, ~ P eqv (P+). But obviously P cnt (P+). So P pcn (P+).

Q9 (P) (H P => H (P+))
Pf: Assume H P. Suppose (P+)x. Then Px V x = P. In the first case, x pcn P since H P. Since P cnt (P+), x pcn (P+). In the second case, use Q8.

Q10 (n) (Nn => [P] (H P & Mn,P))
Pf: By induction. By Q5, H {x : ~x = x}. By F4, M0,{x : ~x = x}. So true for n = 0. Suppose Nn & Sn,m & [P] (H P & Mn,P). Indeed, suppose H P & Mn,P for some P as promised. Then H (P+) by Q9. ~PP by Q4. Then Mm,(P+) by F5 and Q6.

Q11 POTINF
Pf: Suppose Nn. By Q10, H P & Mn,P for some P. ~PP by Q4.

Q12 (P)(Q)(n) ( Nn & Mn,P & Mn,Q & P cnt Q => P eqv Q )
Pf: By induction. True by F4 for n = 0. Suppose then Nn & Sn,m & ~ m = 0 (P)(Q)(Nn & Mn,P & Mn,Q & P cnt Q => P eqv Q). And suppose Nm & Mm,P & Mm,Q & P cnt Q. As usual, m = 0 has already been shown, so we may suppose ~ m = 0. Then ~Pa for some a, and we let P' = P \ {a} and Q' = Q \ {a}. By F5, Mn,P' and Mn,Q'. Obviously, P' cnt Q'. By the induction hypothesis, P' eqv Q'. So P eqv Q.

Q13 ACTINF
Pf: Suppose Nn & Mn,{x : x = x} for some n. By Q11, Mn,P & ~Pa for some P and a. Evidently, P cnt {x : x = x}. By Q12, P eqv {x : x = x}. But then ~{x : x = x}a, contradicting F1.

Now as my high-school English teachers were always fond of saying, "Compare and contrast the two systems." And maybe I'm just a little biased, but there are assumptions in the Fregean system which I would not choose to make.

Boolos himself criticizes B3, citing the case of {x : x = x}. Now I think he is correct in his criticism, but by singling out this set/class/predicate, he has taken the easy route, and he is appealing to the gut instincts of his audience, who largely believe in ZF, where {x : x = x} doesn't exist, much less have a number. But really the difficulty is much more widespread: there is no reason to suppose that most sets have a number. This idea (sorry for the polemics, but it must be said) is best called Cantor's Fallacy, since Cantor was the first to suppose that by some magical capability, we could abstract from the fact that P and Q are equinumerous (can be put into 1-1 correspondance) to the thesis that P and Q both have a number and indeed the same number. And there just is no reason to suppose this, anymore than there is to suppose that N or the real numbers R or, yes, {x : x = x}, have a number.

Nor is B3 the only dubious axiom. Once B3 establishes that N has a number, it is B4 which implies that the even numbers have the same number as all the natural numbers, which again is a modern prejudice dating from Cantor, without any particular backing. Even if one were to accept B4 as true, it would seem more of the nature of something to be proved, rather than assumed.

Finally, even B7 seems a bit over-reaching. Because of it, Sm,n implies that there are n (and m) objects, which again seems more something which should be proved, rather than assumed. That 100 succeeds 99 shouldn't "mean" that there are 100 things.

Against this, the second system only assumes that predicates may be objects. While this goes against the separation of object-concept most notably put into place by Frege, and also the set-class distinction which logicians are very comfortable with, it nonetheless is the more natural approach. As Quine insisted, if you're quantifying it, then it is an object. If "All P have a number" (the assumption B3), well then P certainly seems to be an object.

All this goes to suggest that Frege's proof has serious problems. Nonetheless, to give Frege his due, the "bootstrap" technique does in fact go through, in second-order logic with only predicative comprehension, using different axioms, indeed F3, F4, F5, and F6.

So, Frege is much like Dedekind in this respect: he must be credited with the major intuition and insight, but criticized ultimately for his particular implementation. In short, in this particular contest between Dedekind and Frege, it is not a victory for Frege, but a draw.