nLab limited principle of omniscience

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Constructivism, Realizability, Computability

Contents

Definition

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 the subsingleton is decidable follows, since x,P(x)\forall x, P(x) holds, then either the subsingleton is inhabited, in which x,P(x)\exists x, P(x) holds, or the subsingleton is empty, in which x,¬P(x)\forall x, \neg P(x) holds. Thus, that LPOLPO holds for all subsingletons implies EMEM; 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. Similarly here, if AA is a subsingleton corresponding to a given truth value and this principle is applied to the constant function at 11, then the subsingleton AA is decidable, since if x.f(x)=1\forall x. f(x) = 1 holds, then either the subsingleton is inhabited, in which x.f(x)=1\exists x. f(x) = 1 holds, or the subsingleton is empty, in which x.f(x)=0\forall x.f(x) = 0 holds.

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.

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 (LPOLPO) states that the existential quantification of any decidable proposition on a sete AA is again decidable. That is,

(xA,P(x)̲¬P(x))(xA,P(x))̲¬(xA,P(x)), (\forall x \in A, P(x) \underline{\vee} \neg{P(x)}) \Rightarrow (\exists x \in A, P(x)) \underline{\vee} \neg(\exists x \in A, P(x)) ,

or equivalently

(xA,P(x)̲¬P(x))(x,P(x))̲(x,¬P(x)). (\forall x \in A, P(x) \underline{\vee} \neg{P(x)}) \Rightarrow (\exists x, P(x)) \underline{\vee} (\forall x, \neg{P(x)}) .

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. That is,

f{0,1} A,(xA,f(x)=1)̲¬(xA,f(x)=1), \forall f \in \{0,1\}^A, (\exists x \in A, f(x) = 1) \underline{\vee} \neg(\exists x \in A, f(x) = 1) ,

or equivalently

f{0,1} A,(xA,f(x)=1)̲(xA,f(x)=0). \forall f \in \{0,1\}^A, (\exists x \in A, f(x) = 1) \underline{\vee} (\forall x \in A, f(x) = 0) .

In dependent type theory

In the context of dependent type theory, the usual limited principle of omniscience for a type AA is expressed as

f:A𝟚[[ x:Af(x)=1]+ x:Af(x)=0]\prod_{f:A \to \mathbb{2}} \left[\left[\sum_{x:A} f(x) = 1\right] + \prod_{x:A} f(x) = 0\right]

However, there are in general two ways of interpreting predicate logic, the traditional interpretation using propositional truncations, and the BHK interpretation which do not use propositional truncations. This results in four different versions of the limited principle of omniscience of AA, depending on whether the existential quantifier is truncated or untruncated, and whether the disjunction is truncated or untruncated:

  • the usual LPO A\mathrm{LPO}_A states that
f:A𝟚[[ x:Af(x)=1]+ x:Af(x)=0]\prod_{f:A \to \mathbb{2}} \left[\left[\sum_{x:A} f(x) = 1\right] + \prod_{x:A} f(x) = 0\right]
  • the disjunction-untruncated limited principle of omniscience for AA states that
f:A𝟚([ x:Af(x)=1]+ x:Af(x)=0)\prod_{f:A \to \mathbb{2}} \left(\left[\sum_{x:A} f(x) = 1\right] + \prod_{x:A} f(x) = 0\right)
  • the quantifier-untruncated limited principle of omniscience for AA states that
f:A𝟚[( x:Af(x)=1)+ x:Af(x)=0]\prod_{f:A \to \mathbb{2}} \left[\left(\sum_{x:A} f(x) = 1\right) + \prod_{x:A} f(x) = 0\right]
  • the fully untruncated limited principle of omniscience for AA states that
f:A𝟚(( x:Af(x)=1)+ x:Af(x)=0)\prod_{f:A \to \mathbb{2}} \left(\left(\sum_{x:A} f(x) = 1\right) + \prod_{x:A} f(x) = 0\right)

Theorem

LPO A\mathrm{LPO}_A holds if and only if the disjunction-untruncated LPO A\mathrm{LPO}_A holds.

Proof

