nLab limited principle of omniscience

This page is currently under heavy revision. There are many errors on this page that need to be fixed.

Definition

The limited principle of omniscience ($LPO$) states that the existential quantification of any decidable proposition on the natural numbers is again decidable. That is,

$$(\forall x \in \mathbb{N}, P(x) \vee \neg{P(x)}) \Rightarrow (\exists x \in \mathbb{N}, P(x)) \vee \neg(\exists x \in \mathbb{N}, P(x)) ,$$

or equivalently

$$(\forall x \in \mathbb{N}, P(x) \vee \neg{P(x)}) \Rightarrow (\exists x \in \mathbb{N}, P(x)) \vee (\forall x \in \mathbb{N}, \neg{P(x)}) .$$

We can also state the principle set-theoretically. The limited principle of omniscience ($LPO$) states that given a subset $P \in \mathcal{P}(\mathbb{N})$ of the natural numbers $\mathbb{N}$, if $P$ is a decidable subset of $\mathbb{N}$ ($P \cup \bar{P} = \mathbb{N}$), then either $P$ is inhabited or $\bar{P} = \mathbb{N}$, where $\bar{P}$ is the complement of $P$.

One can equivalently use functions to the boolean domain instead of decidable subsets. The limited principle of omniscience states that given any function $f$ from the natural numbers $\mathbb{N}$ to the boolean domain $\{0,1\}$, either $f$ is the constant map to $0$ or $1$ belongs to the image of $f$. In this case, the limited principle of omniscience is also called excluded middle for semidecidable truth values, i.e. truth values of the form $\exists n, f(n) = 1$ for some boolean-valued sequence $f:\mathbb{N}\to \mathbf{2}$, or $\Sigma^0_1$-excluded middle (Diener 2018, Kawai 2018) in the sense of the arithmetical hierarchy? in computability theory.

In the antithesis interpretation

In the antithesis interpretation of constructive mathematics, propositions are functions from from the boolean domain $\{0,1\}$ to the set of truth values $\Omega$. Given any set $\mathbb{N}$ and function $f$ from $\mathbb{N}$ to $\{0,1\}$, the antithesis proposition $b \mapsto f(x) = b$ is mutually exclusive and decidable by the induction principle of the boolean domain. As a result, the affine existential quantifier $\bigsqcup_{x \in \mathbb{N}} (b \mapsto f(x) = b)$ is mutually exclusive and affirmative and the the affine universal quantifier $\bigsqcap_{x \in \mathbb{N}} (b \mapsto f(x) = b)$ is mutually exclusive and refutative. The limited principle of omniscience ($LPO$) states that, given any function $f$ from $\mathbb{N}$ to the boolean domain $\{0,1\}$, $\bigsqcup_{x \in \mathbb{N}} (b \mapsto f(x) = b)$ or $\bigsqcap_{x \in \mathbb{N}} (b \mapsto f(x) = b)$ is decidable.

Using exclusive disjunction

There is an equivalent version of the limited principle of omniscience which uses the exclusive disjunction instead of the inclusive disjunction for the definition of a decidable proposition:

The limited principle of omniscience ($LPO$) states that the existential quantification of any decidable proposition on the natural numbers is again decidable. That is,

$$(\forall x \in \mathbb{N}, P(x) \underline{\vee} \neg{P(x)}) \Rightarrow (\exists x \in \mathbb{N}, P(x)) \underline{\vee} \neg(\exists x \in \mathbb{N}, P(x)) ,$$

or equivalently

$$(\forall x \in \mathbb{N}, P(x) \underline{\vee} \neg{P(x)}) \Rightarrow (\exists x \in \mathbb{N}, P(x)) \underline{\vee} (\forall x \in \mathbb{N}, \neg{P(x)}) .$$

We can also state the principle set-theoretically: the limited principle of omniscience ($LPO$) states that, given any function $f$ from the natural numbers $\mathbb{N}$ to the boolean domain $\{0,1\}$, either $f$ is the constant map to $0$ or $1$ belongs to the image of $f$. That is,

$$\forall f \in \{0,1\}^\mathbb{N}, (\exists x \in \mathbb{N}, f(x) = 1) \underline{\vee} \neg(\exists x \in \mathbb{N}, f(x) = 1) ,$$

