positive element

Positive elements


In classical mathematics, an element of a poset is positive if and only if it not a bottom element.

A more subtle definition is needed in constructive mathematics; analogously to how “nonempty sets” may need to be replaced by inhabited sets. In mathematics that is both constructive and predicative, positivity can be axiomatised but not defined.


Let LL be a preordered set, and let xx be an element of LL.


(in classical mathematics, and in predicative mathematics with classical logic)

An element xLx \in L is positive if it is not a bottom element, equivalently if there exists an element yLy \in L such that xyx \leq y is false: ¬(x)\neg(x \leq \bigvee \empty).


(in classical mathematics, and in impredicative constructive mathematics)

An element xLx \in L is positive if whenever xx is bounded above by a join of some subset AA of LL, AA is inhabited: A;xAuA\forall A\,; x \leq \bigvee A \;\Rightarrow\; \exists\, u \in A.


(in predicative constructive mathematics)

A positivity predicate on LL is a predicate x\lozenge x, pronounced “xx is positive”, such that

  • If xx is bounded above by a join of a subset and xx is positive, then some element of that subset is positive: xxAuA,u\lozenge x \;\wedge\; x \leq \bigvee A \;\vdash\; \exists\, u \in A,\; \lozenge u.

  • If xx is bounded above by a join on the assumption that xx is positive, then xx really is so bounded: xxAxA\lozenge x \;\Rightarrow\; x \leq \bigvee A \;\vdash\; x \leq \bigvee A.

Any two of these definitions can be shown to be equivalent in the union of the corresponding foundational systems. Specifically:

  • In predicative mathematics with classical logic, one can prove that every preorder has a unique positivity predicate, which must match Definition 1.

  • In impredicative constructive mathematics, one can prove that if a preorder admits a positivity predicate, it is given by Definition 2. However, in general Definition 2 gives not rise to a positivity predicate in the sense of Definition 3.

  • In classical mathematics (with classical logic and impredicativity), all of the definitions are equivalent.


Every power set has a positivity predicate: xx is positive iff xx is inhabited. (Of course, there are few power sets in predicative mathematics, but often it is enough to think of the power set as a proper class.)

The positive predicate on a locale plays a role in the definition of an overt space. Locale theory is often considered constructively but impredicatively; in predicative constructive mathematics, a positivity predicate is used in the corresponding theory of formal topology.

In impredicative constructive mathematics, a sufficient condition for a complete poset to possess a positivity predicate is that any element is a join of positive elements. To show this, it suffices to prove that for any element aa, it holds that a={a|apositive}a = \bigvee \{ a | a \, positive \}. The remaining properties can then be easily verified. By assumption, a=supBa = \sup B for some set BB containing only positive elements. For any bBb \in B, it holds that bab \leq a, thus that aa is positive and thus that b{a|apositive}b \leq \bigvee \{ a | a \, positive \}. Therefore supB{a|apositive}\sup B \leq \bigvee \{ a | a \, positive \} holds as well. The other inequality is trivial.

Every atom of LL is positive, and indeed an atom is precisely a minimal positive element.


Although classically trivial, a key property of positivity in the constructive context is this:

A=A +, \bigvee A = \bigvee A^+ ,

where A +A^+ is the set of positive elements of AA.

A similar property is

a={a|apositive} a = \bigvee \{ a | a \, positive \}

for any element aa.

Revised on November 6, 2016 13:50:12 by Anonymous Coward (