By the equivalence of the definitions of decidable proposition using inclusive disjunction and exclusive disjunction, the versions of the LPO A\mathrm{LPO}_A using inclusive and exclusive disjunctions are equivalent to each other.

In dependent type theory, the exclusive disjunction of two types is formulated as the dependent sum type:

A̲B x:A+B y:A+Bx= A+ByA \underline{\vee} B \coloneqq \sum_{x:A + B} \prod_{y:A + B} x =_{A + B} y

The first projection function of the dependent sum types yields a function

π 1:(A̲B)A+B\pi_1:(A \underline{\vee} B) \to A + B

meaning that the LPO A\mathrm{LPO}_A using exclusive disjunction implies the disjunction-untruncated LPO A\mathrm{LPO}_A. Finally, the disjunction-untruncated LPO A\mathrm{LPO}_A implies the LPO A\mathrm{LPO}_A using inclusive disjunction by the properties of propositional truncations.

Thus, LPO A\mathrm{LPO}_A holds if anad only if the disjunction-untruncated LPO A\mathrm{LPO}_A holds.

Properties

LPO for a general set

Assuming an arbitrary set AA,

Theorem

LPO A\mathrm{LPO}_A holds if and only if for every function f:Af:A \to \mathbb{N} from AA to the natural numbers, either there exists an element xx in AA and a natural number nn such that f(x)=n+1f(x) = n + 1, or for all elements xx in AA, f(x)=0f(x) = 0.

Theorem

LPO A\mathrm{LPO}_A holds if and only if the boolean domain is the initial AA-overt \emptyset-overt dominance.

Now, let us define an AA-complete lattice to be a lattice which has all AA-indexed joins, a lattice LL with a function

t:A()(t):(AL)L\bigvee_{t:A} (-)(t):(A \to L) \to L

such that for all elements xAx \in A and functions f:ALf:A \to L,

f(x) t:Af(t)f(x) \leq \bigvee_{t:A} f(t)

and for all elements yLy \in L and functions f:ALf:A \to L, if f(x)yf(x) \leq y for all elements xAx \in A, then

t:Af(t)y\bigvee_{t:A} f(t) \leq y

and let us define an AA-frame to be a AA-complete lattice in which meets distribute over the AA-indexed joins: for all elements xLx \in L and functions f:ALf:A \to L,

a t:Af(t)= t:Aaf(t)a \wedge \bigvee_{t:A} f(t) = \bigvee_{t:A} a \vee f(t)

We say that a AA-frame homomorphism is a lattice homomorphism which also preserves AA-indexed joins.

Theorem

LPO A\mathrm{LPO}_A holds if and only if the boolean domain is the initial AA-frame; i.e. the boolean domain is an AA-frame and for every other AA-frame LL, there is a unique AA-frame homomorphism from the boolean domain to LL.

When the set AA is the natural numbers \mathbb{N}, this yields the familiar theorem that LPO \mathrm{LPO}_\mathbb{N} holds if and only if the boolean domain is the initial σ \sigma -frame.

The next statement relate the LPO A\mathrm{LPO}_A with the axiom that tight apartness relation on the function set 𝟚 A\mathbb{2}^A is a decidable tight apartness.

Theorem

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

f#gxA.f(x)g(x)f \# g \coloneqq \exists x \in A.f(x) \neq g(x)

Proof

Given a set AA, since the boolean domain is a boolean ring, the function set 𝟚 A\mathbb{2}^A is also a boolean ring via pointwise addition, subtraction and multiplication of boolean-valued functions. Thus, for functions ff and gg from AA to 𝟚\mathbb{2}, the tight apartness relation on the function set 𝟚 A\mathbb{2}^A, defined by

f#gx:A.f(x)g(x)f \# g \coloneqq \exists x:A.f(x) \neq g(x)

is logically equivalent to x:A.f(x)g(x)=1\exists x:A.f(x) - g(x) = 1, since f(x)g(x)f(x) \neq g(x) is logically equivalent to f(x)=g(x)+1f(x) = g(x) + 1.

