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.
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?
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.
How does it look now?
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”?
Yes, I mean in classical mathematics.
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?
By the way, there is also a discussion of predicativity at the Cafe at the moment.
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.)
I’ve just edited the page to destroy the numbering in my previous comment. Hopefully now it is perfectly clear.
Great, thanks!
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.
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.
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.
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?
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).
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.
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.
1 to 17 of 17