Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeSep 5th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSo I've finally read all of _[Stack semantics and the comparison of material and structural set theories](http://arxiv.org/abs/1004.3802)_ 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): 1. Every (constructively) well-pointed topos validates collection; 2. Very few toposes, even well-pointed ones, validate separation (are autological). 3. Separation follows from collection and excluded middle. 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?

   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):

   1. Every (constructively) well-pointed topos validates collection;
   2. Very few toposes, even well-pointed ones, validate separation (are autological).
   3. Separation follows from collection and excluded middle.

   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?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 6th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexGood 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: 1. Collection is validated in the stack semantics of every topos, but is not necessarily validated externally in a well-pointed topos. In fact, a well-pointed topos validates collection externally if and only if there is no difference at all between internal and external validity for that topos -- this is Theorem 7.17. 1. Autology is equivalent to internal validity of separation. However, a well-pointed topos can validate separation externally without being autological. For instance, this is the case for a model of Zermelo set theory which is not a model of ZF. In fact, a well-pointed topos is autological if and only if it externally validates both separation and collection -- this is part of Theorem 7.22. 1. Finally, separation does indeed follow from collection and full excluded middle, and this of course works both internally and externally. Thus, 1. If a well-pointed topos satisfies collection and full excluded middle externally, then it satisfies separation externally. 1. If an arbitrary topos satisfies full excluded middle internally (collection being automatic in that case), then it is autological. 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}$.

   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:

   1. Collection is validated in the stack semantics of every topos, but is not necessarily validated externally in a well-pointed topos. In fact, a well-pointed topos validates collection externally if and only if there is no difference at all between internal and external validity for that topos – this is Theorem 7.17.
   2. Autology is equivalent to internal validity of separation. However, a well-pointed topos can validate separation externally without being autological. For instance, this is the case for a model of Zermelo set theory which is not a model of ZF. In fact, a well-pointed topos is autological if and only if it externally validates both separation and collection – this is part of Theorem 7.22.
   3. Finally, separation does indeed follow from collection and full excluded middle, and this of course works both internally and externally. Thus,
      1. If a well-pointed topos satisfies collection and full excluded middle externally, then it satisfies separation externally.
      2. If an arbitrary topos satisfies full excluded middle internally (collection being automatic in that case), then it is autological.

   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}$.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeSep 6th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorZhen Lin
   • CommentTimeSep 7th 2011
   • (edited Sep 7th 2011)
   • PermaLink
   Author: Zhen Lin
   Format: Markdown@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?

   @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?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 7th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex@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.

   @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.