# Positive elements

## Idea

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.

## Definitions

Let $L$ be a preordered set, and let $x$ be an element of $L$.

###### Definition

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

An element $x\in L$ is positive if it is not a bottom element, equivalently if there exists an element $y\in L$ such that $x\le y$ is false: $¬\left(x\le \bigvee \varnothing \right)$.

###### Definition

(in classical mathematics, and in impredicative constructive mathematics)

An element $x\in L$ is positive if whenever $x$ is bounded above by a join of some subset $A$ of $L$, $A$ is inhabited: $\forall A\phantom{\rule{thinmathspace}{0ex}};x\le \bigvee A\phantom{\rule{thickmathspace}{0ex}}⇒\phantom{\rule{thickmathspace}{0ex}}\exists \phantom{\rule{thinmathspace}{0ex}}u\in A$.

###### Definition

(in predicative constructive mathematics)

A positivity predicate on $L$ is a predicate $\diamond x$, pronounced “$x$ is positive”, such that

• If $x$ is bounded above by a join of a subset and $x$ is positive, then some element of that subset is positive: $\diamond x\phantom{\rule{thickmathspace}{0ex}}\wedge \phantom{\rule{thickmathspace}{0ex}}x\le \bigvee A\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}\exists \phantom{\rule{thinmathspace}{0ex}}u\in A,\phantom{\rule{thickmathspace}{0ex}}\diamond u$.
• If $x$ is bounded above by a join on the assumption that $x$ is positive, then $x$ really is so bounded: $\diamond x\phantom{\rule{thickmathspace}{0ex}}⇒\phantom{\rule{thickmathspace}{0ex}}x\le \bigvee A\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}x\le \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 every preorder has a unique positivity predicate, which must match Definition 2.

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

## Examples

Every power set has a positivity predicate: $x$ is positive iff $x$ 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.

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

## Properties

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

$\bigvee A=\bigvee {A}^{+},$\bigvee A = \bigvee A^+ ,

where ${A}^{+}$ is the set of positive elements of $A$.

Revised on March 11, 2012 19:12:09 by Toby Bartels (75.88.85.16)