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 23 of 23
At fully formal ETCS there is the comment that the theory of a topos with NNO can be written as an essentially algebraic theory, and so there are models in any finitely complete category. I was thinking about this recently before I came across this comment, and I was thinking that we would need cartesian closedness as well, so this is a pleasant surprise. (Aside: I should write down the relevant sketch…)
However, I was wondering if it was possible to consider the internal logic (or the stack semantics) of the canonical internal topos with nno in the finite limit theory of such and recover well-pointedness. This would be, for me at least, a remarkable result. Is this a reasonable thing to expect? Or am I trying to fly by picking myself up?
Please don’t edit the ETCS article, because I am currently working on it! I plan to make good on that claim about essential algebraicity.
Don’t worry, I won’t edit it. I just had a look because I saw it was being updated :) Just a quick remark. Near the top you say that AC belongs to coherent logic, and near the bottom it says AC belongs to geometric logic. I guess the former is correct.
Thanks, yes.
Much of the rewriting is being done in remembrance of a fairly scathing assessment of the “fully formal” article by Emil Jerabek at MO, who correctly pointed out an omission and a mistake (both easily fixed), but there was a more general critique (that felt to me more like an attack) which definitely called for a response that was essentially impossible to flesh out in those damned comment boxes – too much stuff to explain, and I was too pissed off to even want to explain for his benefit. (I could look up the link, but I don’t much feel like doing so, even months after the fact.) The article at present is in a messy state because there have been a number of edits in the meantime none of which were carried to completion – I really need to go through the whole thing properly now.
I have added some more hyperlinks to the first two introductory paragraphs. For instance I hyperlinked the term first-order theory, etc. The entry first-order theory had been minimal. I have now expanded it ever so slightly. But it’s still minimal.
Todd, I found that thread with Emil, and it seems to have come to life again earlier this month. I actually agree with Emil about nontriviality. I wrote a comment on MO that I copy here:
I agree with Emil; nontriviality should be part of the definition of ETCS. It goes along with well-pointedness. It is true, of course, that “there is no rational square root of two” is true in the internal logic of the trivial topos, but if we were interested in founding mathematics on what can be proved in the internal logic of every suitable topos, then we wouldn’t have well-pointedness either. The point of being well-pointed is to make the internal logic line up with the external logic, and this requires nontriviality too.
See also well-pointed topos.
Interesting point, Toby! I wasn’t actually aware of the nondegeneracy requirement on at well-pointed topos; is that standard? But anyway, your point makes sense.
Edit: I looked in Mac Lane-Moerdijk, and in Lawvere’s article, but a quick glance tells me that neither source includes the nondegeneracy requirement. Is there a source besides the nLab that has this requirement?
@Urs #5: okay, I was able to reproduce your edits in the editing window I had open, but I would like to ask everyone reading this please not to introduce more edits for at least today or so; it’s just going to screw things up for me. I’ll drop another note when I’m done for the time being.
Sorry, Todd, I didn’t understand that you wanted strictly no edits. I thoiught you just didn’t want substantial edits.
So I guess you are editing the source separately, not in the nLab edit window. Okay, sorry.
@Todd #7: I always thought that nontriviality was standard for well-pointedness, but it's the sort of thing that people can easily leave out when they really assume (or sometimes put in when they really don't need it). In Lawvere's article, it follows from Axiom 8. I'm pretty sure that is stated explicitly as an axiom in Lawvere & Rosebrugh (which is where I learnt ).
Oh, there it is – thanks very much, Toby!
My copy of Mac Lane and Moerdijk says on p275
to exclude the trivial example for which is the category with only one object and one arrow, we will always assume that a well-pointed topos is also nondegenerate, i.e., .
I think nondegeneracy as part of well-pointedness makes more sense when you think about the constructive version of well-pointedness, in which you have to also assume indecomposability and projectivity of 1 explicitly. It’s sort of an accident that those two properties follow in classical logic from 1 being a generator. Just as nondegeneracy is about falsehood, indecomposability is about disjunction and projectivity is about existential quantification.
As for David’s original question in #1, I don’t understand what you are asking. Can you elaborate?
Maybe to address #1, note that every category is internally well-pointed.
@Toby - that’s right. I was wondering if starting from a topos with nno, we can somehow bootstrap in well-pointedness, by considering the internal logic of the canonical internal topos one gets from the essentially algebraic theory.
I’m afraid I still don’t understand. The essentially algebraic theory gives you the “free finitely-complete-category containing an internal well-pointed topos object”. What do you then want to do with that? Where does your starting topos with nno come into the picture?
Where does your starting topos with nno come into the picture?
Whoops, that’s not what I meant. I meant starting from the topos in the free finitely-complete-category containing an internal well-pointed topos-with-nno object.
And I was wondering (just now, not before) if this is something like the analogue of a countable model of ZFC, if we assume the existence of an ambient set theory. I mean this in only a very loose way.
Okay, starting from there, now you want to do what?
Well, I’m not sure I really want to do anything in particular, I just find it amazing that one can write down a finite limit sketch, and then from this arises everything one can do in Choice-free, ordinary mathematics. You may wonder why this sort of amazement doesn’t arise when confronted with the finite axiomatisation of ETCS, or the fewer-symbols-but-not-actually-finite axiomatisation of ZF(C). Well, I suppose it’s that topos theory is so rich, and that finite limit sketches are so down-to-earth and concrete, but when written in the patois of traditional logicians, it all looks very much more complex, especially ZF(C) (or, to be fair BZ(C) as this is the directly comparable theory).
Anyway, I probably shouldn’t have left out an opening disclaimer of ’This is just idle thoughts…’ in my original post. :-)
the finite axiomatisation of ETCS, or the fewer-symbols-but-not-actually-finite axiomatisation of ZF(C)
Since the axiomatisation of the latter is recursively enumerable, it has a conservative extension whose axiomatisation is finite; the usual example is BNG.
@Todd #7: Definition 9.34 of Johnstone’s Topos Theory includes nondegeneracy in the definition of well-pointedness. It defines a topos to be well-pointed if 1 is a generator and is not iso.
Tom: I accept that this is the standard definition. Thanks.
You’re welcome. I just happened to be reading that page of Topos Theory, remembered this thread, and thought I might as well add it as a data point, in case anyone was keeping track.
1 to 23 of 23