limited principle of omniscience

The limited principle of omniscience states {{harv|Bridges|Richman|1987|p=3}}:

:LPO: For any sequence $a\_0$, $a\_1$, ... such that each $a\_i$ is either $0$ or $1$, the following holds: either $a\_i=0$ for all $i$, or there is a $k$ with $a\_k=1$. {{Cite book|title=A course in constructive algebra|last=Mines|first=Ray|publisher=Springer-Verlag|others=Richman, Fred and Ruitenburg, Wim|year=1988|isbn=0387966404|location=New York|pages=4–5|oclc=16832703}}

The second disjunct can be expressed as $\backslash exists\; k.\; a\_k\; \backslash neq\; 0$ and is constructively stronger than the negation of the first, $\backslash neg\backslash forall\; k.\; a\_k\; =\; 0$. The weak schema in which the former is replaced with the latter is called WLPO and represents particular instances of excluded middle.{{Cite arXiv|eprint=1804.05495|title=Constructive Reverse Mathematics|class=math.LO|last1=Diener|first1=Hannes|year=2020}}

The lesser limited principle of omniscience states:

:LLPO: For any sequence $a\_0$, $a\_1$, ... such that each $a\_i$ is either $0$ or $1$, and such that at most one $a\_i$ is nonzero, the following holds: either $a\_\{2i\}=0$ for all $i$, or $a\_\{2i+1\}=0$ for all $i$.

Here $a\_\{2i\}$ and $a\_\{2i+1\}$ are entries with even and odd index respectively.

It can be proved constructively that the law of the excluded middle implies LPO, and LPO implies LLPO. However, none of these implications can be reversed in typical systems of constructive mathematics.

The term "omniscience" comes from a thought experiment regarding how a mathematician might tell which of the two cases in the conclusion of LPO holds for a given sequence $(a\_i)$. Answering the question "is there a $k$ with $a\_k=1$?" negatively, assuming the answer is negative, seems to require surveying the entire sequence. Because this would require the examination of infinitely many terms, the axiom stating it is possible to make this determination was dubbed an "omniscience principle" by {{harvtxt|Bishop|1967}}.

The two principles can be expressed as purely logical principles, by casting it in terms of decidable predicates on the naturals. I.e. $P$ for which $\backslash forall\; n.\; P(n)\backslash lor\; \backslash neg\; P(n)$ does hold.

The lesser principle corresponds to a predicate version of that De Morgan's law that does not hold intuitionistically, i.e. the distributivity of negation of a conjunction.

Both principles have analogous properties in the theory of real numbers. The analytic LPO states that every real number satisfies the trichotomy or $x\; =\; 0$ or $x\; >\; 0$ . The analytic LLPO states that every real number satisfies the dichotomy $x\; \backslash geq\; 0$ or $x\; \backslash leq\; 0$, while the analytic Markov's principle states that if $x\; \backslash le\; 0$ is false, then $x\; >\; 0$.

All three analytic principles if assumed to hold for the Dedekind or Cauchy real numbers imply their arithmetic versions, while the converse is true if we assume (weak) countable choice, as shown in {{harvtxt|Bishop|1967}}.

• Constructive analysis

• {{cite book |last=Bishop |first=Errett |authorlink=Errett Bishop |date=1967 |title=Foundations of Constructive Analysis |isbn=4-87187-714-0 }}
• {{cite book |last1=Bridges |first1=Douglas |last2=Richman |first2=Fred |date=1987 |title=Varieties of Constructive Mathematics |isbn=0-521-31802-5 }}

• {{SEP|mathematics-constructive|Constructive Mathematics|Douglas Bridges}}

Category:Constructivism (mathematics)

{{mathlogic-stub}}