Suppose LPO A\mathrm{LPO}_A holds. Then for functions ff and gg from AA to 𝟚\mathbb{2}, define the function hh by h(x)=f(x)g(x)h(x) = f(x) - g(x) for all xAx \in A. Then since LPO A\mathrm{LPO}_A says that x:A.h(x)=1\exists x:A.h(x) = 1 is decidable, and x:A.h(x)=1\exists x:A.h(x) = 1 is logically equivalent to f#gf \# g, then f#gf \# g is decidable.

Conversely, assume that f#gf \# g is decidable. Then take gg to be the constant function at the boolean 00, and f#λx:A.0f \# \lambda x:A.0 is logically equivalently to x:A.f(x)0=1\exists x:A.f(x) - 0 = 1 and thus x:A.f(x)=1\exists x:A.f(x) = 1. Since f#gf \# g is decidable, then x:A.f(x)=1\exists x:A.f(x) = 1 is decidable, which is LPO A\mathrm{LPO}_A.

The next two statements relate the LPO A\mathrm{LPO}_A with axioms that the tight apartness relation on certain other function sets are a decidable tight apartness.

Theorem

More generally, given a finite set SS of cardinality n>1n \gt 1, LPO A\mathrm{LPO}_A holds if and only if that the function set S AS^A has decidable tight apartness, where the tight apartness relation on the function set S AS^A be defined as

f#gxA.f(x)g(x)f \# g \coloneqq \exists x \in A.f(x) \neq g(x)

Theorem

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

f#gxA.f(x)g(x)f \# g \coloneqq \exists x \in A.f(x) \neq g(x)

LPO for all subsingletons

There is a constant function x1x \mapsto 1 from every subsingleton AA to the boolean domain 𝟚\mathbb{2} taking every element xAx \in A to the boolean 1𝟚1 \in \mathbb{2}.

Theorem

Given a subsingleton AA, suppose that LPO A\mathrm{LPO}_A holds: either there exists xAx \in A such that (x1)(x)=1(x \mapsto 1)(x) = 1, or for all xAx \in A, (x1)(x)=0(x \mapsto 1)(x) = 0. Then AA is a decidable subsingleton.

Proof

We prove by case analysis.

Suppose that there exists x:Ax:A such that (x1)(x)=1(x \mapsto 1)(x) = 1. Then AA is a inhabited subsingleton and thus a decidable subsingleton.

Then suppose that for all x:Ax:A, (x1)(x)=0(x \mapsto 1)(x) = 0. Then AA is empty and thus a decidable subsingleton.

This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.

Theorem

Suppose that for sets AA and BB with decidable tight apartness relations, the tight apartness relation on the function set B AB^A, defined by f#gx:A.f(x)g(x)f \# g \coloneqq \exists x:A.f(x) \neq g(x), is decidable. Then excluded middle holds.

Proof

Every subsingleton AA has a decidable tight apartness relation where x#yx \# y is always false. The boolean domain 𝟚\mathbb{2} also has a decidable tight apartness relation where x#yx \# y is given by the denial inequality xyx \neq y. We proved earlier in the article that LPO A\mathrm{LPO}_A is equivalent to the tight apartness relation on the function set 𝟚 A\mathbb{2}^A being decidable, and LPO A\mathrm{LPO}_A implies that every subsingleton AA is a decidable subsingleton, which is precisely the condition of excluded middle.

There is also a constant function x0x \mapsto 0 from every subsingleton AA to the boolean domain 𝟚\mathbb{2} taking every element xAx \in A to the boolean 0𝟚0 \in \mathbb{2}.

Theorem

Given a subsingleton AA, suppose that either there exists xAx \in A such that (x1)(x)(x0)(x)(x \mapsto 1)(x) \neq (x \mapsto 0)(x), or for all xAx \in A, (x1)(x)=(x0)(x)(x \mapsto 1)(x) = (x \mapsto 0)(x). Then AA is a decidable subsingleton.

Proof

We prove by case analysis.

Suppose that there exists xAx \in A such that (x1)(x)(x0)(x)(x \mapsto 1)(x) \neq (x \mapsto 0)(x). Then AA is a inhabited subsingleton and thus a decidable subsingleton.

