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 of is positive if whenever is the join of some subset of in , is inhabited (and so all of ): .
It follows that any arbitrary subset of is inhabited if is the join of . (This is because if , then .) But it's important that the definition only quantifies over truth values, which is why this definition is classically predicative, and may even be acceptable to some constructive predicativists who don't accept function sets.
(in predicative constructive mathematics)
A positivity predicate on is a predicate , pronounced “ is positive”, such that
If is the join of a subset and is positive, then some element of that subset is positive: .
If equals a join on the assumption that is positive, then really is that join: .
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 . But note that in impredicative constructive matematics, Definition does not necessarily satisfy this; rather, that definition satisfies either property (hence both) if and only if it satisfies Definition . So these properties are really for Definitions and only.
Last revised on September 13, 2024 at 19:34:31. See the history of this page for a list of all contributions to it.