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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum 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 sheaves 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.
   • CommentAuthorUrs
   • CommentTimeNov 5th 2011
   • (edited Nov 5th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have split off [[universal quantifier]] and [[existential quantifier]] from [[quantifier]] in order to expose the idea in a more pronounced way in dedicated entries. Mainly I wanted to further amplify the idea of how these notions are modeled by adjunctions, and how, when formulated suitably, the whole concept immediately and seamlessly generalizes to [[(infinity,1)-logic]]. But I am not a logic expert. Please check if I got all the terminology right, etc. Also, there is clearly much more room for expanding the discussion.

   I have split off universal quantifier and existential quantifier from quantifier in order to expose the idea in a more pronounced way in dedicated entries.

   Mainly I wanted to further amplify the idea of how these notions are modeled by adjunctions, and how, when formulated suitably, the whole concept immediately and seamlessly generalizes to (infinity,1)-logic.

   But I am not a logic expert. Please check if I got all the terminology right, etc. Also, there is clearly much more room for expanding the discussion.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeNov 5th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI added some comments about the difference between the two situations ($\Pi$ preserves (-1)-truncated objects, whereas $\Sigma$ does not). I'm not entirely happy with the Idea sections; they seem kind of circular. "$\forall$ is... used to express... the proposition $\forall x\colon X, \phi x$". Not sure what to say instead, though.

   I added some comments about the difference between the two situations ($\Pi$ preserves (-1)-truncated objects, whereas $\Sigma$ does not).

   I’m not entirely happy with the Idea sections; they seem kind of circular. “$\forall$ is… used to express… the proposition $\forall x\colon X, \phi x$”. Not sure what to say instead, though.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeNov 6th 2011
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI didn't really like the notation $\exists$ and $\forall$ for the left and right adjoints to the pullback functor $X \times -: E \to E/X$ (which I would prefer to denote by $X^\ast: E \to E/X$, reserving $X \times -$ for the evident functor $E \to E$). I would prefer to denote these by the traditional notation $\Sigma_X: E/X \to E$ and $\Pi_X: E/X \to E$. I'll be happy to make changes, if there is no objection.

   I didn’t really like the notation $\exists$ and $\forall$ for the left and right adjoints to the pullback functor $X \times -: E \to E/X$ (which I would prefer to denote by $X^\ast: E \to E/X$, reserving $X \times -$ for the evident functor $E \to E$). I would prefer to denote these by the traditional notation $\Sigma_X: E/X \to E$ and $\Pi_X: E/X \to E$. I’ll be happy to make changes, if there is no objection.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeNov 7th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexTodd: please; I would like that too. I'd prefer to reserve $\exists$ and $\forall$ for the action on (-1)-truncated objects.

   Todd: please; I would like that too. I’d prefer to reserve $\exists$ and $\forall$ for the action on (-1)-truncated objects.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeNov 7th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexDid you take material out of [[quantification]] or just the cache-bug infested version that you linked to?

   Did you take material out of quantification or just the cache-bug infested version that you linked to?

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeNov 7th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexAll this talk of ‘term’s in the Idea sections is worse than circular; it's downright wrong. So I took language from [[quantification]] and fixed it.

   All this talk of ‘term’s in the Idea sections is worse than circular; it’s downright wrong. So I took language from quantification and fixed it.

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeNov 7th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexAlso, the restriction to toposes seems needlessly specific, so I broadened things considerably.

   Also, the restriction to toposes seems needlessly specific, so I broadened things considerably.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeNov 7th 2011
   • PermaLink
   Author: Urs
   Format: MarkdownItex> Did you take material out of quantification or just the cache-bug infested version that you linked to? I didn't take any material out anywhere! > this talk of ‘term’s in the Idea sections is worse than circular; it's downright wrong. So I took language from quantification and fixed it. Er, thanks. Do you consider what is currently in the "Defnition"-section a self-contained definition? I may be missing something, but currently it looks like before any definition was given it says "we need to define it more carefully". More carefully than what? Also, it would be nice to have an explanation of how that distinction between the more and the less careful version relates to the following section "In topos theory".

   Did you take material out of quantification or just the cache-bug infested version that you linked to?

   I didn’t take any material out anywhere!

   this talk of ‘term’s in the Idea sections is worse than circular; it’s downright wrong. So I took language from quantification and fixed it.

   Er, thanks. Do you consider what is currently in the “Defnition”-section a self-contained definition? I may be missing something, but currently it looks like before any definition was given it says “we need to define it more carefully”. More carefully than what?

   Also, it would be nice to have an explanation of how that distinction between the more and the less careful version relates to the following section “In topos theory”.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeNov 7th 2011
   • (edited Nov 7th 2011)
   • PermaLink
   Author: Urs
   Format: MarkdownItexTo make the notation clearer, I have relabeled and extended the diagram to look as follows $$ \array{ \mathcal{E}/X & \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} & \mathcal{E} \\ {}^{\mathllap{\tau_{\leq_{-1}}}}\downarrow \uparrow && {}^{\mathllap{\tau_{\leq_{-1}}}}\downarrow \uparrow \\ \tau_{\leq_{-1}} \mathcal{E}/X & \stackrel{\overset{\exists}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{\forall}{\to}}} & \tau_{\leq_{-1}} \mathcal{E} } \,. $$

   To make the notation clearer, I have relabeled and extended the diagram to look as follows

   $$\array{ \mathcal{E}/X & \stackrel{\overset{X_!}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}}} & \mathcal{E} \\ {}^{\mathllap{\tau_{\leq_{-1}}}}\downarrow \uparrow && {}^{\mathllap{\tau_{\leq_{-1}}}}\downarrow \uparrow \\ \tau_{\leq_{-1}} \mathcal{E}/X & \stackrel{\overset{\exists}{\to}}{\stackrel{\overset{X^*}{\leftarrow}}{\underset{\forall}{\to}}} & \tau_{\leq_{-1}} \mathcal{E} } \,.$$