or equivalently

$$\forall f \in \{0,1\}^\mathbb{N}, (\exists x \in \mathbb{N}, f(x) = 1) \underline{\vee} (\forall x \in \mathbb{N}, f(x) = 0) .$$

Equivalent statements

There are various results that are equivalent to the limited principle of omniscience.

Theorem

LPO holds if and only if the function set $\mathbb{2}^\mathbb{N}$ has decidable tight apartness, where the tight apartness relation on the function set $\mathbb{2}^\mathbb{N}$ be defined as

$$f \# g \coloneqq \exists x \in \mathbb{N}.f(x) \neq g(x)$$

Proof

Since the boolean domain is a boolean ring, the function set $\mathbb{2}^\mathbb{N}$ is also a boolean ring via pointwise addition, subtraction and multiplication of boolean-valued functions. Thus, for functions $f$ and $g$ from $\mathbb{N}$ to $\mathbb{2}$, the tight apartness relation on the function set $\mathbb{2}^\mathbb{N}$, defined by

$$f \# g \coloneqq \exists x \in \mathbb{N}.f(x) \neq g(x)$$

is logically equivalent to $\exists x \in \mathbb{N}.f(x) - g(x) = 1$, since $f(x) \neq g(x)$ is logically equivalent to $f(x) = g(x) + 1$.

Suppose LPO holds. Then for functions $f$ and $g$ from $\mathbb{N}$ to $\mathbb{2}$, define the function $h$ by $h(x) = f(x) - g(x)$ for all $x \in \mathbb{N}$. Then since LPO says that $\exists x \in \mathbb{N}.h(x) = 1$ is decidable, and $\exists x \in \mathbb{N}.h(x) = 1$ is logically equivalent to $f \# g$, then $f \# g$ is decidable.

Conversely, assume that $f \# g$ is decidable. Then take $g$ to be the constant function at the boolean $0$, and $f \# \lambda x \in \mathbb{N}.0$ is logically equivalently to $\exists x \in \mathbb{N}.f(x) - 0 = 1$ and thus $\exists x \in \mathbb{N}.f(x) = 1$. Since $f \# g$ is decidable, then $\exists x \in \mathbb{N}.f(x) = 1$ is decidable, which is LPO.

Other statements

We have the equivalence of LPO with the analytic LPO for various notions of real numbers.

• The analytic LPO for the following sets of real numbers are equivalent to LPO: the Cauchy real numbers $\mathbb{R}_C$, the Escardo-Simpson real numbers/HoTT book real numbers $\mathbb{R}_E$/$\mathbb{R}_H$, and the subfield of Dedekind real numbers $\mathbb{R}_\Sigma \subseteq \mathbb{R}_D$ which are constructed out of Dedekind cuts valued in the set of quasidecidable propositions $\Sigma \subseteq \Omega$.

Proofs of this theorem are available at the article analytic LPO.

One also has:

• The Bolzano-Weierstrass theorem states that the unit interval is sequentially compact, and it holds of the Cauchy real numbers if and only if LPO holds; see Mandelkern 1988.

• The Cauchy real numbers are isomorphic to the radix expansion in any base (e.g., a decimal expansion or binary expansion) iff LPO holds; see Feldman (2010).

• Every semidecidable proposition is a decidable proposition if and only if LPO holds; see Diener 2018.

• Every quasidecidable proposition is a decidable proposition if and only if LPO holds; see at quasidecidable proposition for a proof.

• Let $\mathbb{N}_\infty$ denote the extended natural numbers. We say that an extended natural number $x \in \mathbb{N}_\infty$ is finite if it is in the image of the canonical injection $i:\mathbb{N} \hookrightarrow \mathbb{N}_\infty$ of the natural numbers into the extended natural numbers. Escardo 17 showed that LPO holds if and only if for all extended natural numbers $x \in \mathbb{N}_\infty$, finiteness of $x$ is decidable proposition.

These statements beneath this standout box currently do not have proofs on the nLab or references to literature containing a proof of the statement. Please add such proofs or references to the article, or delete them if these statements are not true.

