Do numbers exist? What a crazy question for a computer scientist to consider! I admit that my curiosity on this topic is not due to any application in Computer Science that I can see. Reading Feferman’s *In the Light of Logic*, though, has gotten me interested in some of the philosophical questions that some logicians — Feferman and Goedel are two notable examples — have devoted considerable attention to. This question regarding the ontological status of the objects of mathematics is considered by many very serious philosophers, certainly in the 20th century and no doubt before (though I know little about the history of the question). I think it is quite interesting to consider, since it sheds light on exactly what is happening when we do theoretical work.

The most straightforward answer to the question “Do numbers exist?” is simply, “yes (of course!)”. Numbers and more complex mathematical objects are indispensable to scientific practice, which W. V. Quine famously argued justified our acceptance (at least in some sense) of the existence of whatever objects mathematics requires, at least mathematics that is needed for scientific practice. But as Feferman argues in Chapter 14 of *In the Light of Logic* (and also in earlier chapters), the logical theories required in principle for the development of all the mathematics needed for modern science are quite weak in their ontological commitments. Indeed, Feferman puts forward theory W, a weak system of recursive operations on the natural numbers, and predicatively defined classes of such entities, and argues that it is sufficient for the needs of all of modern science. And theory W is a conservative extension of Peano Arithmetic, and proof-theoretically reducible to it. So enormously complex cardinal numbers, for example, need not be assumed to exist in order to carry out scientifically relevant mathematics. Thus if we follow Quine’s idea that we should accept mathematical objects that are needed for science, we need not accept such things. In this way Feferman rejects a strongly Platonist conception of mathematics, where the entire menagerie of higher set theory is accepted as actually existing.

But all this proof-theoretic fanciness is, in a sense, a distraction. After all, on Feferman’s approach we are still left with Peano Arithmetic at least. So just seeing that we do not need the more esoteric mathematical objects to do modern science does not let us avoid the question of whether or not (or how) numbers exist. And indeed, I personally am not motivated by Quinean concerns, which are ultimately rooted in naturalism. And naturalism, I suspect, ultimately represents a desire to banish the concept of God or other religious beliefs from intellectual discourse and indeed, from human life. There are very weighty reasons for thinking that that is a bad idea, which I will not discuss here: that topic is, of course, even more controversial than the existence of mathematical objects!

So: do numbers exist? Really I think we should consider two separate questions: do theoretical objects exist, and do abstract objects exist. While I have my doubts, it seems quite reasonable to believe that, at least in some sense, at least rather small finite numbers could be said to exist. I actually am open to persuasion on that point, but when I say the number of books on my desk is currently 4, maybe it is not just a figure of speech, but an actual statement about this thing called a number. I don’t know. But the question of whether or not theoretical objects exist — that is, objects that a particular theory is committed to — this seems clearer. Why on earth should we believe that just because a particular mathematical theory speaks of certain objects, that they definitely exist? I can easily write down a set of first-order formulas giving certain characteristics of unicorns, or ghosts, or whatever else you like. We would certainly not wish to say that because such a theory is committed to the existence of those things, they really exist. They might exist, of course. I could have a theory of cars, or other generally noncontroversially existing things. But just having a theory about them does not tell us anything about whether or not they exist. We would need some independent reason for believing in their existence.

Of course, in mathematics or other formal disciplines (Computer Science, too), people spend a lot of time working with the particular entities the theory considers. In Computer Science, one might work with Turing Machines, which are, of course, idealized computers with an infinite amount of memory. No computer has or perhaps physically could have an infinite amount of memory, so in that sense, Turing Machines do not exist. Working within a theory, it is natural to talk and act as though the theory were definitely true.

Perhaps psychologically, one must, in a sense, enter the world of the theory to be successful at deriving new theorems or reaching new insights into the theory. Indeed, this idea of entering the world of the theory suggests a modal interpretation of theoretical truth. A version of this interpretation is proposed by Hilary Putnam in “Mathematics without Foundations”, which can be found in his book *Mathematics, Matter, and Method*. The idea roughly is to say that when we assert a theorem of arithmetic, for example, as true, what we are really asserting is the necessary truth of the statement that the axioms of arithmetic imply the theorem. So any structure which satisfies the axioms of arithmetic will also satisfy the theorem. With this kind of perspective, “modalism” (which amusingly, Putnam says explicitly that he is not trying to start as an alternative foundational philosophy, though certainly it by now is) is a kind of structuralism, which asserts that structures exist, even if mathematical objects are identified only by their roles in such structures.

