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.