nLab positive element

Redirected from "SQIR".
Positive elements

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 LL be a preordered set, and let xx be an element of LL.

Definition

(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).

Definition

(in classical mathematics, and in impredicative constructive mathematics)

An element xx of LL is positive if whenever xx is the join of some subset AA of {x}\{x\} in LL, AA is inhabited (and so all of {x}\{x\}): P:Prop,x={x|P}P\forall P\colon Prop,\; x = \bigvee \{x \;|\; P\} \;\Rightarrow\; P.

It follows that any arbitrary subset AA of LL is inhabited if xx is the join of AA. (This is because if x=Ax = \bigvee A, then x={x|Aisinhabited}x = \bigvee \{x \;|\; A\ is\ inhabited\}.) 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.

Definition

(in predicative constructive mathematics)

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

  • If xx is the join of a subset and xx is positive, then some element of that subset is positive: xx=AuA,u\lozenge{x} \;\wedge\; x = \bigvee A \;\vdash\; \exists\, u \in A,\; \lozenge{u}.

  • If xx equals a join on the assumption that xx is positive, then xx really is that join: xx=Ax=A\lozenge{x} \;\Rightarrow\; x = \bigvee A \;\vdash\; x = \bigvee A.

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.

Examples

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|a}a = \bigvee \{ a \;|\; \lozenge{a} \} (that is, a={b|b=ab}a = \bigvee \{ b \;|\; b = a \;\wedge\; \lozenge{b} \}). 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|a}b \leq \bigvee \{ a \;|\; \lozenge{a} \}. Therefore supB{a|a}\sup B \leq \bigvee \{ a \;|\; \lozenge{a} \} holds as well. The other inequality is trivial.

Every atom of LL 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:

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

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

a={a} +={a|a} a = \bigvee \{a\}^+ = \bigvee \{ a | \lozenge{a} \}

for any element aa. 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.