# Is there any formal foundation to ultrafinitism?

Ultrafinitism is (I believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been primarily studied by Alexander Esenin-Volpin. On his opinions page, Doron Zeilberger has often expressed similar opinions.

Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get your hands on coming from a purely classical perspective?

Edit: Neel Krishnaswami in his answer gave a link to a paper by Vladimir Sazonov (On Feasible Numbers) that seems to go a ways towards giving a formal foundation to ultrafinitism.

First, Sazonov references a result of Parikh's which says that Peano Arithmetic can be consistently extended with a set variable $F$ and axioms $0\in F$, $1\in F$, $F$ is closed under $+$ and $\times$, and $N\notin F$, where $N$ is an exponential tower of $2^{1000}$ twos.

Then, he gives his own theory, wherein there is no cut rule and proofs that are too long are disallowed, and shows that the axiom $\forall x\ \log \log x < 10$ is consistent.

• Edward Nelson is another well-known exponent of untrafinitism. He has many essays about it on his webpage here : math.princeton.edu/~nelson/papers.html Oct 30, 2010 at 2:45
• Winking emoticons aside, it's probably good to have people like Nelson and Zeilberger around, to test received opinions and keep people on their toes. Oct 30, 2010 at 12:53
• I hope everyone has heard the story told by Harvey Friedman: "I have seen some ultrafinitists go so far as to challenge the existence of 2^100 as a natural number, in the sense of there being a series of 'points' of that length. There is the obvious 'draw the line' objection, asking where in 2^1, 2^2, 2^3, … , 2^100 do we stop having 'Platonistic reality'? Here this … is totally innocent, in that it can be easily be replaced by 100 items (names) separated by commas. I raised just this objection with the (extreme) ultrafinitist Yesenin-Volpin during a lecture of his." (cont...) Oct 30, 2010 at 22:37
• "He asked me to be more specific. I then proceeded to start with 2^1 and asked him whether this is 'real' or something to that effect. He virtually immediately said yes. Then I asked about 2^2, and he again said yes, but with a perceptible delay. Then 2^3, and yes, but with more delay. This continued for a couple of more times, till it was obvious how he was handling this objection. Sure, he was prepared to always answer yes, but he was going to take 2^100 times as long to answer yes to 2^100 then he would to answering 2^1. There is no way that I could get very far with this." Oct 30, 2010 at 22:38
• @Zsban,Daniel: Those are real numbers, not integers. Perhaps we know their values to less than 100 bits of accuracy... May 23, 2011 at 21:05

Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get your hands on coming from a purely classical perspective?

There are no foundations for ultrafinitism as satisfactory for it as (say) intuitionistic logic is for constructivism. The reason is that the question of what logic is appropriate for ultrafinitism is still an open one, for not one but several different reasons.

First, from a traditional perspective -- whether classical or intuitionistic -- classical logic is the appropriate logic for finite collections (but not K-finite). The idea is that a finite collection is surveyable: we can enumerate and look at each element of any finite collection in finite time. (For example, the elementary topos of finite sets is Boolean.) However, this is not faithful to the ultra-intuitionist idea that a sufficiently large set is impractical to survey.

So it shouldn't be surprising that more-or-less ultrafinitist logics arise from complexity theory, which identifies "practical" with "polynomial time". I know two strands of work on this. The first is Buss's work on $$S^1_2$$, which is a weakening of Peano arithmetic with a weaker induction principle:

$$A(0) \land (\forall x.\;A(x/2) \Rightarrow A(x)) \Rightarrow \forall x.\;A(x)$$

Then any proof of a forall-exists statement has to be realized by a polynomial time computable function. There is a line of work on bounded set theories, which I am not very familiar with, based on Buss's logic.

The second is a descendant of Bellantoni and Cook's work on programming languages for polynomial time, and Girard's work on linear logic. The Curry-Howard correspondence takes functional languages, and maps them to logical systems, with types going to propositions, terms going to proofs, and evaluation going to proof normalization. So the complexity of a functional program corresponds in some sense to the practicality of cut-elimination for a logic.

IIRC, Girard subsequently showed that for a suitable version of affine logic, cut-elimination can be shown to take polynomial time. Similarly, you can build set theories on top of affine logic. For example, Kazushige Terui has since described a set theory, Light Affine Set Theory, whose ambient logic is linear logic, and in which the provably total functions are exactly the polytime functions. (Note that this means that for Peano numerals, multiplication is total but exponentiation is not --- so Peano and binary numerals are not isomorphic!)

The reason these proof-theoretic questions arise, is that part of the reason that the ultra-intuitionist conception of the numerals makes sense, is precisely because they deny large proofs. If you deny that large integers exist, then a proof that they exist, which is larger than the biggest number you accept, doesn't count! I enjoyed Vladimir Sazonov's paper "On Feasible Numbers", which explicitly studies the connection.

I should add that I am not a specialist in this area, and what I've written is just the fruits of my interest in the subject -- I have almost certainly overlooked important work, for which I apologize.

• Thanks! That Sazonov paper (which is available not through Springer here: csc.liv.ac.uk/~sazonov/papers/lcc.ps) seems quite interesting. It makes me think the correct answer to my original question might be "yes"! Oct 30, 2010 at 17:53
• Taking cut away is really brutal, though -- it's mathematics with no lemmas allowed! This is where linear logic shines: it lets you bound the size of the expansion from the abbreviation power of lemmas. Oct 30, 2010 at 18:21
• @Sune: This is a flooring division, so $x/2$ gives the largest integer less than or equal to $\frac{x}{2}$ For example, $3/2 = 1$. In particular, this means that in general we only have $2 \times x/2 \leq x$. Oct 31, 2010 at 10:12
• A clarification: Buss’s polynomial induction schema is equivalent to usual induction. It only gets weak when you severely restrict the class of formulas allowed in the schema, and this works for usual induction too. When the schemata are restricted to a class of formulas not closed under bounded quantification, the two schemata are no longer equivalent, hence both are used to axiomatize different theories of bounded arithmetic (such as $S^1_2$). However, what makes these theories weak is the restriction on formula complexity, not the form of the induction schema. Jun 7, 2011 at 14:51
• Reliance on complexity appears strange. The usual notion of polynomial computability only makes sense as an observation of asymptotic behaviors. In other words, how fast computation happens within a range of input sizes taken from just an initial segment of natural numbers has no influence whatsoever on determining whether the computation is polynomial or not, or even bounded by a constant. This seems to clash with the basic philosophy of finitism. Sep 17, 2019 at 13:12

I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather than an answer. (I'm interested in the answers that have already been given though.) My question is this. Is there a system of logic that will allow us to prove only statements that have physical meaning? I don't have a formal definition of "physically meaningful" so instead let me try to illustrate what I mean by an example or two.

Consider first the statement that the square root of 2 is irrational. What would be its physical meaning? A naive suggestion would be that if you drew an enormous grid of squares of side length one centimetre and then measured the distance between (0,0) and (n,n) for some n, then the result would never be an integer number of centimetres. But this isn't physically meaningful according to my nonexistent definition because you can't measure to infinite accuracy. However, the more finitistic statement that the square root of 2 can't be well approximated by irrationals has at least some meaning: it tells us that if n isn't too large then there will be an appreciable difference between the distance from (0,0) to (n,n) and the nearest integer.

As a second example, take the statement that the sum of the first n positive integers is n(n+1)/2. If n is too huge, then there is no hope of arranging a huge triangular array and counting how many points are in it. So one can't check this result experimentally once n is above a certain threshold (though there might be ingenious ways of checking it that are better than the obvious method). This shows that we can't apply unconstrained induction, but there could be a principle that said something like, "If you keep on going for as long as is practical, then the result will always hold."

One attitude one might take is that this would be to normal classical mathematics as the use of epsilons and deltas is to the mathematics of infinities and infinitesimals. One could try to argue that statements that appear to be about arbitrarily large integers or arbitrarily small real numbers (or indeed any real numbers to an arbitrary accuracy) are really idealizations that are a convenient way of talking about very large integers, very small real numbers and very accurate measurements.

If I try to develop this kind of idea I rapidly run into difficulties. For example, what is the status of the argument that proves that the sum of the first n integers is what it is because you can pair them off in a nice way? In general, if we have a classical proof that something will be the case for every n, what do we gain from saying (in some other system) that the conclusion of the proof holds only for every "feasible" n? Why not just say that the classical result is valid, and that this implies that all its "feasible manifestations" are valid?

Rather than continue with these amateur thoughts, I'd just like to ask whether similar ideas are out there in a better form. Incidentally, I'm not too fond of Zeilberger's proposal because he has a very arbitrary cutoff for the highest integer -- I'd prefer something that gets fuzzier as you get larger.

Edit: on looking at the Sazonov paper, I see that many of these thoughts are in the introduction, so that is probably a pretty good answer to my question. I'll see whether I find what he does satisfactory.

• In this system of logic, should the Poincare recurrence theorem be provable? In some way it contradicts the second law of thermodynamics... Nov 4, 2010 at 18:16
• If I am not making a mistake, the mathematical philosophy you are referring to is called actualism. I also think finite model theory is relevant here, they use rational languages (no function symbols like + and .) to avoid forcing the models to be infinite. Nov 9, 2010 at 23:51
• Tim: "can't be well approximated by rationals". Sep 17, 2019 at 13:15
• The second law of thermodynamics is only a "law" statistically. There is no physical mechanism preventing, for instance, a dumbbell-shaped container with two gases mixed together from spontaneously segregating itself; all the second law says is that, at the scales we can see, it's so unlikely that it's pretty much impossible. Sep 27, 2019 at 0:56
• @Zemyla : This statistical sense in which the second law of thermodynamics is correct is much like the sense in which the ultrafinitists are correct that very large numbers don't exist. You say that such a container of gases could unmix, but if you actually make the container and observe it, it never will. I don't have an ironclad proof of that, just as I don't have an ironclad proof that I'll never count to a googolplex, but it's true all the same. Jun 23, 2021 at 18:31

Here is an ultrafinitist manifesto (link) I have co-written a few years ago:

  http://arxiv.org/pdf/cs/0611100v1


It is absolutely not a finished paper (there are a few inaccuracies, and many parts are sloppy), but it contains a brief history of ultrafinitistic ideas from the early greeks all the way to present time, a number of refs, as well as a sketch of a programme towards a model theory and a proof theory of ultrafinitistic mathematics.

You may also want to google the FOM list on "ultrafinitism", there are a few posts by Podnieks, Sazonov, myself, and a few others pro and contra ultrafinitism.

• The most recent on FOM being the thread I started in March cs.nyu.edu/pipermail/fom/2011-March/015326.html and the subsequent replies and links. May 24, 2011 at 2:03
• I added a link to the arXiv abstract page May 24, 2011 at 2:26

I've always thought that assuming a formalist position (i.e., mathematics is merely the manipulation of symbols) easily allows for an ultrafinitist position. The formalist may easily grant that $b=10^{10^{10^{10}}}$ is a formal number, in the sense that it is permissible in the grammar,

(e.g., $\log_{10}(10^{10^{10^{10}}})>10^{9^8}$ is TRUE)

without it being an ontological number (case and point: there is no string of characters which is $10^{10^{10}}$ long, the length of would-be decimal representation of $b$).

Similarly, axioms which fool us into thinking they are about infinity are happily read as finite strings, from which point they may be perfectly acceptable.

From this point of view, the entities which might otherwise be numbers, but will be rejected here, are not those which are expressible in a few characters or even a few pages of characters, but those for which no human will ever come close to expressing, calculating with, etc.

I am not advocating formalism here, but it seems to make ultrafinitism philosophically defensible. As I have put it, it also makes ultrafinitism inconsequential, except as a philosophical point.

• to manipulate symbols you need to accept something like finitism. Remember that Hilbert himself was fine with finitism, the goal of his formalism was reducing higher stuff to finitism. Sep 28, 2011 at 11:20
• An ultrafinitist would argue that any mathematics that is more consequential than a mere philosophical point is, pretty much by definition, ultrafinitist, and it is statements about very large numbers that are "inconsequential, except as a philosophical point."
– pron
Jan 8, 2020 at 0:32

One could take ETCS - which is a finite, first order axiomatisation of the category of sets - and remove the axiom that guarantees the existence of a natural numbers object. Then in this set up one can prove the existence of sets of finite cardinality, but not the existence of a set with cardinality $\geq \aleph_0$. Moreover one could weaken this to a finitist version of Palmgren's constructive, predicative version of ETCS, which would be a well-pointed $\Pi$-pretopos with enough projectives.

This latter version minus function sets (the '$\Pi$' in $\Pi$-pretopos) would perhaps be closer to Nelson's idea, because at one point he expresses doubts about the finiteness of $n^m := \{1,\ldots,n\}^{\{1,\ldots,m\}}$ for large $n$ and $m$. EDIT: I should say that in a formal setting this would translate to the unprovability of the statement "$n^m$ is finite", which would be the case in a model of a "finite set theory" without function sets.

Or one can just work with Nelson's arithmetic, which is the most ultrafinitist thing I know. For example, exponentiation is not a total function in his theory.

• A &Pi;-pretopos still has exponentials, which means that $n^m$ will still exist. So I think you want a non-&Pi; pretopos if you want to exclude exponentials. Nov 1, 2010 at 0:30
• Ah, thanks. I'll edit the answer to reflect that. Nov 1, 2010 at 0:46
• Still a minor error: you identify the "&Pi;" "&Pi;-pretopos" as power sets, but it's actually function sets (exponentials). Palmgren's theory, being (weakly) predicative, already lacks power sets (and it's possible to have function sets without power sets because of the intuitionistic logic). Sep 9, 2011 at 22:24
• Hm, ok. Would it be ok if I just changed it to 'latter version minus function sets (the '$\Pi$'..' Sep 9, 2011 at 23:14
• Yes, that would be correct. Nov 28, 2012 at 6:23

Just my personal opinion, as a non-specialist in this area, is that ultrafinitism cannot be formalized for the same reason that the straw which breaks the camel's back cannot be formalized. We know that a healthy camel can carry one kilogram, but not 10 tons. So there must be some point at which the camel cannot carry another straw, but it is impossible to define. In practice, various things would start to go wrong with the camel as the limit is reached.

In the same way, we cannot list all of the elements of the von Neumann universe 6th stage, which contains $2^{65536}$ elements, which are the sets that you can construct from the empty set alone in ZF set theory up to a nesting depth of 6. However, it is not possible to say exactly what the bounds are for the representation of sets and numbers. There is some $n$ for which a truly random sequence of $2^n$ decimal digits cannot be written down. There are only finitely many atoms in the universe, one assumes, which means that there must be a bound on how large an integer can be written down. But things would just start to go badly wrong as we approach the limit. For example, we might run out of trees to make paper with, or we might run out of silicon to make memory chips with, and so forth.

My own personal solution to this problem is to divide all numbers into dark numbers, which include those real numbers which are truly random and therefore impossible to write as a finite formula as one would do for $\pi$, and grey numbers, which are clearly impossible to represent with all of the atoms in the universe, and then the bright numbers which we use every day, like 3. The problem with this classification is that there is no clear-cut boundary between the bright numbers and grey numbers. And in my opinion, there never will be, just as we will never be able to formalize how many straws will break the camel's back. The best approach, I think, is to acknowledge philosophically that there are limits, but to not worry about them in practice. Because in practice, we will never go over the limit.

There is this argument against Nelson's predicative arithmetic which basically says that the assumption that exponentiation is not total, which is in some sense the whole reason to start predicative arithmetic, implies the inconsistency of the predicative arithmetic.

• The link appears broken - do you have a stable one? Jan 10, 2021 at 22:48
• @NoahSchweber A Google result for mentions of that web address suggests it used to lead to "On The Untenability Of Nelson's Predicativism" by Stefan Iwan, which can be found at link.springer.com/content/pdf/10.1023/A:1005651027553.pdf. Sep 11, 2021 at 21:14

I would suggest the following axiomatization to my ultrafinitist friends. Let Nx mean "x is a natural number", Sxy mean "y succeeds x", and 0 to be "zero". The Peano Axioms are:

1/ N0

2/ S is into N

3/ S is total on N (every number has a successor)

4/ S is a function

5/ S is one-to-one

6/ 0 is not in the image of S

7/ Induction

Remove Axiom 3. Then the models of these axioms are: the standard model (if it exists) and the initial segments. {0} for instance is a model.

One can work either in second-order logic and define sequences as second-order entities (https://www.researchgate.net/publication/351561089_Arithmetic_Without_the_Successor_Axiom) or work in first-order logic and add sequences directly as first-order entities, with some additional axioms (https://www.researchgate.net/publication/354605078_A_Natural_First-Order_System_of_Arithmetic_Which_Proves_Its_Own_Consistency).

With sequences one can make the usual recursive definitions of addition, multiplication, and exponentiation, and then towers of powers. It will not, of course, be able to prove any of them total.

So the ultrafinitist who has any particular idea which numbers are permissible and which are not can simply add in the axioms he wants, such as

E/ "the product of 100 and 100 exist" and

F/ "a tower of 10 powers of 2 does not exist".

IMHO, these assumptions are not of any mathematical interest, since the system without Axiom 3 is capable of proving many mathematical theorems (Quadratic Reciprocity...), and adding any axioms such as E or F only adds trivial capabilities to prove additional theorems. So it is better, mathematically at least (and IMHO philosophically), to be agnostic about the successor axiom, rather than an atheist or a theist.

• Maybe statement E adds only trivial capabilities, but you would want to have some statements like it, such as the statement that the product of 2 and 2 exists (which is pretty relevant to, for example, quadratic reciprocity). Jun 23, 2021 at 18:58
• @TobyBartels. The system which I have described (without assumption E) is "downward" in the sense that if you know or you can prove that $n$ exists, every $m < n$ can be proven to exist. So Quadratic Reciprocity goes through without the assumption of E or "the product of 2 and 2 exists", because the theorem begins by "Let $p$ and $q$ be distinct odd primes." So every number less than $p$ or $q$ can be shown to exist, which suffices for the proof to go through.
– abo
Jun 24, 2021 at 20:11
• I meant that some of the statements that we think of as part of QR refer to $4$, as in ‘if $q \equiv 1 \pmod 4$, then …’. But I see your point; we don't have to accept that $4$ exists in order to state that as a hypothesis. Jun 25, 2021 at 21:46
• @TobyBartels. I'm not clear on your last sentence. If p and q are distinct odd primes, then 5 exists, so 4 exists. That is, the existence of 4 can be proven given the assumptions of QR.
– abo
Jun 26, 2021 at 5:18
• Yes, if you phrase it that way. The version labelled ‘Gauss's Statement’ at en.wikipedia.org/wiki/… doesn't require assuming that the primes are distinct. But I see that you did specify distinct primes in your phrasing; my mistake. Jun 28, 2021 at 4:09

This is an old question, and I'm far from a specialist, but I've recently been reading Dmytro Taranovsky's 2016 preprint Arithmetic with Limited Exponentiation, which seems to me highly relevant to this question.

In it, he constructs a hierarchy of theories with finitely many types $$I_0, ..., I_n$$, in which exponentiation is (essentially) an operation $$I_{k+1} \to I_k$$, taking us e.g. from the natural number $$x$$ to the type $$2^x$$ of binary strings with length $$x$$, which is not assumed to be finite. In this way, $$(n+1)$$-fold iteration of exponentiation, and the associated huge numbers, are undefined.

Nevertheless, Taranovsky shows that theories near the bottom of his hierarchy are enough to support a significant portion of ordinary mathematics. Not only that, but by failing to treat exponentiation as a function $$\mathbb{N} \to \mathbb{N}$$, each of the theories (but not their union) is interpretable straightforwardly in $$I\Delta_0$$, and therefore in Robinson arithmetic, which should be acceptable to all but the most hardcore ultrafinitists.

One can construct a consisten logic which explicitly limits computational complexity of valid statements, and thus is ultrafinitist: https://arxiv.org/abs/2106.13309