nLab lesser limited principle of omniscience

Definition

The lesser limited principle of omniscience ($LLPO$) is a principle of omniscience which states that, if the existential quantification of the conjunction of two decidable propositions on the natural numbers is false, then one of their separate existential quantifications is false. That is,

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

or equivalently

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

We can also state the principle set-theoretically. The lesser limited principle of omniscience (LLPO) states that given subsets $P, Q \in \mathcal{P}(\mathbb{N})$, if $P$ and $Q$ are decidable subsets of $\mathbb{N}$ ($P \cup \bar{P} = \mathbb{N}$, $Q \cup \bar{Q} = \mathbb{N}$), then if it is not true that both $P$ and $Q$ are inhabited subsets of $\mathbb{N}$, then either $\bar{P} = \mathbb{N}$ or $\bar{Q} = \mathbb{N}$, where $\bar{P}$ and $\bar{Q}$ are the complements of $P$ and $Q$ respectively.

One can also use functions to the boolean domain instead of decidable subsets: the lesser limited principle of omniscience (LLPO) states that, given functions $f, g\colon \mathbb{N} \to \{0,1\}$, if $1 \notin \im f \cap \im g$, then $1 \notin \im f$ or $1 \notin \im g$.

Equivalent statements

There are various other results that are equivalent to the principles of omniscience. Here are a few:

• Let $[0,1]/(0 \sim 1)$ be the quotient of the unit interval that identifies the endpoints, and let $\mathbb{R}/\mathbb{Z}$ be the quotient ring; both are classically isomorphic to the circle $\mathbb{S}^1$. (Constructively, we take $\mathbb{S}^1$ to be $\mathbb{R}/\mathbb{Z}$, although $S^1$ can also be constructed as a completion of $[0,1]/(0 \sim 1)$.) Constructively, there is an injection $[0,1]/(0 \sim 1) \hookrightarrow \mathbb{R}/\mathbb{Z}$, which is a bijection if and only if the $LLPO$ holds (for the appropriate kind of real number).

• The analytic LLPO for the Cauchy real numbers is equivalent to the LLPO.

 Related statements

There are various other results that are related to the principles of omniscience. Here are a few:

• The limited principle of omniscience (LPO) and the weak limited principle of omniscience (WLPO) for natural numbers imply LLPO, but not conversely.

• The lesser limited principles of omniscience implies that every pointwise continuous function from the Cauchy unit interval to the Cauchy real numbers is a uniformly continuous function. See section 6.1 of Diener (2018).

• In the presence of the weak countable choice axiom $\mathrm{AC}_{\mathbb{N}, 2}$, there exists a radix expansion in any base (e.g., a decimal expansion or binary expansion) for every Cauchy real number iff LLPO holds. Without weak countable choice, Lifschitz realizability gives a model in which LLPO holds but it is not true that there exists a radix expansion in any base for every Cauchy real number. See Swan (2024).

• In the presence of countable choice, LLPO is equivalent to the claim that the rings of radix expansions in any two bases are isomorphic. See Daniel Mehkeri's answer to Feldman (2010).

Untruncated LLPO in dependent type theory

In the context of dependent type theory, the lesser limited principles of omniscience can be translated in two ways, by interpreting “or” as propositionally truncated (“merely or”) or untruncated (“purely or”); see Escardo 23. The relationships between the truncated and untruncated LLPO are as follows are:

• Untruncated LLPO is equivalent to WLPO (also due to Escardo 23).

• In http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf is a model by Michael Rathjen that separates WLPO from (truncated) LLPO. Similarly, Grossack 24 shows that Johnstone’s topological topos separates WLPO from (truncated) LLPO.

Thus, untruncated LLPO is strictly stronger than truncated LLPO, unlike the case for LPO and WLPO.

Models

• The (analytic) LLPO holds in Johnstone’s topological topos, as a consequence of the preservation of finite closed unions by the inclusion of sequential spaces.

Generalizations

Choiceless lesser limited principle of omniscience

There is a generalization of the lesser limited principle of omniscience defined in King 2024, which was suggested to be called the choiceless lesser limited principle of omniscience. The choiceless lesser limited principle of omniscience states that given a pair of predicates $P$ and $Q$ on the natural numbers such that $P(x) \vee Q(x)$ holds for all $x \in \mathbb{N}$, and a pair of predicates $R$ and $S$ such that $R(x) \vee S(x)$ holds for all $x \in \mathbb{N}$, then if it is not true that there exists $x \in \mathbb{N}$ such that $P(x)$ and there exists $x \in \mathbb{N}$ such that $R(x)$ hold, then either for all $x \in \mathbb{N}$, $Q(x)$ or for all $x \in \mathbb{N}$, $S(x)$.

$$((\forall x \in \mathbb{N}.P(x) \vee Q(x)) \wedge (\forall x \in \mathbb{N}.R(x) \vee S(x))) \Rightarrow \neg (\exists x \in \mathbb{N}.P(x) \wedge \exists x \in \mathbb{N}.R(x)) \Rightarrow ((\forall x \in \mathbb{N}.Q(x)) \vee (\forall x \in \mathbb{N}.S(x)))$$

The idea behind the term “choiceless” is that one isn’t forced to choose between $P(x)$ or $Q(x)$ or between $R(x)$ or $S(x)$ in this version of the lesser limited principle of omniscience. One gets back the usual lesser limited principle of omniscience if $P(x)$ and $Q(x)$ are mutually exclusive propositions for all $x \in \mathbb{N}$ and $R(x)$ and $S(x)$ are mutually exclusive propositions for all $x \in \mathbb{N}$, from which $Q(x)$ if and only if $\neg P(x)$ for all $x \in \mathbb{N}$ and $S(x)$ if and only if $\neg R(x)$ for all $x \in \mathbb{N}$.

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

The choiceless lesser limited principle of omniscience implies the analytic lesser limited principle of omniscience for all sets of real numbers, as shown in King 2024.

Related concepts

• principle of omniscience

• limited principle of omniscience

• weak limited principle of omniscience

• Markov's principle

• de Morgan's law

References

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

  (in the introduction or chapter 1, I forget)

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

• David Feldman (2010) on Math.Overflow, Radix notation and toposes

• Henri Lombardi, Claude Quitté (2010): Commutative algebra: Constructive methods (Finite projective modules) Translated by Tania K. Roblo, 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]

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

• Hannes Diener, Constructive reverse mathematics, Habilitationsschrift Fakultät IV - Naturwissenschaftlich-Technische Fakultät, 2018. (arXiv:1804.05495, dspace:ubsi/1306)

• Michael Rathjen, Andrew Swan, Lifschitz Realizability as a Topological Construction. The Journal of Symbolic Logic, Volume 85, Issue 4, December 2020, pp. 1342 - 1375. [doi:10.1017/jsl.2021.1, arXiv:1806.10047]

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

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

• Andrew Swan (2024) on Category Theory Zulip, Radix expansions in constructive mathematics

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

• Felix Cherubini, Thierry Coquand, Freek Geerligs, Hugo Moeneclaey, A Foundation for Synthetic Stone Duality (arXiv:2412.03203)

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