Is there a constructive version of internal set theory?

Question

Is there a theory T such that:

• T includes all the axioms of CZF.
• T includes the Idealization, Standardization, and Transfer schemas from IST.
• Every axiom of T is a theorem of IST.
• T has Church's rule. Explicitly, for every formula $\phi$ in IST's language, if $T \vdash \forall^{st} x \in \omega. \exists^{st} y \in \omega. \phi(x, y)$, then there is a computable function $f$ such that $T \vdash \forall^{st} x \in \omega. \phi(x, f(x))$.

(If not, is there a nice way to adjust IST schemas that makes the answer yes (but such that adding LEM to T still results in the full IST)?)

EDIT: Thinking about it more, the Idealization schema probably needs revised to be the universal closure of $$(\forall^{st} z. z \text{ finite} \land \forall x \in z. \psi(x) \implies \exists y. \forall x \in z. \phi(x, y)) \iff (\exists y. \forall^{st} x. \psi(x) \implies \phi(x, y))$$ to be useful. That way, when constructing the $y$ on the left side you actually have some information about $z$ to work with.

---

A first candidate I considered was $\{\phi : \exists t. IST \vdash t \Vdash_{tr} \phi\}$ where $\Vdash_{tr}$ is from Definition 5.2 in CZF has the disjunction and numerical existence property but $t \Vdash_{tr} \phi$ is only defined for $\phi$ in the language of first order set theory (which does not include the IST axioms). The obvious generalization leads to things like $\exists N \in \omega. \forall^{st} m \in \omega. N > m$ requiring nonstandard realizers, and permitting those seems to cause problems.

The reduction algorithm in Internal set theory: A new approach to nonstandard analysis has a way to convert formulas in IST's language to first order set theory, and all of the IST axioms get translated to theorems of ZFC. So the next candidate is the set of statements that reduce to an axiom of CZF (or any set theory containing CZF which obeys Church's rule, such as IZF). The problem is that the reduction algorithm involves a conversion to prenex normal form, I can't figure out how to adapt the reduction algorithm to be compatible with intuitionistic logic.

Answer 1

As you have proven (by a well-known construction), one cannot expect to have full Transfer in constructive NSA. For different but related reasons, full Standardisation is off the table, though its restriction to reals seems semi-constructive. In fact, one can have Idealisation and weak versions of the other IST axioms, working in constructive/intuitionistic finite type arithmetic. There is even an associated proof translation (and reduction algorithm), which may well be adaptable to CZF.

In particular, you should take a look at the following paper by Benno van den Berg et al:

https://arxiv.org/abs/1109.3103

They consider Heyting arithmetic in all finite types (with function extensionalty). This is only the starting point, there are a number of follow-up papers (see google/mathscinet).

Answer 2

No

Even though I mentioned allowing for some flexibility in interpreting the question, I think I've ruled out any reasonable interpretation. This answer only relies on bounded transfer and the existence of a nonstandard natural number, which any reasonable theory of nonstandard analysis should have.

We will prove $$\forall^{st} x \in \omega. \exists^{st} y \in \omega. (y = 1 \land \text{the $x$th Turing machine halts}) \lor (y = 0 \land \text{the $x$th Turing machine doesn't halts})$$

The witness for this is solves the halting problem, and so obviously can't be computable.

CZF is more than enough to prove that for each natural number $N$, a Turing machine either halts within $N$ steps or it doesn't, since that is a finite computation. Let $N$ be nonstandard and do a proof by cases.

Case 1, the $x$th Turing machine halts within $N$ steps: the Turing machine halts, and we let $y = 1$.

Case 2, the $x$th Turing machine doesn't halt within $N$ steps: since $N$ is greater than every standard natural number, we get that the Turing machine doesn't halt within $n$ steps for any standard $n$. By transfer, this means the Turing machine doesn't halt within $n$ steps for any $n$. So the Turing machine doesn't halt. We let $y = 0$.

So our theory let's us solve the halting problem, and is thus incompatible with church's rule.

$\square$

Basically, the problem is that by expanding the domain of discourse to include nonstandard objects, previously computable things like "a Turing machine either halts within $N$ steps or it doesn't" encodes what is from a meta point of view an infinite computation.

Answer 3

In Moerdijk, A model for intuitionistic non-standard arithmetic there is a sheaf topos for non standard analysis built within a constructive metatheory. By carrying out the construction internally in the effective topos, he showed overspill is compatible with Church's thesis. It is possible to use algebraic set theory to obtain models of set theory with similar properties to a topos, including the toposes studied by Moerdijk, although as far as I can tell noone has looked in detail at using this to study constructive versions of Nelson's IST. In addition to the papers other people have already pointed out, see Palmgren, A sheaf-theoretic foundation for nonstandard analysis for a further development of the constructive topos theoretic approach (but not about IST), and the PhD thesis, Paiva Miranda De Siqueira, J. V. Tripos models of Internal Set Theory for connections between topos theory and IST (but which seems to be non constructive).