To me, structuralism’s structures are no better than the original mathematical objects. I would take a more proof-oriented version of modalism: to say that a theorem of a particular theory is true, is just to assert that it is provable from the axioms of the theory, using whatever logical axioms and rules one accepts. There is no ontological commitment at all there. Yes, we could understand this deductivist interpretation modally: if a structure exists that satisfies the axioms of the theory, then that structure will satisfy the theorem. But if we look at it that way, I think we must avoid phrasing this as above: “it is necessary that the axioms imply the theorem”. For this interpretation requires us to assume also that the axioms could be satisfied. If they absolutely could not be satisfied, then all formulas become theorems: if no structure models the axioms, then in every structure, the axioms are false, and the implication “axioms imply theorem” is true. I would not want to ground that modality in possibly existing structures — we’d just be back to where we started, because we would need a theory for those, and we’d be unsure of their status. It would be more acceptable to ground the modality in actually existing structures. So then the modal interpretation would amount to saying that for any structure that exists, if it satisfies the axioms, then it satisfies the theorem. But then arithmetic would become inconsistent if the universe is finite, for example. So we would not want to take this kind of more semantic modalism. We just need a more modal notion of implication, which we can find in constructive logic: if we were to enter a world where the axioms are true (regardless of whether or not there is such a world), then the theorem would be true. This has a bit of the air of the fictionalism I read attributed to Hartry Field. More simply, the theorem follows by the rules of logic from the axioms of the theory, and that is the end of the story from an ontological perspective.

Why one theory is of more use or interest than another is then a wholly separate question from whether or not use of the theory requires acceptance of the existence of the theory’s objects. Asserting a theorem, no matter how vivid the intuition for a world satisfying the axioms of a theory, is ultimately no more than asserting that the theorem follows deductively from those axioms.

Ok, after getting my attempts to learn some of this philosophy out of my system, I’ll be back to more technical topics next post.

## 6 Comments

Questions about the actual existence of mathematical objects have always confused me. In college, I was very happy to discover an intellectual history of working computer scientists with an alternate view. “It’s all in your head”, cries the intuitionist.

More to the point, I’m interested in Feferman’s claim that Peano arithmetic is all we need to formalize modern science. Surely complexity theory is “real” enough to be a concern here. And, through descriptive complexity, we know bounding the running time of programming problems is really asking questions about the (finite) models of logics. Sometimes very complicated logics, too big for Peano.

Hi, Chris. Thanks for your reply! Feferman here really is concerned with empirical science: physics, chemistry, that kind of thing. Back in the day, science of that kind was considered the highest form of human knowledge-gathering. I definitely agree with you that the mathematical or formal disciplines are another matter as far as the foundations they need, although even there, the program of Reverse Mathematics seeks (as I understand) to determine what axioms are required for which theorems, and has shown that lots of mathematics does not really need complex logic. Of course, when you actually get to something proof theory or set theory — well, you can’t analyze those systems without systems which are even stronger, of course.

I’ve commented before that I think we need something like “Reverse Type Theory”: to do the things we want to do, do we really need the full power of a system like CIC? A lot of that power is not being used in the applications where CIC is applied. So maybe there is a proof-theoretically weaker subtheory of something like CIC, that would serve many of the same purposes (although maybe not for generic proving as in your research — generic proofs seem as though they would be a lot like logical relations arguments, which we know could be proof-theoretically strong).

Hi Aaron,

I see now. Certainly complexity theory isn’t investigated empirically.

It does provide an interesting source of “real world” problems which have important implications for expressive logics, though. It still amazes me to think that the question of how quickly we can find the best route for a traveling salesman comes down to the expressive power of existential second order logic.

To come back around to “reverse type theory”, I wonder if this might inform our view of how strong a logic we need. Do we want to be able to prove (in the language itself) that our algorithms are “as fast as possible”? For harder and harder programming problems, this may require us to reason about progressively more complex logics.

I should confess that I’m taking a course in finite model theory right now, so these questions are improbably close at hand!

Chris,

I think you’ve raised an important question, at least for a language design effort like our Trellys project: what do we want the logic of the language to be able to do? Are we going to use it to prove low-level pointer programs correct? Then maybe we should use Hoare Type Theory or some similar system. Are we going to prove results about algorithms? Then I gather from what you are saying about your finite model theory course, that we might find we need an expressive logic for some of those arguments.

My vote is that we should be focusing on more lightweight verification, where our goal is not full program correctness, but dependently typed programming. We will not prove complex programs correct, but rather express some of their invariants (which a full correctness proof would require) using dependent types. Expressing the invariants might require some code, and we then might have to reason about that code. But that is specificational code, and we can hope that it uses relatively straightforward functions and data structures. There would certainly be little call for using fancy data structures in a specification, since efficiency of specificational code should not (as far as I can see) matter.

Aaron

I am a calculus student in high school and one day I was thinking about the concept that numbers could go on forever. I then, for some odd reason began to think about the space between zero and one. If decimal are indeed numbers, and numbers can continue to grow forever, how does the number one exist? in other words no matter how small, the number, what number comes right after zero? The answer is indeterminable because the zeros after the decimal can continue forever also, with this being said, I believe that numbers are just assumed values that don’t exist, because where does the fist decimal that includes the value of one occurs. I believe that the only “real” value we know about is zero. Can this be confirmed please?

Hi, LaStar. I think what you are wrestling with here is the fact that the real or rational numbers are

dense: there is a number between any two numbers. The integers are not dense, so the reals or rationals can seem strange, because not all of our intuitions about integer numbers apply to real numbers. Thanks for your comment.