Return to 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 revision to be useful and constructive. The left to right implication is more useful as 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)) \implies \exists y. \forall^{st} x. (\psi(x) \implies \phi(x, y))$$

This way, when constructing the $y$ in the hypothesis you actually have some information about $z$ to work with. The right to left implication seems to strong constructively for it's purpose and can be replaced with $\forall^{st} z. z \text{ finite} \implies \forall x \in z. st(x)$, which is classically equivalent.

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.

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.

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

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.

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 revision to be useful and constructive. The left to right implication is more useful as 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)) \implies \exists y. \forall^{st} x. (\psi(x) \implies \phi(x, y))$$

This way, when constructing the $y$ in the hypothesis you actually have some information about $z$ to work with. The right to left implication seems to strong constructively for it's purpose and can be replaced with $\forall^{st} z. z \text{ finite} \implies \forall x \in z. st(x)$, which is classically equivalent.

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.