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** states that for every boolean predicate on the natural numbers, either it is the constant function into $0$ or the fiber of the boolean predicate at $1$ is inhabited: $$\prod_{P:\mathbb{N} \to \mathbb{2}} \left[\left[fiber(P, 1)\right] + \prod_{n:\mathbb{N}} P(n) = 0\right]$$ ## Properties ## * If the [[Dedekind real numbers]] each have a [[locator]], then the weak limited principle of omniscience is true. * If the [[Cauchy real numbers]] each have an infinite decimal representation, then the limited principle of omniscience is true. ## See also ## * [[decidable set]] * [[infinite decimal representation of a unit interval]] * [[pre-algebra real numbers]]