< [[nlab:principle of omniscience]] The **limited principle of omniscience (LPO)**, the **weak limited principle of omniscience (WLPO)**, and the **lesser limited principle of omniscience (LLPO)** are classicality axioms that are weaker than [[excluded middle]]. For now, see [[nlab:principle of omniscience|the nlab]] for their statements. They can be translated into HoTT in two ways, by interpreting "or" as truncated ("merely or") or untruncated ("purely or"). The relationships are: * Truncated LPO and untruncated LPO are equivalent; see Exercise 3.19 in [[the HoTT book]]. (due to [[nLab:MartÃn Escardó]]) * Similarly, truncated WLPO and untruncated WLPO are equivalent. * Untruncated LLPO is equivalent to WLPO (also due to Martin Escardo). * In <http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf> is a model by Michael Rathjen that separates WLPO from LLPO. ## Definition ## The **truncated limited principle of omniscience** for a type $A$ states that for every boolean predicate on $A$, either it is the constant function into $0$ or the fiber of the boolean predicate at $1$ is inhabited: $$\prod_{P:A \to \mathbb{2}} \left[\left[fiber(P, 1)\right] + \prod_{a:A} P(a) = 0\right]$$ ## See also ## * [[decidable set]]