Homotopy Type Theory limited principle of omniscience > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

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 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 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]

Homotopy Type Theory limited principle of omniscience > history (Rev #3, changes)

Definition

See also