• Every Cauchy real number is a rational number or has an strictly non-repeating base $b$ radix expansion if and only if LPO holds.

• LPO holds if and only if for every function $f:\mathbb{N} \to \mathbb{N}$ from $\mathbb{N}$ to the natural numbers, either there exists an element $x \in \mathbb{N}$ and a natural number $n$ such that $f(x) = n + 1$, or for all elements $x \in \mathbb{N}$ we have $f(x) = 0$.

• Given a finite set $S$ of cardinality $n \gt 1$, LPO holds if and only if that the function set $S^\mathbb{N}$ has decidable tight apartness, where the tight apartness relation on the function set $S^\mathbb{N}$ be defined as

  $$f \# g \coloneqq \exists x \in \mathbb{N}.f(x) \neq g(x)$$

• The $p$-adic integers being a discrete integral domain and the $p$-adic rationals being a discrete field are both equivalent to LPO.

• LPO holds if and only if the function set $\mathbb{N}^\mathbb{N}$ has decidable tight apartness, where the tight apartness relation on the function set $\mathbb{N}^\mathbb{N}$ be defined as

  $$f \# g \coloneqq \exists x \in \mathbb{N}.f(x) \neq g(x)$$

• The ring of rational power series $\mathbb{Q}[[x]]$ being a discrete integral domain is equivalent to LPO. Similarly, the Heyting field of rational Laurent series $\mathbb{Q}((x))$ being a discrete field is equivalent to LPO.

Let $C$ denote the category of discrete sequentially Cauchy complete Archimedean ordered fields. $C$ is a groupoid and a subsingleton up to unique isomorphism: for every two objects $R \in C$ and $R' \in C$ there exists a unique morphism between $R$ and $R'$ which is an isomorphism.

• LPO holds if and only if there is an object $\mathbb{R} \in C$, which will necessarily be unique up to unique isomorphism, and LPO fails if and only if $C$ is an empty category.

Consequences

There are various statements that are consequences of LPO.

Theorem

WLPO follows from LPO, but not conversely.

Proof

If $P(x)$ is a decidable proposition, then so is $\neg{P(x)}$, and so LPO gives

$$(\exists x \in \mathbb{N}, \neg{P(x)}) \vee (\forall x \in \mathbb{N}, \neg{\neg{P(x)}}),$$

which implies

$$\neg(\forall x \in \mathbb{N}, P(x)) \vee (\forall x \in \mathbb{N}, P(x))$$

as $P$ is decidable.

Theorem

LLPO follows from LPO, but not conversely.

Proof

LLPO follows from LPO, WLPO is equivalent to fully untruncated LLPO, which implies LLPO, and WLPO follows from LPO. However, the converse does not necessarily hold, since in http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf is a model by Michael Rathjen that separates WLPO from LLPO. Similarly, Grossack 24 shows that Johnstone’s topological topos separates WLPO from LLPO. Thus LLPO is separated from LPO.

Statements that imply LPO

There are various other statements that imply LPO, some of which are listed in this section.

• full bar induction implies LPO; see Troelstra & van Dalen 1988 and Kawai 2018

There are also some results from constructive ordinal theory:

• If every pair of ordinals $\alpha$ and $\beta$ has a binary meet, then LPO holds; this is Proposition 5.2 in de Jong, Kraus, Mohammadzadeh, & Forsberg 2026.

• If binary joins exist for non-successor ordinals $\alpha$ and $\beta$, then LPO holds; this is Proposition 6.2 in de Jong, Kraus, Mohammadzadeh, & Forsberg 2026.

Statements inconsistent with LPO

There are various statements in mathematics which are inconsistent with LPO, some of which are listed here.

• LPO is inconsistent with the existence of a Specker sequence; see Diener 2018.

• LPO is inconsistent with Phoa's principle and synthetic quasi-coherence for the set of quasidecidable propositions; see at quasidecidable proposition for a proof.

In real analysis

Theorem

LPO is inconsistent with Brouwer's continuity principle for any one of the Cauchy real numbers $\mathbb{R}_C$, the HoTT book real numbers $\mathbb{R}_H$, or the Dedekind real numbers $\mathbb{R}_\Sigma$ defined using the set of quasidecidable propositions.

