Various weak theories of arithmetic have been partially motivated by a concern with numbers (or functions/proofs) that are feasible. This concern is sometimes connected to an interest in strictly finitistic approaches to arithmetic.
Examples of work where this concern is apparent are Parikh's work on bounded arithmetic, Sazonov's systems of feasible numbers, or Nelson's work on Predicative Arithmetic.
While the precise account of feasibility varies across these systems, the general idea is that the theory should prove that
- 0 is feasible
- if $n$ is feasible then so is its successor $S(n)$
- the feasible numbers are in some sense 'bounded'
There are various ways of making this last statement precise: e.g. we can see it as a statement of the form $\exists xy \neg\exists z (z= \exp(x,y))$ stating that some fast-growing function is not total (or, as in the case of $I\Delta_{0}$, it may suffice to know that exponentiation -- and, by Parikh's Theorem, any function with superpolynomial growth -- is not provably total, so that the above is at least consistent with $I\Delta_{0}$). A different approach is to give some explicit upper bound on feasibility, and require the theory to prove $\forall x (\log_{2}\log_{2}x<10)$, as in Sazonov's $\texttt{FEAS}$ system.
My question: is there any model-theoretic, or more broadly 'semantic', account of feasible numbers? Preferably, an account that would be (1) helpful in providing a clear mathematical picture of the structure of feasible numbers and/or (2) acceptable by the strict finitist's own lights?
A word on the two desiderata: in the above systems, characterisations of feasibility are rather implicit, as well as very sensitive to the underlying language and proof systems. Moreover, models of those theories (when they exist) seem to fail both (1) and (2).
For instance, models of $I\Delta_{0}$ where $\exp$ is not total (say, obtained via cuts of nonstandard models of PA) are not, presumably, objects to be taken seriously by the strict finitist as `concrete' objects, be it only due to their size. In addition, they hardly seem to be good models of 'intuitively feasible' numbers: their domains are basically given by (possibly nonstandard) integers bounded above by a power of some infinite nonstandard integer. The link to feasibility, or counting, or smallness, is very unclear, and it does not help building a mental picture consistent with the strict finitist's motivations.
Sazonov's theory is downright inconsistent in the classical sense (i.e. if we allow unbounded proof length), so it admits no (classical) models.
So: is there a serious mathematical account of 'feasibility' of this kind?
Some additional remarks:
Many logicians, like Gaifman, suggest a connection with vagueness, as the feasible numbers can be seen as forming a vague set. But do we really need to resort to vagueness to provide semantics for feasible numbers?
One possibility is to attempt an account in modal terms, where we imagine a Kripke frame where states are finite sets of integers representing 'the numbers we've counted to so far', and accessibility relations represent something like reaching further numbers via applying 'feasible' functions to the current (finite) domain. Of course, the Kripke frame would have infinite domain, but one could at least argue that it models feasibility in a way that gets things right 'locally', in providing an intuitive mental picture of the process of constructing numbers. But it is difficult to see how any construction of this sort could account in any way for the role played by particular notation systems or induction axioms (bounded induction).
I understand that most strict finitists are not concerned with giving a semantic account of arithmetic; some (like Nelson) are explicit formalists, and regard `semantics' as an unnecessary, or perhaps even misleading, distraction. At the very least, the idea seems to be that feasibility depends on the notational system used. This makes good sense from a constructivist perspective; feasible numbers are not a finished collection that our formal theory describes; instead, the theory describes the rules that we can employ to 'construct' numbers.
Nonetheless, there may be some intrinsic interest in the question of whether an elegant 'semantic' mathematical account of feasible numbers exists, or can be provided at all.