In constructive mathematics, the limited principle of omniscience (LPO) and the lesser limited principle of omniscience (LLPO) are axioms that are nonconstructive but are weaker than the full law of the excluded middle. They are used to gauge the amount of nonconstructivity required for an argument, as in constructive reverse mathematics. These principles are also related to weak counterexamples in the sense of Brouwer.

The limited principle of omniscience states (Bridges & Richman 1987, p. 3):

LPO: For any sequence ${\displaystyle a_{0}}$, ${\displaystyle a_{1}}$, ... such that each ${\displaystyle a_{i}}$ is either ${\displaystyle 0}$ or ${\displaystyle 1}$, the following holds: either ${\displaystyle a_{i}=0}$ for all ${\displaystyle i}$, or there is a ${\displaystyle k}$ with ${\displaystyle a_{k}=1}$. ^[1]

The second disjunct can be expressed as ${\displaystyle \exists k.a_{k}\neq 0}$ and is constructively stronger than the negation of the first, ${\displaystyle \neg \forall k.a_{k}=0}$. The weak schema in which the former is replaced with the latter is called WLPO and represents particular instances of excluded middle.^[2]

The lesser limited principle of omniscience states:

LLPO: For any sequence ${\displaystyle a_{0}}$, ${\displaystyle a_{1}}$, ... such that each ${\displaystyle a_{i}}$ is either ${\displaystyle 0}$ or ${\displaystyle 1}$, and such that at most one ${\displaystyle a_{i}}$ is nonzero, the following holds: either ${\displaystyle a_{2i}=0}$ for all ${\displaystyle i}$, or ${\displaystyle a_{2i+1}=0}$ for all ${\displaystyle i}$.

Here ${\displaystyle a_{2i}}$ and ${\displaystyle a_{2i+1}}$ are entries with even and odd index respectively.

It can be proved constructively that the law of the excluded middle implies LPO, and LPO implies LLPO. However, none of these implications can be reversed in typical systems of constructive mathematics.

• Constructive analysis