Is there a theory T such that:


* T includes all the axioms of [CZF](https://en.wikipedia.org/wiki/Constructive_set_theory).
* T includes the Idealization, Standardization, and Transfer schemas from [IST](https://en.wikipedia.org/wiki/Internal_set_theory#Formal_axioms_for_IST).
* Every axiom of T is a theorem of IST.
* T has [Church's rule](https://en.wikipedia.org/wiki/Disjunction_and_existence_properties#Related_properties). 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](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.2816)* 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](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.8758)* 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.



Is there a constructive version of internal set theory?
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).


