Model-theoretic accounts of feasibility in bounded arithmetic and related systems 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. 
 A: In my answer to a related question on MO, I took the point of view that vagueness needs to enter the picture somehow or another.  To see this, simply ask the question, if you add 1 to a feasible number, do you always get a feasible number?  Classically, if vagueness is verboten, the answer to this question has to be an absolute yes or an absolute no.  But then there is no way to allow feasible numbers to peter out gracefully into nothingness when you get too big.
If you try to corner a feasibilist with this paradox by asking whether 1 exists, whether 2 exists, whether 3 exists, and so on, hoping to discover a sharp boundary, then a clever feasibilist will pause $n$ units of time before answering "yes" to the question "Does $n$ exist?"
To me, this suggests that if one wants to develop a classically precise theory of feasibility, then it is more promising to start by modeling feasibilists, and then define feasible numbers in terms of the behavior of a feasibilist, than to try to develop a classically precise concept of a feasible number directly.  I'm not aware of anyone who has done this, though.
A: Did you look at Manucci and Cherubin's preprint about the model theory of ultrafinitism?  It wasn't that well developed, but I thought the envisioned approach was interesting.
http://arxiv.org/abs/cs/0611100
A: Is it good to say that feasible numbers must have little coding power? Say they are (non-standard) elements of some tame model of weak arithmetic. Consider the following tentative notion.
Let us say that $M\models I\Delta_0$ is tame if for every formula $\varphi(x,y)\in L(M)$ there is an $n$ and a $\Delta_0$-formula $\psi(x)\in L(M)$ such that $\neg\exists y\, \forall x<n\,[\psi(x)\leftrightarrow\varphi(x,y)]$.
Do tame models of $I\Delta_0$ exist? If they do, then some version of NIP model theory could be applicable there.
