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 be a preordered set, and let be an element of .
(in classical mathematics, and in predicative mathematics with classical logic)
An element is positive if it is not a bottom element, equivalently if there exists an element such that is false: .
(in classical mathematics, and in impredicative constructive mathematics)
An element is positive if whenever is bounded above by a join of some subset of , is inhabited: .
(in predicative constructive mathematics)
A positivity predicate on is a predicate , pronounced “ is positive”, such that
If is bounded above by a join of a subset and is positive, then some element of that subset is positive: .
If is bounded above by a join on the assumption that is positive, then really is so bounded: .
These definitions are equivalent under certain circumstances. Specifically:
In predicative mathematics with classical logic, one can prove that every preorder has a unique positivity predicate, which must match Definition .
In impredicative constructive mathematics, one can prove that if a preorder admits a positivity predicate, then it is given by Definition . However, in general, the predicate defined in Definition is not a positivity predicate in the sense of Definition .
In classical mathematics (with classical logic and impredicativity), all of the definitions are equivalent.
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.
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 , it holds that (that is, ). The remaining properties can then be easily verified. By assumption, for some set containing only positive elements. For any , it holds that , thus that is positive and thus that . Therefore holds as well. The other inequality is trivial.
Every atom of 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:
where is the set of positive elements of .
A special case is
for any element .
Last revised on January 13, 2017 at 19:46:34. See the history of this page for a list of all contributions to it.