nLab
principle of omniscience

Idea

In logic and foundations, a principle of omniscience is any principle of classical mathematics that is not valid in constructive mathematics. The idea behind the name (which is due to Bishop (1967)) is that, if we attempt to extend the computational interpretation of constructive mathematics to incorporate one of these principles, we would have to know something that we cannot compute. The main example is the law of excluded middle ($\mathrm{EM}$); to apply $p\vee \neg p$ computationally, we must know which of these disjuncts hold; to apply this in all situations, we would have to know everything (hence ‘omniscience’).

Bishop's principles of omniscience (stated below) may be seen as principles that extend classical logic from predicates (where $\mathrm{EM}$ may happen to be valid, even constructively, for certain predicates) to their quantifications over infinite domains (where $\mathrm{EM}$ is typically not constructively valid).

The limited principle of omniscience

The limited principle of omniscience ($\mathrm{LPO}$) states that the existential quantification of any decidable proposition is again decidable. That is,

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

or equivalently

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

We have not stated the domain of quantification of the variable $x$. If you take it to be the subsingleton corresponding to a given truth value and apply this principle to the constantly true proposition, then $\mathrm{EM}$ follows; conversely, $\mathrm{EM}$ implies $\mathrm{LPO}$ (over any domain). However, Bishop's $\mathrm{LPO}$ takes the domain to be the set of natural numbers, giving a weaker principle than $\mathrm{EM}$. (It appears that a realizability topos based on infinite-time Turing machine?s validates $\mathrm{LPO}$ but not $\mathrm{EM}$; see Bauer (2011).)

We can also state the principle set-theoretically, with explicit reference to the domain of quantification. Given a set $A$, the limited principle of omniscience for $A$ (${\mathrm{LPO}}_A$) states that, given any function $f$ from $A$ to the boolean domain $\{0,1\}$, either $f$ is the constant map to $0$ or $1$ belongs to the image of $f$. Then Bishop's $\mathrm{LPO}$ is ${\mathrm{LPO}}_{\mathbb{N}}$, which applies to any infinite sequence of bits.

While $\mathrm{LPO}$ for $\mathbb{N}$ is a classic example of the difference between constructive and classical mathematics, $\mathrm{LPO}$ holds for the set $\overline{\mathbb{N}}$ of extended natural numbers; this is related to the fact that $\overline{\mathbb{N}}$ may constructively be given a compact topology. See Escardó (2011) for this and much more.

The lesser limited principle of omniscience

The lesser limited principle of omniscience ($\mathrm{LLPO}$) states that, if the existential quantification of the conjunction of two decidable propositions is false, then one of their separate existential quantifications is false. That is,

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

or equivalently

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

If, as before, you take the domains of quantification to be subsingletons, you get de Morgan's law $\neg (p\wedge q)\Rightarrow \neg p\vee \neg q$ ($\mathrm{DM}$), which is weaker than $\mathrm{EM}$; conversely, $\mathrm{DM}$ implies $\mathrm{LLPO}$ (over any domain). Again, Bishop's $\mathrm{LLPO}$ takes the domain to be $\mathbb{N}$, giving a principle weaker than $\mathrm{DM}$ (and also weaker than ${\mathrm{LPO}}_{\mathbb{N}}$).

Stated set-theoretically, the lesser limited principle of omniscience for $A$ (${\mathrm{LLPO}}_A$) states that, given functions $f,g:A\to \{0,1\}$, if $1\notin imf\cap img$, then $1\notin imf$ or $1\notin img$. So Bishop's $\mathrm{LLPO}$ is ${\mathrm{LLPO}}_{\mathbb{N}}$. Note that ${\mathrm{LLPO}}_A$ follows from ${\mathrm{LPO}}_A$, but not conversely.

Analytic versions

Bishop introduced the above principles of omniscience to show that certain results in pointwise analysis could not be constructive, by showing that these results implied a principle of omniscience. The principles of omniscience that appear directly in analysis are these:

• The analytic LPO states that the set $ℝ$ of real numbers has decidable equality ($x=y$ or $x\ne y$).
• The analytic LLPO states that the usual order on $ℝ$ is a total order ($x\le y$ or $x\ge y$).

The analytic (L)LPO implies the (L)LPO for natural numbers; the converses hold if we assume weak countable choice (as Bishop did). In any case, if we use the Cauchy real numbers (sequential real numbers), then the sequential analytic (L)LPO is the same as the (L)LPO for natural numbers.

(Note that we need not accept $\mathrm{WCC}$ to see that an analytic result implies the (L)LPO and so cannot be constructively valid.)

There are various other results that are equivalent to or related to the principles of omniscience, which it might be handy to collect here. For the connection to writing real numbers as decimals (or in some other radix), see Daniel Mehkeri's answer to Feldman (2010).

References

• Andrej Bauer (2011) via constructivenews, An Injection from ${\mathbb{N}}^{\mathbb{N}}$ to $\mathbb{N}$ (pdf)

• Erret Bishop? (1967), Foundations of Constructive Analysis (in the introduction or chapter 1, I forget)

• Martín Escardó? (2011) via constructivenews, Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics (pdf)

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