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).

Definition

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)}) .

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 weak limited principle of omniscience

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)).

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}}.

Relation between the principles of omniscience

We have the following relations between the three principles of omniscience:

  • WLPOWLPO follows from LPOLPO, but not conversely. 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.

  • LLPOLLPO follows from LPOLPO, but not conversely.

In the internal logic

In set theory, there are actually two different notions of logic: there is the external predicate logic used to define the set theory itself, and there is the internal predicate logic induced by the set operations on subsingletons and injections. In particular,

  • An internal proposition is a set PP such that for all elements xAx \in A and yAy \in A, x=yx = y.

  • The internal proposition true is a singleton \top.

  • The internal proposition false is the empty set

  • The internal conjunction of two internal propositions PP and QQ is the cartesian product P×QP \times Q of PP and QQ.

  • The internal disjunction of two internal propositions PP and QQ is the image of the unique function ! PQ:PQ1!_{P \uplus Q}:P \uplus Q \to 1 from the disjoint union of PP and QQ to the singleton \top.

PQ=im(! PQ)P \vee Q = \mathrm{im}(!_{P \uplus Q})
  • The internal implication of two internal propositions PP and QQ is the function set PQP \to Q between PP and QQ.

  • The internal negation of an internal proposition PP is the function set from PP to the empty set

¬P=P\neg P = P \to \emptyset
  • An internal proposition PP is a decidable proposition if it comes with a function χ P:P2\chi_P:P \to 2 from PP to the boolean domain 22.

  • An internal predicate on a set AA is a set PP with injection i:PAi:P \hookrightarrow A, whose family of propositions indexed by xAx \in A is represented by the preimages i *(x)i^*(x).

  • The internal existential quantifier of an internal predicate i:PAi:P \hookrightarrow A is the image of the unique function ! P:P!_P:P \to \top into the singleton \top.

AP=im(! P)\exists_A P = \im(!_P)
AP={fP A|xA,f(x)i *(x)}\forall_A P = \{f \in P^A \vert \forall x \in A, f(x) \in i^*(x) \}
  • An internal predicate i:PAi:P \hookrightarrow A is a decidable proposition if it comes with a function χ P(x):i *(x)2\chi_P(x):i^*(x) \to 2 into the boolean domain for all elements xAx \in A, or equivalently if it comes with a function χ P:A2\chi_P:A \to 2 from AA to the boolean domain 22.

Then the internal LPO for a family of sets (A z) zI(A_z)_{z \in I} is the LPO for each A zA_z stated in the internal logic of the set theory:

  • For any internal predicate i:PA zi:P \hookrightarrow A_z, if there is a function χ P:A z2\chi_P:A_z \to 2, then the internal existential quantification of PP, A zP=im(! P)\exists_{A_z} P = \im(!_P) has a function ( A zP)2(\exists_{A_z} P) \to 2 into the boolean domain.

or equivalently, as

  • For any function a:A z2a:A_z \to 2, the internal existential quantification of P={xA z|a(x)=1}P = \{x \in A_z \vert a(x) = 1\}, A zP=im(! P)\exists_{A_z} P = \im(!_P) has a function ( A zP)2(\exists_{A_z} P) \to 2 into the boolean domain.

Similarly, the internal WLPO for a family of sets (A z) zI(A_z)_{z \in I} is the WLPO for each A zA_z stated in the internal logic of the set theory:

  • For any internal predicate i:PA zi:P \hookrightarrow A_z, if there is a function χ P:A z2\chi_P:A_z \to 2, then the internal universal quantification of PP, A zP={fP A z|xA z,f(x)i *(x)}\forall_{A_z} P = \{f \in P^{A_z} \vert \forall x \in A_z, f(x) \in i^*(x) \} has a function ( A zP)2(\forall_{A_z} P) \to 2 into the boolean domain.

or equivalently

  • For any function a:A z2a:A_z \to 2, the internal universal quantification of P={xA z|a(x)=1}P = \{x \in A_z \vert a(x) = 1\}, A zP={fP A z|xA z,f(x)i *(x)}\forall_{A_z} P = \{f \in P^{A_z} \vert \forall x \in A_z, f(x) \in i^*(x) \} has a function ( A zP)2(\forall_{A_z} P) \to 2 into the boolean domain.

And finally, the internal LLPO for a family of sets (A z) zI(A_z)_{z \in I} is the LLPO for each A zA_z stated in the internal logic of the set theory:

  • The internal LPO for a family of sets (A z) zI(A_z)_{z \in I} holds only for the internal predicates i:PA zi:P \hookrightarrow A_z which comes with an internal predicate j:QA zj:Q \hookrightarrow A_z such that i *(x)=¬j *(x)i^*(x) = \neg j^*(x) for all xA zx \in A_z.

In particular, the internal LPO for the family of all subsingletons is internal excluded middle and the internal LLPO for the family of all subsingletons is internal weak excluded middle. Similarly, given a universe UU, the internal LPO for the family of all sets in UU is excluded middle in UU, and the internal LLPO for the family of all sets in UU is weak excluded middle in UU.

The internal versions of the principles of omniscience, like all internal versions of axioms, are weaker than the external version of the principle of omniscience, since while bounded separation implies that one can convert any external predicate xAP(x)x \in A \vdash P(x) on a set AA to an internal predicate {xA|P(x)}A\{x \in A \vert P(x)\} \hookrightarrow A, it is generally not possible to convert an internal predicate to an external predicate without a reflection rule which turns subsingletons in the set theory into propositions in the external logic.

Truncated and untruncated versions in dependent type theory

In the context of dependent 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:

  • Truncated LPO and untruncated LPO are equivalent (due to Martin Escardo, see UFP)

  • Similarly, truncated WLPO and untruncated WLPO are equivalent.

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

  • 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.

Analytic principles of omniscience

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. There are similar axioms in analysis which imply the principles of omniscience for natural numbers, called analytic principles of omniscience, and include the following:

Equivalent statements

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

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

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 Cauchy 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 July 7, 2024 at 23:31:20. See the history of this page for a list of all contributions to it.