Then suppose that for all xAx \in A, (x1)(x)=(x0)(x)(x \mapsto 1)(x) = (x \mapsto 0)(x). Then AA is empty and thus a decidable subsingleton, since (x1)=(x0)(x \mapsto 1) = (x \mapsto 0) by function extensionality.

This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.

Universe of types satisfying LPO

In dependent type theory, given a univalent Tarski universe (U,T)(U, T), one can construct the universe of all types in UU which satisfy the limited principle of omniscience:

U LPO A:U f:T(A)bool(x:T(A).f(x)= bool1)( x:T(A)f(x)= bool0)U_\mathrm{LPO} \coloneqq \sum_{A:U} \prod_{f:T(A) \to \mathrm{bool}} (\exists x:T(A).f(x) =_{\mathrm{bool}} 1) \vee \left(\prod_{x:T(A)} f(x) =_{\mathrm{bool}} 0\right)

Since the type

f:T(A)bool(x:T(A).f(x)= bool1)( x:T(A)f(x)= bool0)\prod_{f:T(A) \to \mathrm{bool}} (\exists x:T(A).f(x) =_{\mathrm{bool}} 1) \vee \left(\prod_{x:T(A)} f(x) =_{\mathrm{bool}} 0\right)

is a mere proposition for all A:UA:U, U LPOU_\mathrm{LPO} is a sub-universe of UU.

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.

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

The internal versions of the limited principles of omniscience, like all internal versions of axioms, are weaker than the external version of the limited 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.

LPO for the natural numbers

The term “limited principle of omniscience”, without any specification of the set for which LPO holds, usually refers to the limited principle of omniscience for the natural numbers LPO \mathrm{LPO}_\mathbb{N}.

Equivalent statements

Apart from the equivalent statements stated above for the LPO for a general set AA, there are various other results that are equivalent specifically to the limited principle of omniscience for the natural numbers.

Let us begin with the equivalence of the various truncated versions of the LPO \mathrm{LPO}_\mathbb{N} with the usual untruncated version of the LPO \mathrm{LPO}_\mathbb{N}.

Theorem

The LPO \mathrm{LPO}_\mathbb{N} implies the disjunction-untruncated LPO \mathrm{LPO}_\mathbb{N}.

Theorem

Given a sequnece of booleans f:𝟚f:\mathbb{N} \to \mathbb{2}, the preimage of ff at the boolean 11 has a choice operator.

Proof

See Rijke 2022 for a proof of the statement in dependent type theory.

Theorem

The disjunction-untruncated LPO \mathrm{LPO}_\mathbb{N} implies the fully untruncated LPO \mathrm{LPO}_\mathbb{N}.

Proof

Theorem

LPO \mathrm{LPO}_\mathbb{N} and fully untruncated LPO \mathrm{LPO}_\mathbb{N} are equivalent.

Next, we have the equivalence of the LPO \mathrm{LPO}_\mathbb{N} with the analytic LPO for various notions of real numbers.

Theorem

The analytic LPO for the following sets of real numbers are equivalent to the LPO for the natural numbers: the Cauchy real numbers C\mathbb{R}_C, the Escardo-Simpson real numbers/HoTT book real numbers E\mathbb{R}_E/ H\mathbb{R}_H, and the subfield of Dedekind real numbers Σ D\mathbb{R}_\Sigma \subseteq \mathbb{R}_D which are constructed out of Dedekind cuts valued in the initial σ \sigma -frame ΣΩ\Sigma \subseteq \Omega.

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

Theorem

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

There are other equivalent statements from real analysis:

Theorem

Sequential compactness of the unit interval holds if and only if LPO \mathrm{LPO}_\mathbb{N} holds.

Theorem

Every Cauchy real number is a rational number or has an strictly non-repeating base bb radix expansion if and only if LPO \mathrm{LPO}_\mathbb{N} holds.

Theorem

The Cauchy real numbers are isomorphic to the radix expansion in any base (e.g., a decimal expansion or binary expansion) iff LPO \mathrm{LPO}_\mathbb{N} holds.

