Here’s something that I just learned: a topos, despite the fact it can model intuitionistic logic is not quite the right setting for a constructive set theory. The reason is that in a topos every function has an image. In a constructive set theory, the only sets whose existence you want to assert is those whose membership functions are explicitly computable. The image of a function between two infinite sets may not be explicitly computable.
(I think the correct analogue for constructive set theory is something called a quasitopos, but I don’t know much about them.)
You’re quite right that “constructive” means something very different for those who work in constructive analysis (after Bishop) to those who work in topos theory. I believe there’s much better agreement between the two senses if the topos is the effective topos or some other realizability topos, where the only functions from N to N are those which are Church-Turing computable. (I haven’t looked at Colin McCarty’s book on topos theory for this, but it’s probably worth a look-see.)
I don’t know too much about quasitoposes either, but there morphisms do have images, I’m pretty sure (I can give some details on request). There’s a book by Oswald Wyler on toposes and quasitoposes, which I haven’t looked at myself, but which should have lots of good info.
You might be right that that morphisms have images as objects (I’m not clear on that one way or the other, so I wouldn’t mind hearing the details), but they don’t have images as subobjects classified by the subobject classifier. Otherwise every subset would have a decidable membership function.
I’m not sure what’s up with the effective topos. Are functions in the effective topos partial? That would explain it.
My claim about images in quasitoposes was based on vague recollections of the exactness properties which hold in such categories, and a half-baked proof I constructed in my head when I wrote my comment. I was wrong: morphisms in a quasitopos apparently do not generally have image factorizations (defining the image of a morphism f as the smallest subobject through which f factors).
This makes your comment on quasitoposes as appropriate for constructive set theory rather more intriguing to me — would like to follow up on that. The archetypal example of a quasitopos is the category of separated presheaves on a site. Can we see constructive set theory this way?
Can you provide a reference (or a lengthier argument) for where you found this idea? After thinking about it quite a bit, I still can’t convince myself that it is true (or false).
In particular, it is not clear to me that a topos CSet would be forced by the topos axioms to include any problematic objects or morphisms between them: i.e. uncountable sets or graphs.
[...] was doing some web searches to see if I could answer Todd Trimble’s questions here. As usual, instead of answers I found more papers to read and no time to read [...]
Todd: After doing some reading, the best I can come up with is maybe.
The big difference seems to be in the handling of equality. The way the effective topos works is by allowing the subobject of a set X corresponding to “x=x” to be smaller than X. Constructive set theories require x=x to be true, a property that I assume separated presheaves satisfy. But they might have some other undesireable property from the point of view of constructive set theory.
Marc: Unfortunately, I don’t have a precise reference. I read a couple of weeks ago that some constructivists objected to the existence of a subobject classifier, that it was “too strong”. It puzzled me at the time, but I think that the objection is that in a purely constructive set theory every set will be constructively given, in that equality and subset membership will be decidable. But not all images of functions have decidable memberships (say the image of Godel numbering of theorems in Peano arithmetic), so constructive set theory would somehow preclude you from defining that set, which rules out the existence of a subobject classifier.
This thread is getting old, but in light of other later threads, I wanted to come back and comment on this concept.
I’ve been reading Goldblatt’s book on Topoi, and he summed up for me what this was all about.
He shows (whether his own work or someone else’s is unclear) that a well-pointed topos is necessarily bivalent.
Well-pointed means that every distinct subobject is distinguishable from all others by at least one member element (arrow from 1 to the subobject.)
Bivalent means that the subobject classifier has only two elements. (necessarily T and ⊥)
Taken together, you have the situation that if your topos is well-pointed, its logical model is necessarily boolean (even if its language is not), since it will be true that for any potential element p of a subobject, it will be true that p ∨ ¬ p, where truth denotes membership, even though this can’t be expressed by the proof system defined by the logical language of the topos.
If, on the contrary, you choose a topos that is not well-pointed, it doesn’t really have the full power of the subobject classifier, since there are some distinct subobjects that can’t be distiguished by it internally within the topos. You would be limited in what you could do with such a topos.
The effective topos seems to be an effort to introduce this partiality formally into the system (a well-pointed non-well-pointedness, in a sense). I plan to read more about this in Bart Jacobs book on Categorical Logic and Type Theory to see if I still think it is really a topos in the normal sense.
Marc, much as I would like to keep the discussion positive and fruitful, and avoid making enemies, the plain truth is that when it comes to topos theory, you don’t know what you’re talking about. Most of it is not even wrong — it’s gibberish.
If someone else would like to interpret and respond to the last three paragraphs in particular, please feel free.
Todd, you’re a bolder man than I, but you’re still right.