4
$\begingroup$

To prove there is an elementary topos with natural numbers object, it should be sufficient to assume ZF has a model. Probably ZF by itself, or IZF, is already sufficient. And probably even this is not necessary. Do we know what is?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

This question was studied in the early days of elementary topos theory, and the connection was worked out by Bill Mitchell and J.C. Cole (independently, as far as I know). The MathSciNet references are:

MR0319757 (47 #8299) Mitchell, William, Boolean topoi and the theory of sets. J. Pure Appl. Algebra 2 (1972), 261--274.

MR0357116 (50 #9584) Cole, J. C., Categories of sets and models of set theory. The Proceedings of the Bertrand Russell Memorial Conference (Uldum, 1971), pp. 351--399. Bertrand Russell Memorial Logic Conf., Leeds, 1973.

Essentially, they show that Boolean topos theory with a natural numbers object is equivalent to a version of Zermelo set theory (not ZF, i.e., without the replacement scheme) and with the separation scheme restricted to formulas with all quantifiers bounded (but the bounds can involve power sets, so quite a lot of separation is available). (I'm omitting some technicalities here, not because they're negligible but because I don't remember them.)

If you don't assume Boolean logic for your topos, I don't think it changes the consistency strength of the theory. In any nontrivial topos with a natural numbers object, the subtopos of double-negation sheaves will also be nontrivial and will have a natural numbers object (the associated sheaf of the original one). In other words, the double-negation translation of classical logic into intuitionistic logic works here.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ In particular, since in ZF you can prove the existence of models of Z, such as $V_{\omega+\omega}$, this would seem to verify that the OP's assertion that ZF by itself or something less is sufficient to get an elementary topos. $\endgroup$
    – Joel David Hamkins
    Jun 28, 2010 at 2:04
  • 1
    $\begingroup$ Joel, you're absolutely right. You get a very nice topos by taking as objects the sets in $V_{\omega+\omega}$ and taking as morphisms all functions between them. $\endgroup$
    – Andreas Blass
    Jun 28, 2010 at 2:41
  • $\begingroup$ I wouldn't have guessed it was below Z! In fact I never before saw that Z was more than just the union of n'th order arithmetic for all n. Thanks! $\endgroup$
    – Daniel Mehkeri
    Jun 29, 2010 at 0:43

Your Answer

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

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