Proof

LPO implies that $\mathbb{R}_C$, $\mathbb{R}_H$, and $\mathbb{R}_\Sigma$ are equivalent to each other, which means we can simply denote this set of real numbers as $\mathbb{R}$, and that the pseudo-order relation on $\mathbb{R}$ is decidable. As a result, we can define a pointwise-discontinuous function $f:\mathbb{R} \to \mathbb{R}$ by case analysis: $f(x) = 1$ if $x \gt 0$ and $f(x) = 0$ if $x \leq 0$. This contradicts Brouwer’s continuity principle which says that all functions $f:\mathbb{R} \to \mathbb{R}$ are pointwise-continuous.

Theorem

In the presence of the weak countable choice axiom $\mathrm{AC}_{\mathbb{N}, 2}$, LPO is inconsistent with Brouwer's continuity principle for the usual impredicative Dedekind real numbers defined using the frame of truth values $\Omega$.

Proof

$\mathrm{AC}_{\mathbb{N}, 2}$ implies that the Cauchy real numbers and the Dedekind real numbers coincide. Since the previous theorem implies that LPO is inconsistent with Brouwer's continuity principle for the Cauchy real numbers, $\mathrm{AC}_{\mathbb{N}, 2}$ implies that LPO is inconsistent with Brouwer's continuity principle for the Dedekind real numbers.

This means that theories which accept both LPO and Brouwer's continuity principle for the Dedekind real numbers, such as the internal logic of the cohesive (infinity,1)-topos of Euclidean-topological infinity-groupoids, necessarily reject $\mathrm{AC}_{\mathbb{N}, 2}$.

Models

• Assuming that Set is a Boolean topos, then $LPO$ holds in any presheaf topos over $Set$ and indeed in any locally connected topos over $Set$, essentially since then $2^N$ is a constant object.

• LPO fails in Johnstone’s topological topos, due to its internal continuity principle. Hence, the analytic LPO also fails, since the modulated Cauchy reals and Dedekind reals coincide in this topos.

• LPO fails in the parameterized realizability topos constructed in Bauer & Hanson 2024.

• It appears that a realizability topos based on infinite-time Turing machines validates $LPO$ but not $EM$; see Bauer 2015.

Generalizations

Choiceless limited principle of omniscience

There is a generalization of the limited principle of omniscience defined in King 2024, which was suggested to be called the choiceless limited principle of omniscience. The choiceless limited principle of omniscience states that given and a pair of predicates $P$ and $Q$ on $\mathbb{N}$ such that $P(x) \vee Q(x)$ holds for all $x \in \mathbb{N}$, then either there exists $x \in \mathbb{N}$ such that $P(x)$ or for all $x \in \mathbb{N}$, $Q(x)$. The idea behind the term “choiceless” is that one isn’t forced to choose between $P(x)$ or $Q(x)$ in this version of the limited principle of omniscience. One gets back the usual limited principle of omniscience if $P(x)$ and $Q(x)$ are mutually exclusive propositions for all $x \in A$, from which $Q(x)$ if and only if $\neg P(x)$ for all $x \in \mathbb{N}$.

We can also state the principle set-theoretically. The choiceless limited principle of omniscience states that given subsets $P, Q \in \mathcal{P}(\mathbb{N})$, if $P \cup Q = \mathbb{N}$, then either $P$ is inhabited or $Q = \mathbb{N}$. One gets back the usual limited principle of omniscience if $P$ and $Q$ are disjoint subsets $P \cap Q = \emptyset$, from which $Q = \bar{P}$, where $\bar{P}$ is the complement of $P$.

The choiceless limited principle of omniscience implies the analytic limited principle of omniscience for all sets of real numbers, as shown in King 2024, thus also implying that the real numbers coincide with each other.

Exhaustible sets

One can consider generalizing the domain of discourse of the limited principle of omniscience from the natural numbers to an arbitrary set $A$. Such sets satisfying the limited principle of omniscience are called exhaustible sets.

Related concepts

• principle of omniscience

• weak limited principle of omniscience

• lesser limited principle of omniscience

• Markov's principle

• excluded middle

• exhaustible set

 References

• Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)

  (in the introduction or chapter 1, I forget)

• Mark Mandelkern, Components of an open set, Journal of the Australian Mathematical Society, Volume 33, Issue 2, October 1982, pp. 249 - 261, [doi:10.1017/S1446788700018383, pdf]

• Mark Mandelkern: Limited Omniscience and the Bolzano-Weierstrass Principle, Bulletin of the London Mathematical Society 20 4 (1988) 319–320, [doi:10.1112/blms/20.4.319, pdf]

• Anne Sjerp Troelstra, Dirk van Dalen: Constructivism in Mathematics – An introduction, Volume I, Studies in Logic and the Foundations of Mathematics 121, North Holland (1988) [ISBN:9780444702661]

• Fred Richman, Polynomials and linear transformations. Linear Algebra and its Applications, Volume 131, 1 April 1990, Pages 131-137. [doi:10.1016/0024-3795(90)90379-Q]

• Hajime Ishihara: Reverse Mathematics in Bishop’s Constructive Mathematics, Philosophia Scientiæ, CS 6 (2006) [doi:10.4000/philosophiascientiae.406, pdf]

• Yasuhito Tanaka: The Gibbard–Satterthwaite theorem of social choice theory in an infinite society and LPO (limited principle of omniscience), Applied Mathematics and Computation 193 2 (2007) 475–481 [doi:10.1016/j.amc.2007.04.001, pdf archived]

• Henri Lombardi, Claude Quitté (trans. buTania K. Roblo): Commutative algebra: Constructive methods (Finite projective modules), Springer (2015) [doi:10.1007/978-94-017-9944-7, pdf]

• Michael Rathjen: Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience [arXiv:1302.3037]

• Martín Escardó: Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic, Vol 78, September 2013, pp. 764-784. [doi:10.2178/jsl.7803040, pdf]

• Andrej Bauer, An injection from the Baire space to natural numbers. Mathematical Structures in Computer Science. 2015;25(7):1484-1489. [doi:10.1017/S0960129513000406, pdf]

• Tatsuji Kawai: Principles of bar induction and continuity on Baire space [arXiv:1808.04082]

• Mike Shulman: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science 28 6 (2018) 856–941 [arXiv:1509.07584, doi:10.1017/S0960129517000147]

• Hannes Diener, Constructive Reverse Mathematics, Habil. thesis, Univ. Siegen (2018) [arXiv:1804.05495, dspace:ubsi/1306]

• Auke Booij: Analysis in univalent type theory (2020) [etheses:10411, pdf]

• Andrej Bauer: Instance reducibility and Weihrauch degrees, Logical Methods in Computer Science 18 3 (2022) [doi:10.46298/lmcs-18(3:20)2022,arXiv:2106.01734, pdf]

• Francesco Ciraulo: $\sigma$-locales in Formal Topology, Logical Methods in Computer Science 18 1 (2022) [doi:10.46298/lmcs-18%281%3A7%292022, arXiv:1801.09644]

• Egbert Rijke: Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (2025) [doi:10.1017/9781108933568, arXiv:2212.11082]

• Andrej Bauer, James Hanson, The Countable Reals (arXiv:2404.01256)

• Chris Grossack, Life in Johnstone’s Topological Topos 3 – Bonus Axioms (web)

• Madeleine Birchfield, Andrew Swan (2024) on Category Theory Zulip, LPO and sigma-frame structure on booleans

• Henri Lombardi, Assia Mahboubi, Théories géométriques pour l’algèbre des nombres réels sans test de signe ni axiome de choix dépendant (arXiv:2406.15218)

• Christopher King, What are these generalizations of the principles of omniscience called?, MathOverflow, 15 February 2024. (web)

• Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg, Generalized Decidability via Brouwer Trees (arXiv:2602.10844)

• Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Louis Wasserman: The limited principle of omniscience, Agda-Unimath library for Agda, [web]

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Martin Escardo: Taboos.LPO, TypeTopology Agda library, web.

• Martin Escardo: TypeTopology.CompactTypes, TypeTopology Agda library, web.

• Martin Escardo: TypeTopology.WeaklyCompactTypes, TypeTopology Agda library, web.