Positivity Predicate

A positivity predicate $\diamond:L\to\Omega$ on a Suplattice $(L,\leq)$ algebraicizes predicates like "$S$ is Merely Inhabited" that are constructively stronger than "$S$ is Nonempty". Explicitly, $\diamond:L\to\Omega$ is a positivity predicate if:

• $x\leq y\to\diamond x\to\diamond y$

• $\diamond\bigvee_{i:I}x_{i}\to\exists(i:I).\;\diamond x_{i}$

• $(\diamond x\to x\leq y)\to x\leq y$

We can replace the 3rd condition with the equivalent condition:

Examples

• The predicate of Merely Inhabitation is a positivity predicate on the Power Set of a type $X$.

References

• Ciraulo, Francesco, and Michele Contente. “Overlap Algebras: A Constructive Look at Complete Boolean Algebras.” Logical Methods in Computer Science Volume 16, Issue 1 (February 13, 2020): 5417. https://doi.org/10.23638/LMCS-16(1:13)2020.