nLab principle of omniscience

Principles of omniscience

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Principles 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 (EMEM); to apply p¬pp \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 EMEM may happen to be valid, even constructively, for certain predicates) to their quantifications over infinite domains (where EMEM is typically not constructively valid).

The limited principle of omniscience

The limited principle of omniscience (LPOLPO) states that the existential quantification of any decidable proposition is again decidable. That is,

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

or equivalently

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

The weak limited principle of omniscience (WLPOWLPO) states that the universal quantification of any decidable proposition is again decidable. That is,

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

Note that LPOLPO implies WLPOWLPO: if P(x)P(x) is a decidable proposition, then so is ¬P(x)\neg{P(x)}, and so LPOLPO gives

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

which implies

¬(x,P(x))(x,P(x))\neg(\forall x, P(x)) \vee (\forall x, P(x))

as PP is decidable.

We have not stated the domain of quantification of the variable xx. If you take it to be the subsingleton corresponding to a given truth value and apply this principle to the constantly true proposition, then EMEM follows; conversely, EMEM implies LPOLPO (over any domain). However, Bishop's LPOLPO takes the domain to be the set of natural numbers, giving a weaker principle than EMEM. (It appears that a realizability topos based on infinite-time Turing machines validates LPOLPO but not EMEM; see Bauer (2011).) Note that propositions of the form x,P(x)\exists x, P(x) when PP is decidable are the open truth values in the Rosolini dominance.

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

While LPOLPO for \mathbb{N} is a classic example of the difference between constructive and classical mathematics, LPOLPO 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 (LLPOLLPO) 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,

(x,P(x)¬P(x))(y,Q(y)¬Q(y))¬(x,P(x)y,Q(y))¬(x,P(x))¬(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

(x,P(x)¬P(x))(y,Q(y)¬Q(y))¬(x,P(x)y,Q(y))(x,¬P(x))(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 (\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 ¬(pq)¬p¬q\neg(p \wedge q) \Rightarrow \neg{p} \vee \neg{q} (DMDM), which is weaker than EMEM; conversely, DMDM implies LLPOLLPO (over any domain). Again, Bishop's LLPOLLPO takes the domain to be \mathbb{N}, giving a principle weaker than DMDM (and also weaker than LPO LPO_{\mathbb{N}}).

Stated set-theoretically, the lesser limited principle of omniscience for AA (LLPO ALLPO_A) states that, given functions f,g:A{0,1}f, g\colon A \to \{0,1\}, if 1imfimg1 \notin \im f \cap \im g, then 1imf1 \notin \im f or 1img1 \notin \im g. So Bishop's LLPOLLPO is LLPO LLPO_{\mathbb{N}}. Note that LLPO ALLPO_A follows from LPO ALPO_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 usual apartness relation on the set \mathbb{R} of real numbers is decidable (xyx \neq y or x=yx = y), or equivalently trichotomy for the real numbers (x<yx \lt y or x=yx = y or x>yx \gt y).
  • The analytic LLPO states that the usual order on \mathbb{R} is a total order (xyx \leq y or xyx \geq y), which (by analogy with trichotomy) may be called dichotomy for the real numbers.

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 modulated Cantor 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 WCCWCC to see that an analytic result implies the (L)LPO and so cannot be constructively valid.)

That the real numbers have decidable equality is weaker than the analytic LPO (and decidable equality for the modulated Cantor reals in weaker than LPO NLPO_{\mathbf{N}}), unless we also assume Markov's principle (over N\mathbf{N} for the modulated Cantor reals, an analytic version for the Dedekind reals).

Truncated and untruncated versions in homotopy type theory

In the context of homotopy type theory, the various principles of omniscience can be translated in two ways, by interpreting “or” as propositionally truncated (“merely or”) or untruncated (“purely or”). The relationships between the truncated and untruncated principles of omniscience are as follows are:

Equivalent statements

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

  • Every modulated Cantor real number has a radix expansion in any base (e.g., a decimal expansion or binary expansion) iff LLPO NLLPO_{\mathbf{N}} holds; every Dedekind real number has a radix expansion iff the analytic LLPOLLPO holds. At least in the presence of countable choice (which also implies that modulated Cantor reals and Dedekind reals agree), this 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).

  • Let [0,1]/(01)[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 𝕊 1\mathbb{S}^1. (Constructively, we take 𝕊 1\mathbb{S}^1 to be /\mathbb{R}/\mathbb{Z}, although S 1S^1 can also be constructed as a completion of [0,1]/(01)[0,1]/(0 \sim 1).) Constructively, there is an injection [0,1]/(01)/[0,1]/(0 \sim 1) \hookrightarrow \mathbb{R}/\mathbb{Z}, which is a bijection if and only if the LLPOLLPO holds (for the appropriate kind of real number).

Models

  • Assuming that Set is a Boolean topos, then LPO LPO_{\mathbb{N}} (the LPO for natural numbers) holds in any presheaf topos over SetSet and indeed in any locally connected topos over SetSet, essentially since then 2 N2^N is a constant object.

  • The LPO for natural numbers fails in Johnstone’s topological topos, due to its internal continuity principle. Hence, the analytic LPO also fails, since the modulated Cantor reals and Dedekind reals coincide in this topos. However, the (analytic) LLPO holds, as a consequence of the preservation of finite closed unions by the inclusion of sequential spaces.

References

Last revised on December 4, 2023 at 14:21:27. See the history of this page for a list of all contributions to it.