How is ultrafinitism imprecise

logicsoft-questionultrafinitism

This is similar to "Why isn't finitism nonsense?" but instead of asking about the practical nature (applications), or instead of asking about the definition, I'm trying to understand how ultrafinitism is imprecise (foundations/philosophy).

Consider the following paragraph from wikipedia (emphasis mine):

Some versions of ultrafinitism are forms of constructivism, but most constructivists view the philosophy as unworkably extreme. The logical foundation of ultrafinitism is unclear; in his comprehensive survey Constructivism in Mathematics (1988), the constructive logician A. S. Troelstra dismissed it by saying "no satisfactory development exists at present." This was not so much a philosophical objection as it was an admission that, in a rigorous work of mathematical logic, there was simply nothing precise enough to include.

And a recent source other than wikipedia:

Ultrafinitist views are notoriously hard to pin down precisely, …

Timothy Chow, Foundation of Math mailing list, https://cs.nyu.edu/pipermail/fom/2018-December/021296.html

Question: How is ultrafinitism imprecise?

Best Answer

It is simply that there is no formal system that is widely accepted as representing (a least common denominator of) ultrafinitist ideas. For constructivism, we have things like intuitionistic propositional logic, Heyting arithmetic, and constructive set theories. If you work in these systems you will generally be doing things that no constructivist will complain about. Similarly for predicativism (e.g. the internal language of pretopos) and finitism (PRA).

There are formal systems that are presented as "ultrafinistic", e.g. the system sketched in Sazonov's On Feasible Numbers, but I doubt Sazonov had any intent for this to be a comprehensive system that should be widely adopted by ultrafinitists. Vopěnka's Alternative Set Theory seems like it was intended as a more serious proposal, but (from the little I've read about it, so take this with a large grain of salt) it seems more focused on the notion of semisets (subclasses of sets) which provides an approach to vague predicates, e.g. the kinds of things that come up in the Sorites paradox. The relevance to ultrafinitism is that we can assert that all sets are "hereditarily finite" (or, rather, satisfy a first-order induction schema that roughly corresponds to that) but then assert that there's a proper semiset to model the "humanly describable" sets. The more levels of nested sets we exhaustively enumerate, the deeper this proper semiset must be but it is still contained in some set (and all sets are "hereditarily finite"). This allows reasoning about a "cutoff" "somewhere" but somewhere that's always beyond the horizon. However, this doesn't explicitly provide any concrete upper bound. I'm not familiar enough with Alternative Set Theory to say for sure, but I suspect that you could probably define some concretely very large things that would bother ultrafinitists.

Another aspect which is part of the point of Sazonov's paper is that an ultrafinitist theory would need an ultrafinitist meta-theory. Proof theory lets us reduce most other theories (e.g. ZFC) to a finitist meta-theory. You don't need to believe in uncountably infinite sets to believe in manipulating syntax that purports to talk about them in some deductive system. However, "reducing" an ultrafinitist theory to a finitist meta-theory isn't much of a reduction (which doesn't mean it wouldn't be useful). There are also aspects of the meta-theory that can leak back in to the theory.

Related Question