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 definitions 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 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.
   • CommentAuthorMike Shulman
   • CommentTimeJan 24th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThis is presumably directed at Toby. I am confused about [[positive element]]. First it says "There are two definitions, one of which is useful predicatively but not constructively, and one of which is useful constructively but not predicatively," and gives two definitions, but without any explicit indication of which is which. Then in the next section, it proceeds to say that positivity *cannot* be defined predicatively, but must be given axiomatically, which seems to contradict the assertion in the previous section that there is a definition which is "useful predicatively but not constructively." And I'm not sure what that last phrase means, either; isn't constructive usually a superset of predicative?

   This is presumably directed at Toby.

   I am confused about positive element. First it says “There are two definitions, one of which is useful predicatively but not constructively, and one of which is useful constructively but not predicatively,” and gives two definitions, but without any explicit indication of which is which. Then in the next section, it proceeds to say that positivity cannot be defined predicatively, but must be given axiomatically, which seems to contradict the assertion in the previous section that there is a definition which is “useful predicatively but not constructively.” And I’m not sure what that last phrase means, either; isn’t constructive usually a superset of predicative?

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeJan 24th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI'll start with your last clause: >isn't constructive usually a superset of predicative? This is false. Much if not most of the work in [[predicative mathematics]] uses *classical* logic, even though most of the explicitly predicative material on the nLab (which has been written primarily by me) is constructive. >without any explicit indication of which is which The order is the same as in the previous sentence. But I'll clarify that. >it proceeds to say that positivity *cannot* be defined predicatively No, it doesn't say that. It says that there's no predicative definition *that matches the constructive definition*. But that can also be clarified.

   I’ll start with your last clause:

   isn’t constructive usually a superset of predicative?

   This is false. Much if not most of the work in predicative mathematics uses classical logic, even though most of the explicitly predicative material on the nLab (which has been written primarily by me) is constructive.

   without any explicit indication of which is which

   The order is the same as in the previous sentence. But I’ll clarify that.

   it proceeds to say that positivity cannot be defined predicatively

   No, it doesn’t say that. It says that there’s no predicative definition that matches the constructive definition. But that can also be clarified.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeJan 24th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexHow does it look now?

   How does it look now?

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJan 24th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOkay, now I think I understand, but I may try reorganizing the entry a bit more. So when you say "classically, these two definitions are equivalent" you mean not just "with classical logic" but "with classical logic and impredicative definitions"?

   Okay, now I think I understand, but I may try reorganizing the entry a bit more. So when you say “classically, these two definitions are equivalent” you mean not just “with classical logic” but “with classical logic and impredicative definitions”?

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeJan 25th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYes, I mean in [[classical mathematics]].

   Yes, I mean in classical mathematics.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOkay, I have reorganized [[positive element]] in a way which makes the relationship of all the definitions clearer to me. Feel free to object. There must be something I don't understand about predicative mathematics with classical logic. A bottom element of L is, by definition, an element $\bot$ such that $\forall y\in L, \bot\le y$. Thus an element $x$ is *not* a bottom element precisely if $\neg \forall y\in L, x\le y$, which with classical logic should be equivalent to $\exists y\in L: \neg (x\le y)$. What is impredicative about that?

   Okay, I have reorganized positive element in a way which makes the relationship of all the definitions clearer to me. Feel free to object.

   There must be something I don’t understand about predicative mathematics with classical logic. A bottom element of L is, by definition, an element $\bot$ such that $\forall y\in L, \bot\le y$. Thus an element $x$ is not a bottom element precisely if $\neg \forall y\in L, x\le y$, which with classical logic should be equivalent to $\exists y\in L: \neg (x\le y)$. What is impredicative about that?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexBy the way, there is also a discussion of predicativity at the [Cafe](http://golem.ph.utexas.edu/category/2011/01/topos_theory_can_make_you_a_pr.html) at the moment.

   By the way, there is also a discussion of predicativity at the Cafe at the moment.

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeJan 25th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>What is impredicative about that? Nothing at all! That is precisely the predicative-but-not-constructive definition that I gave. (It's constructively meaningful too, just not what we want.) If you mean, why distinguish Definitions 1 & 2, I would say, don't. I gave Definition 2 instead of 1 because, naïvely, a constructivist might think that Definition 2 is good enough (I did once, per the history of [[proper subset]]), whereas Definition 1 is obviously not right; but Definition 2 is still not good enough constructively (at least for locale theory). It's certainly not right to single out Definition 1 as the ‘classical’ definition. They are *all* valid classically! (Definition 4 is also valid in both impredicative constructive mathematics and in nonconstructive predicative mathematics, although it's rather overkill in those cases.)

   What is impredicative about that?

   Nothing at all! That is precisely the predicative-but-not-constructive definition that I gave. (It’s constructively meaningful too, just not what we want.)

   If you mean, why distinguish Definitions 1 & 2, I would say, don’t. I gave Definition 2 instead of 1 because, naïvely, a constructivist might think that Definition 2 is good enough (I did once, per the history of proper subset), whereas Definition 1 is obviously not right; but Definition 2 is still not good enough constructively (at least for locale theory).

   It’s certainly not right to single out Definition 1 as the ‘classical’ definition. They are all valid classically! (Definition 4 is also valid in both impredicative constructive mathematics and in nonconstructive predicative mathematics, although it’s rather overkill in those cases.)

9. • CommentRowNumber9.
   • CommentAuthorTobyBartels
   • CommentTimeJan 25th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI've just edited the page to destroy the numbering in my previous comment. Hopefully now it is perfectly clear.

   I’ve just edited the page to destroy the numbering in my previous comment. Hopefully now it is perfectly clear.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGreat, thanks!

    Great, thanks!

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeMar 11th 2012
    • (edited Mar 11th 2012)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexThe recent dicussion of atoms has made me look at [[positive elements|this page]] enough to notice that it was wrong; wherever I had $x = \bigvee A$, it should be $x \leq \bigvee A$. Now I've fixed it.

    The recent dicussion of atoms has made me look at this page enough to notice that it was wrong; wherever I had $x = \bigvee A$, it should be $x \leq \bigvee A$. Now I’ve fixed it.

12. • CommentRowNumber12.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeApr 4th 2014
    • (edited Apr 4th 2014)
    • PermaLink
    Author: IngoBlechschmidt
    Format: MarkdownItexI'm having trouble verifying the claim at _[[positive element]]_ that in impredicative constructive mathematics, the definition "$x \in L$ is positive iff for all subsets $A$, $x \leq \bigvee A$ implies that $A$ is inhabited" actually yields a positivity predicate. I can prove this under the extra assumption that any element is a join of [[atom|atoms]]; that's good because that means we still have that in a complete atomic Heyting algebra, any atom is tiny (see and constructify the proof at _[[atom]]_). This is used in the proof that $\Set^op$ is equivalent to the category of complete atomic Heyting algebras, and more generally that for any topos $\mathcal{E}$, $\mathcal{E}^op$ is equivalent to the category of internal complete atomic Heyting algebras in $\mathcal{E}$. (This is relevant to a [recent question at Math.SE](http://math.stackexchange.com/questions/736852/toposes-and-stone-type-dualities).) Please correct me if I'm wrong. Otherwise, I'll add an appropriate remark, fill in some details, and rework the proof at _[[atom]]_ to be impredicatively constructively acceptable.

    I’m having trouble verifying the claim at positive element that in impredicative constructive mathematics, the definition “$x \in L$ is positive iff for all subsets $A$, $x \leq \bigvee A$ implies that $A$ is inhabited” actually yields a positivity predicate.

    I can prove this under the extra assumption that any element is a join of atoms; that’s good because that means we still have that in a complete atomic Heyting algebra, any atom is tiny (see and constructify the proof at atom). This is used in the proof that $\Set^op$ is equivalent to the category of complete atomic Heyting algebras, and more generally that for any topos $\mathcal{E}$, $\mathcal{E}^op$ is equivalent to the category of internal complete atomic Heyting algebras in $\mathcal{E}$. (This is relevant to a recent question at Math.SE.)

    Please correct me if I’m wrong. Otherwise, I’ll add an appropriate remark, fill in some details, and rework the proof at atom to be impredicatively constructively acceptable.

13. • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeApr 6th 2014
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexYou\'re probably right. This has been bugging me for a while; I had convinced myself of this claim once, but later I couldn\'t reconstruct the argument, but neither could I find a counterexample. I always mean to settle it one way or another and then fix the page (either correcting it or writing out the argument). You should feel free to make whatever remarks you find appropriate.

    You're probably right. This has been bugging me for a while; I had convinced myself of this claim once, but later I couldn't reconstruct the argument, but neither could I find a counterexample. I always mean to settle it one way or another and then fix the page (either correcting it or writing out the argument).

    You should feel free to make whatever remarks you find appropriate.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeApr 6th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIf this is the case, then my inclination would be to regard the predicative definition of "positivity predicate" as in error. Surely *the* positivity predicate that exists impredicatively ought to be *a* positivity predicate?

    If this is the case, then my inclination would be to regard the predicative definition of “positivity predicate” as in error. Surely the positivity predicate that exists impredicatively ought to be a positivity predicate?

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeApr 7th 2014
    • (edited Apr 7th 2014)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexYes; but at the same time, the additional properties required in (what the page claimed to be) the most general definition are important properties. I believe that they are related to overtness. So one can speak generally of a positivity predicate and more specifically of an overt positivity (which may or may not be identical to what is already on the page).

    Yes; but at the same time, the additional properties required in (what the page claimed to be) the most general definition are important properties. I believe that they are related to overtness. So one can speak generally of a positivity predicate and more specifically of an overt positivity (which may or may not be identical to what is already on the page).

16. • CommentRowNumber16.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeApr 7th 2014
    • PermaLink
    Author: IngoBlechschmidt
    Format: MarkdownItexThank you for the comments! I will add some things to the articles today or tomorrow. Re 15: A nice review is in [an article from Bas Spitters](http://arxiv.org/abs/math/0703561), page 11, although in the context of frames and locales instead of general posets. For an open $a$ of a locale $L$, he defines $Pos(a)$ as "every cover of $a$ is inhabited". He states that this gives a positivity predicate (in the current nLab sense) if and only if $L$ is overt. See also some [slides of Thierry Coquand](http://www.cse.chalmers.se/~coquand/pos.pdf), which are in the context of formal topology. Positivity is discussed on slides 13ff.

    Thank you for the comments! I will add some things to the articles today or tomorrow.

    Re 15: A nice review is in an article from Bas Spitters, page 11, although in the context of frames and locales instead of general posets. For an open $a$ of a locale $L$, he defines $Pos(a)$ as “every cover of $a$ is inhabited”. He states that this gives a positivity predicate (in the current nLab sense) if and only if $L$ is overt.

    See also some slides of Thierry Coquand, which are in the context of formal topology. Positivity is discussed on slides 13ff.

17. • CommentRowNumber17.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeApr 11th 2014
    • PermaLink
    Author: IngoBlechschmidt
    Format: MarkdownItexReformulated the proof at _[[atom]]_ that any atom is tiny to be impredicatively constructively acceptable. Added to _[[positive element]]_ a remark about the failure of the canonical notion of positivity to be a positivity predicate and a proof that it does work if any element is a join of positive elements.

    Reformulated the proof at atom that any atom is tiny to be impredicatively constructively acceptable. Added to positive element a remark about the failure of the canonical notion of positivity to be a positivity predicate and a proof that it does work if any element is a join of positive elements.