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 be a preordered set, and let be an element of .
An element is positive if it is not a bottom element, equivalently if there exists an element such that is false: .
A positivity predicate on is a predicate , pronounced “ is positive”, such that
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.
Every power set has a positivity predicate: is positive iff 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.
Although classically trivial, a key property of positivity in the constructive context is this:
where is the set of positive elements of .