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.
So I’ve finally read all of Stack semantics and the comparison of material and structural set theories and I find that I have a confusion.
From this paper, I get the first two of a set of three facts (the last of which is well known, and I even wrote a proof of it on Wikipedia years ago that hasn’t been significantly edited yet):
If you had a theorem that every well-pointed topos with full classical logic was autological, then you would have said so; and in any case, there must be plenty of models of $ETCS$ (hence well-pointed toposes with full classical logic) that aren’t, since $ETCS$ doesn’t validate separation. But with the 3 facts above, this seems to lead to a contradiction.
What am I missing?
Good question! First of all, we need to remember the difference between internally and externally validating a principle. All the principles of structural set theory used in the paper are statements about a category, so they can be asserted externally about a topos as a category (in which case, we usually also require the topos to be well-pointed) – but they can also be asserted internally (in the stack semantics) to an arbitrary, not necessarily well-pointed topos. Now we have the following facts:
I think this last statement is the theorem you thought I would have said if I had had it. I know it was in an earlier draft of the paper, but right now I can’t find it in the current version (which ended up kind of poorly edited and organized, somehow). I’ll make sure to put it back in when I revise it (something which has been on the to-do list for a while, but which I now might actually get to within a few months).
So why is this not a contradiction? The point is that unlike the situation for $\Delta_0$-classical logic (and also the axiom of choice), external full classical logic does not imply internal full classical logic. (For the benefit of bystanders: “full” classical logic means we assert excluded middle for all statements; $\Delta_0$-classical logic asserts excluded middle only for statements containing only bounded quantifiers.) In particular, a model of ETCS which does not validate both separation and collection externally cannot be autological, and therefore it cannot satisfy full classical logic internally – even though any model of ETCS satisfies full classical logic externally (by definition, since ETCS denotes a theory phrased in classical first-order logic).
It’s a nice exercise to find an explicit statement P such that “P or not P” cannot be asserted in the stack semantics of $V_{\omega\cdot 2}$.
I put well pointedness in there so that there’d be no difference between internal and external, but that didn’t work.
Somehow I got the impression that a well-pointed topos has full classical logic if we accept classical logic in the metatheory, which seems to be a symptom of the same problem.
I will now set myself that exercise.
@Mike: But isn't it true that a (classically) well-pointed topos, such as a model of ETCS, is a two-valued Boolean topos, and therefore validate the law of excluded middle (in the usual topos semantics) already? This is Proposition VI.2.7 in Sheaves in Geometry and Logic, for example. Assuming that this is correct, I'd guess that the point is that stack semantics interpret more formulae than topos semantics and that there is some formula with unbounded quantifiers which witnesses the failure of the law of excluded middle in stack semantics. Is that right?
@Zhen: Yes, exactly; that’s the difference between what I was calling “$\Delta_0$-classical logic” and “full classical logic”. (Two-valuedness is irrelevant, by the way – Booleanness is what makes the internal logic $\Delta_0$-classical.) The stack semantics is a proper extension of the usual internal logic; it interprets all the same formulas with the same meanings, but also interprets more formulas (those with unbounded quantifiers). So the answer to the exercise I mentioned above must involve at least one unbounded quantifer.
1 to 5 of 5