Ultrafinitism with a largest number

The theory of finite arithmetic is a form of ultrafinitism asserting that there is a largest natural number. But where should the numbers stop and why exactly there?

In my post last week on Ultrafinitism, we introduced and discussed the philosophy of ultrafinitism, the view that only comparatively small or accessible numbers exist. According to ultrafinitism, the various extremely large numbers that mathematicians conventionally take themselves to describe, such as 2¹⁰⁰ or 10^100!, do not actually exist, and it partakes of a kind of illusion to speak of them.

Some forms of ultrafinitism posit a class of feasible numbers and then assert that the number 0 is feasible; that the class of feasible numbers are closed under the successor operation n ↦ n + 1; and also that 2¹⁰⁰ is not feasible. Proponents then take pains to design the accompanying logical apparatus, of course, so as to prevent what would otherwise be the inevitable inconsistency by blocking attempts to carry out an inductive proof for that many steps. In the previous essay, I argued that these logical maneuvers amount in effect to implementing a measure of ultrafinitism in the metatheory, seeking in effect to allow only feasible terms and feasible proofs.

Meanwhile, I also discussed another, totally different approach to ultrafinitism, an approach that is less often discussed, but which I find to be in strong accordance with core ultrafinitist ideas. Namely, this alternative view arises from the simple idea that there could be a largest number. We introduced and discussed the theory I call finite arithmetic, abbreviated FA, which axiomatizes an approach to arithmetic with a largest number. I should like to further explore this theory today. This theory is also known as PA^top.

Welcome to this second in a series of four critical essays on ultrafinitism, which are appearing here on Infinitely More in the ultrafinitism tag. These essays grow out of a talk I gave at the conference Ultrafinitism: Physics, Mathematics, and Philosophy held at Columbia University last April, 2025.

We discussed last time the question whether FA is the same as the common theory of all the standard truncation models ℕ ↾ n—we proved that it is not. In fact, the theory consisting of all sentences true in all the standard truncation models ℕ ↾ n admits of no computable axiomatization, since from any such axiomatization one could solve the halting problem. So it is difficult even for us to write down that common truncation-model theory, whereas FA consists of a simple list of axioms.

We also mentioned last time the ad hoc criticism, which objects to FA on the grounds that it cannot be our final, best account of the nature of arithmetic, in light of the deeply contingent, arbitrary nature of stopping at that particular largest number N. Why should the numbers stop sharply right at that point and not go on a little further? Why not define N + 1 somehow, as well as N · 2 and even N² somehow, and thereby provide a suitable, meaningful extension of the arithmetic operations up to larger numbers? It strikes many as absurd that our best, ultimate theory of arithmetic would posit the existence of a largest number.

In this essay, I shall aim to give mathematical legs to the ad hoc criticism by explaining the proof that every model of FA interprets a strictly taller model of this same theory. The fact of the matter is that inside any model of FA we can interpret a strictly taller model of FA in which the formerly largest number N now achieves its square N² or indeed N³ or much more. Indeed, it follows from this that in fact, all sums and products of members of M become fully defined in this taller model, even if they were not meaningful in the original model M. That is, all the undefined cases of sums and products in M become meaningful in the taller model. This picture therefore begins to reveal a fundamentally potentialist aspect to the nature of arithmetic, where the extent and nature of the arithmetic operations are gradually revealed via a possibility modality operator.

Ultimately, by iterating these interpretations to a limit, we shall prove next time that every model of FA arises via truncation from a model of bounded induction IΔ₀, a result due originally to Jeff Paris.

Let’s get into it.