7
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Isn't this kind of defeating the porpoise? Do the hyperreals even provably exist in constructive settings? $\endgroup$
    – Asaf Karagila ♦
    Sep 12, 2022 at 6:57
  • 2
    $\begingroup$ I don’t know the topic well enough to give a proper answer, but have you looked at the work of Erik Palmgren on constructive nonstandard analysis? He has several papers on the topic — googling brings them up easily. $\endgroup$
    – Peter LeFanu Lumsdaine
    Sep 12, 2022 at 9:22
  • $\begingroup$ @AsafKaragila That's why we can't just use Nelson's model within CZF or something. IST doesn't give you access to the ultrafilter though, and I can't think of anything nonconsecutive that the additional axioms let you do. $\endgroup$
    – Christopher King
    Sep 12, 2022 at 15:47
  • $\begingroup$ @PeterLeFanuLumsdaine I didn't see anything that could specifically be extended to IST when I looked at Palmgren's work previously, but maybe I'll take another look. $\endgroup$
    – Christopher King
    Sep 12, 2022 at 15:49
  • 3
    $\begingroup$ @Asaf Karagila There are plenty of constructive approaches to Nonstandard Analysis (with metatheory Martin-Loef type theory) due to Erik Palmgren and co-authors. See google. $\endgroup$
    – Sam Sanders
    Sep 13, 2022 at 19:01

3 Answers 3

Reset to default
8
$\begingroup$

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

Improve this answer
$\endgroup$
6
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Very nice! Your proof is similar to this proof (Theorem 4.25) of Benno van den Berg and Jaap van Oosten's result that in the effective topos, Heyting arithmetic is categorical in the sense of admitting (up to isomorphism) exactly one model. $\endgroup$
    – Ingo Blechschmidt
    Sep 13, 2022 at 3:04
  • $\begingroup$ In the paper at doi.org/10.1016/0168-0072(94)00030-7 Palmgren put some syntactic restrictions on what formulas you can transfer. I think it has to prevent this kind of argument, since otherwise it would work fine in $\mathbf{HA}_\omega$and he claimed the theory there is conservative over $\mathbf{HA}_\omega$. $\endgroup$
    – aws
    Sep 13, 2022 at 16:25
3
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.