Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2011

    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?

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJan 24th 2011

    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.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeJan 24th 2011

    How does it look now?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2011

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

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2011

    Yes, I mean in classical mathematics.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2011

    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 yL,y\forall y\in L, \bot\le y. Thus an element xx is not a bottom element precisely if ¬yL,xy\neg \forall y\in L, x\le y, which with classical logic should be equivalent to yL:¬(xy)\exists y\in L: \neg (x\le y). What is impredicative about that?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2011

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

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2011

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

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2011

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

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2011

    Great, thanks!

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeMar 11th 2012
    • (edited Mar 11th 2012)

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

    • CommentRowNumber12.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeApr 4th 2014
    • (edited Apr 4th 2014)

    I’m having trouble verifying the claim at positive element that in impredicative constructive mathematics, the definition “xLx \in L is positive iff for all subsets AA, xAx \leq \bigvee A implies that AA 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\Set^op is equivalent to the category of complete atomic Heyting algebras, and more generally that for any topos \mathcal{E}, op\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.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeApr 6th 2014

    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.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeApr 6th 2014

    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?

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeApr 7th 2014
    • (edited Apr 7th 2014)

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

  1. 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 aa of a locale LL, he defines Pos(a)Pos(a) as “every cover of aa is inhabited”. He states that this gives a positivity predicate (in the current nLab sense) if and only if LL is overt.

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

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