Finitistic interpretation of Nelson's internal set theory

Question

What does “standard” in internal set theory really mean? Is it secretly a way of reconciling conventional mathematics with (ultra)finitism?

Until recently I thought “standard” was just a way of talking about an elementary submodel but after reading Nelson's later writings it seems to me there is a more interesting and intuitive way of thinking about “standard”: standard things are the specific/definite things that mathematicians have hitherto conceived of and are concerned with. Since (as far as we know) the history of mathematics is finite, there are at most finitely many standard things. On the other hand, every day some mathematician somewhere conceives of some new definite thing, so the meaning of “standard” is dynamic and cannot be pinned down sufficiently to be allow “standard” to be used freely in (internal) set formation etc.

Since this is MathOverflow I suppose I should try to ask a precise mathematical question.

Ultimately, the reason why nonstandard models are called so is because their internal notion of finite (or countable or whatever) is “obviously” different from the external notion of finite (or countable or whatever). However, Nelson has emphasised from the beginning that internal set theory should be understood as a syntactic extension of conventional set theory, with new quantifiers $\forall^\textsf{st}$ and $\exists^\textsf{st}$, and new axioms. As it happens (or, rather, by design) these new quantifiers can be replaced with ordinary quantifiers after introducing a new predicate $\textsf{st}$, so it is unnecessary to invent a new notion of model that directly interprets $\forall^\textsf{st}$ and $\exists^\textsf{st}$; the cost is that models are necessarily nonstandard. Could we avoid this by inventing a direct interpretation of $\forall^\textsf{st}$ and $\exists^\textsf{st}$?

Although $\forall^\textsf{st}$, $\exists^\textsf{st}$, $\forall$, and $\exists$ can be nested in any order in a closed formula, Nelson's reduction algorithm gives an equivalent prenex form where all the quantifiers appear at the beginning in the order mentioned just now, at which point the transfer principle is applicable. This suggests that a natural syntax for nonstandard analysis is some kind of type theory distinguishing between “external” variables, which are restricted to have standard values, and “internal” variables, with semantics where in the interpretation of any particular subformula, there are really only finitely many “standard” values for each variable in context. Surely someone must have tried this already? What goes wrong?

I suppose one difficulty is that even after applying a $\forall^\textsf{st}$ or $\exists^\textsf{st}$, the variable does not completely disappear from the interpretation but is instead replaced with an “external” variable that controls what elements are to be considered “standard” in the interpretation. This is because the interpretation of “standard” must be specific to each variable if there are to be only finitely many “standard” values. Consider $\forall^\textsf{st} (m : \mathbb{N}) \exists^\textsf{st} (n : \mathbb{N}) (n = m + 1)$: obviously, the meaning of “standard” for $m$ has to be different from the meaning of “standard” for $n$. This is supported by Nelson's reduction algorithm, which reduces the formula to: $$\forall (m' : \mathscr{P}_\textrm{fin} (\mathbb{N}) ) \exists (n' : \mathscr{P}_\textrm{fin} (\mathbb{N}) ) \forall (m : m') \exists (n : n') (n = m + 1)$$ Could the inability to set the meaning of “standard” uniformly per type be not a mere nuisance but actually a deep problem?

Answer 1

Building on work by Benno van den Berg et al, the quantifiers $(\forall^{st}x)$ and $(\exists^{st}x)$ can be interpreted as "for all computationally relevant objects $x$" and "there exists a computationally relevant object $x$". Here, $x$ should be of finite type and our logic can be classical without problems.

Formally, if we can prove $(\forall^{st} x)(\exists^{st} y)\varphi(x, y)$ for some internal $\varphi$ in some restricted version of classical NSA, then from that proof we can read off an algorithm $t$ such that $(\forall x)(\exists y \in t(x, z))\varphi(x, y)$ holds in standard mathematics. The variable $z$ collects various oracles; for instance if the NSA-proof uses Transfer for arithmtical formulas, then the Turing jump is among $z$.

This paper contains a lot of details and examples.

Expressed in a different way, the standard quantifiers have computational content while the usual quantifiers do not have computational content. Helmut Schwichtenberg pioneered quantifiers with computational content in MINLOG. Agda later adopted the "dot notation" and even later there is truncation in HoTT.

Thus, classical NSA is replete with computational content, while e.g. Bishop and Connes have claimed the polar opposite.