10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 7th 2011
    • (edited Nov 7th 2011)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexPresumably on [[universal quantifier]] the line beginning >where $(-) \times X$ is the functor... needs to be changed to talk about the arrows in the diagram above it.

    Presumably on universal quantifier the line beginning

    where $(-) \times X$ is the functor…

    needs to be changed to talk about the arrows in the diagram above it.

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>I didn't take any material out anywhere! I meant where did it come from, not where was it removed from. But it doesn't make any difference, as I see that you really didn't copy anything. I was just worried that you'd used an old cache-bug copy as a source for something instead of a current version!

    I didn’t take any material out anywhere!

    I meant where did it come from, not where was it removed from. But it doesn’t make any difference, as I see that you really didn’t copy anything. I was just worried that you’d used an old cache-bug copy as a source for something instead of a current version!

12. • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>More carefully than what? More carefully than what's in the Idea section. And yes, in the context of ordinary logic (where we care only about whether an entailment is valid, not any higher homotopy types), that is a complete definition. (If you prefer, it's an axiomatisation, a definition of what *a* universal/particular quantification is rather than what *the* universal/particular quantification is, although uniqueness follows.)

    More carefully than what?

    More carefully than what’s in the Idea section.

    And yes, in the context of ordinary logic (where we care only about whether an entailment is valid, not any higher homotopy types), that is a complete definition. (If you prefer, it’s an axiomatisation, a definition of what a universal/particular quantification is rather than what the universal/particular quantification is, although uniqueness follows.)

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItex> More carefully than what's in the Idea section. That's not really becoming clear. I would prefer if the Definition-section starts with stating a definition. It seems to me that generally it is true that a Definition needs to involve more care than the corresponding idea.

    More carefully than what’s in the Idea section.

    That’s not really becoming clear. I would prefer if the Definition-section starts with stating a definition. It seems to me that generally it is true that a Definition needs to involve more care than the corresponding idea.

14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: Todd_Trimble
    Format: TextI have added some words to [[universal quantification]] which hopefully incorporate the discussion above and ease the transition between sections.

    I have added some words to universal quantification which hopefully incorporate the discussion above and ease the transition between sections.
15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat about phrasing the definition in terms of a [[hyperdoctrine]]? That seems to me like it incorporates both definitions currently on the page -- the first is talking about the hyperdoctrine of formulas over contexts with provability, and the second about the hyperdoctrine of subobjects over objects of a category (most generally, a [[Heyting category]] for $\forall$ and a [[regular category]] for $\exists$) with inclusion.

    What about phrasing the definition in terms of a hyperdoctrine? That seems to me like it incorporates both definitions currently on the page – the first is talking about the hyperdoctrine of formulas over contexts with provability, and the second about the hyperdoctrine of subobjects over objects of a category (most generally, a Heyting category for $\forall$ and a regular category for $\exists$) with inclusion.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHmm, I think the page [[hyperdoctrine]] needs a little love.

    Hmm, I think the page hyperdoctrine needs a little love.

17. • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 7th 2011
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYes, that and the page [[first-order hyperdoctrine]]. But I should really be doing something else right now besides math.

    Yes, that and the page first-order hyperdoctrine. But I should really be doing something else right now besides math.

18. • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeNov 7th 2011
    • (edited Nov 7th 2011)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Urs Does it make sense now? If so, then I will edit [[existential quantifier]] as well.

    @ Urs

    Does it make sense now?

    If so, then I will edit existential quantifier as well.

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Does it make sense now? Now it's very nice, yes. Thanks!

    Does it make sense now?

    Now it’s very nice, yes. Thanks!

20. • CommentRowNumber20.
    • CommentAuthorTobyBartels
    • CommentTimeNov 10th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexGreat, now both articles are like that.

    Great, now both articles are like that.

21. • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 10th 2011
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexMade changes to [[existential quantifier]] to make it more like its universal partner.

    Made changes to existential quantifier to make it more like its universal partner.