Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 5 of 5
Some time ago I answered a question at M.SE about why a topos with NNO was not sufficient for ordinary mathematics, to the effect that one only has intuitionistic logic, and anything requiring choice or excluded middle was lost. I received a comment today asking what happens if we throw choice in the ring, and so have ETCS without well-pointedness. I’m not enough of a topos guru to think of an example about what might break if we have to rely on generalised elements instead of working with a generator which is terminal. I know that people here have thought about the other alternative (ETCS - choice), but I haven’t seen anything on this permutation of the axioms.
Can we do things like calculus in a topos with NNO and Choice, using a real number object?
Well pointedness is a red herring; it just allows us to reason in a more natural language. The internal language of a topos with NNO and choice is sufficient to do ordinary mathematics, but it doesn’t match the external language.
Mike can probably explain this better than I can.
Right; or, put another way, every topos internally considers itself to be a well pointed topos, in a natural sense, so anything you can do with a well pointed topos, you can do in the internal logic of an arbitrary topos.
It seems to me, in taking seriously the idea of using a topos as one’s foundational environment, that one should only ever be reasoning internally to the topos and not worrying about how to describe that topos from the external perspective of some other foundational environment, anyway, so to speak.
@Sridhar and Toby - I think I agree.
in taking seriously the idea of using a topos as one’s foundational environment, that one should only ever be reasoning internally to the topos and not worrying about how to describe that topos from the external perspective of some other foundational environment
I agree also, but I would say the same thing like this. The theory of a non-well-pointed topos is not a very good foundational theory. The theory of a well-pointed topos is a (structural) set theory, and we know how to build mathematics out of sets. The theory of a non-well-pointed topos is a theory of some objects that behave a bit like sets in some ways, but very unlike sets in many important ways.
It just so happens that if you have, in some external theory T (which might, itself, be the theory of a well-pointed topos, or it might not) a model S of the theory of a non-well-pointed topos, then S gives rise to a “compilation” or “translation” or “encoding” of statements in the language of a well-pointed topos into statements in the language of T, which is sound. Therefore, anything we prove in the foundational theory of a well-pointed topos can be translated into a different true statement in the theory T that says something about the model S.
In other words, I don’t usually think of non-well-pointed toposes and internal logic as part of the usage of topos theory to provide a foundation for mathematics, but rather as part of the application of that fact to give us an easier way to prove things about toposes that we are led naturally to construct as part of the process of doing mathematics (presumably within some particular foundational system, but the nature of that system being mostly irrelevant).
1 to 5 of 5