Limited principle of omniscience

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 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}$, where ${\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.

The term "omniscience" comes from a thought experiment regarding how a mathematician might tell which of the two cases in the conclusion of LPO holds for a given sequence ${\displaystyle (a_{i})}$. Answering the question "is there a ${\displaystyle k}$ with ${\displaystyle a_{k}=1}$?" negatively, assuming the answer is negative, seems to require surveying the entire sequence. Because this would require the examination of infinitely many terms, the axiom stating it is possible to make this determination was dubbed an "omniscience principle" by Bishop (1967).

• Bishop, Errett (1967). Foundations of Constructive Analysis. ISBN 4-87187-714-0.
• Bridges, Douglas; Richman, Fred (1987). Varieties of Constructive Mathematics. ISBN 0-521-31802-5.

• "Constructive Mathematics" entry by Douglas Bridges in the Stanford Encyclopedia of Philosophy