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)?)

---

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 some other set theory with the disjunction property like 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.