Proof

See Feldman (2010).

Here are a few others:

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

  • The full bar theorem implies the LPO \mathrm{LPO}_\mathbb{N}.

  • The existence of various classical universes or models of foundations of mathematics implies the LPO \mathrm{LPO}_\mathbb{N}:

    • Any model 𝒱\mathcal{V} of bounded Zermelo set theory contains a pure set of real numbers \mathbb{R}. One can collect all the pure sets of 𝒱\mathcal{V} which are in \mathbb{R} and show that the resulting set is a subset of 𝒱\mathcal{V} and a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying LPO \mathrm{LPO}_\mathbb{N} for the entire foundations. Thus, the existence of stronger models of material set theory such as ZFC also imply LPO \mathrm{LPO}_\mathbb{N} for the entire foundations.

    • For a similar reason, the existence of a constructively well-pointed Boolean W-topos \mathcal{E} implies the LPO \mathrm{LPO}_\mathbb{N}, since the hom-set Hom (1,)\mathrm{Hom}_\mathcal{E}(1, \mathbb{R}), where 11 \in \mathcal{E} is the terminal generator and \mathbb{R} \in \mathcal{E} is the real numbers object in \mathcal{E}, yields a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying LPO \mathrm{LPO}_\mathbb{N} for the entire foundations. Thus, the existence of any constructive model of ETCS also implies LPO \mathrm{LPO}_\mathbb{N} for the entire foundations.

    • Finally, in dependent type theory, there being a univalent Tarski universe (U,T)(U, T) closed under dependent product types, dependent sum types, and identity types and satisfying the axiom of infinity and excluded middle implies the LPO \mathrm{LPO}_\mathbb{N}, since one can construct an element :U\mathbb{R}:U representing the UU-small type of real numbers, whose type reflection T()T(\mathbb{R}) is a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying LPO \mathrm{LPO}_\mathbb{N} for the entire type theory. Thus, any univalent Tarski universe which has axiom of choice or a choice operator for the types in the universe also implies LPO \mathrm{LPO}_\mathbb{N} for the entire type theory.

    • Note that in all these cases, the real numbers \mathbb{R} constructed from these universes or classical models of foundations of mathematics, while equivalent to the internal Dedekind real numbers constructed in the universe or model, are not necessarily equivalent to the external Dedekind real numbers in the foundations.

  • WLPO \mathrm{WLPO}_\mathbb{N} follows from LPO \mathrm{LPO}_\mathbb{N}, but not conversely. If P(x)P(x) is a decidable proposition, then so is ¬P(x)\neg{P(x)}, and so LPO \mathrm{LPO}_\mathbb{N} 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.

  • LLPO \mathrm{LLPO}_\mathbb{N} follows from LPO \mathrm{LPO}_\mathbb{N}, WLPO \mathrm{WLPO}_\mathbb{N} is equivalent to fully untruncated LLPO \mathrm{LLPO}_\mathbb{N}, which implies LLPO \mathrm{LLPO}_\mathbb{N}, and WLPO \mathrm{WLPO}_\mathbb{N} follows from LPO \mathrm{LPO}_\mathbb{N}. 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 \mathrm{WLPO}_\mathbb{N} from LLPO \mathrm{LLPO}_\mathbb{N}. Similarly, Grossack 24 shows that Johnstone’s topological topos separates WLPO \mathrm{WLPO}_\mathbb{N} from LLPO \mathrm{LLPO}_\mathbb{N}. Thus LLPO \mathrm{LLPO}_\mathbb{N} is separated from LPO \mathrm{LPO}_\mathbb{N}.

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.

 References

This reference calls the fully untruncated limited principle of omniscience for the natural numbers simply by the term “limited principle of omniscience”. However, the limited principle of omniscience usually refers to the fully truncated version.

These two references call the limited principle of omniscience simply by the term “principle of omniscience” or “omniscience principle”. However, principle of omniscience can refer to multiple possible axioms.

Last revised on September 14, 2024 at 15:17:07. See the history of this page for a list of all contributions to it.