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 ($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 may be seen as principles that extend classical logic from predicates (where $EM$ may happen to be valid, even constructively, for certain predicates) to their quantifications over infinite domains (where $EM$ is typically not constructively valid).

Examples

Examples of principles of omniscience include

• limited principle of omniscience, a weak form of excluded middle applied to the existential quantifier for a decidable predicate on a given domain of discourse.

• weak limited principle of omniscience, a weak form of weak excluded middle applied to the existential quantifier for a decidable predicate on a given domain of discourse.

• lesser limited principle of omniscience, a weak form of de Morgan's law applied to the existential quantifier for a decidable predicate on a given domain of discourse.

• Markov's principle, a weak form of the double negation law applied to the existential quantifier for a decidable predicate on a given domain of discourse.

Bishop’s principles of omniscience take the domain of discourse to be the natural numbers. However, it is possible to use some other domain of discourse to get a different principle of omniscience.

There are also the analytic principles of omniscience, which are versions of Bishop’s principles of omniscience that are used in real analysis, including

• analytic LPO

• analytic WLPO

• analytic LLPO

• analytic Markov's principle

In addition, in King 2024 there are more generalizations of the principles of omniscience listed above, which are equivalent to Bishop’s principles of omniscience under the weak countable choice principle $\mathrm{AC}_{\mathbb{N}, 2}$.

There are also generalisations of the principles of omniscience involving inequality spaces:

• Every inequality space has decidable tight apartness, which generalises LPO and analytic LPO. In the presence of function sets, this is equivalent to excluded middle.

• Every inequality space has decidable equality, which generalises WLPO and analytic WLPO. In the presence of function sets, this is equivalent to weak excluded middle.

• Every inequality space has stable tight apartness, which generalises Markov's principle and analytic Markov's principle. In the presence of function sets, this is equivalent to the double negation law.

References

• Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)

  (in the introduction or chapter 1, I forget)

• Fred Richman, Polynomials and linear transformations. Linear Algebra and its Applications, Volume 131, 1 April 1990, Pages 131-137. [doi:10.1016/0024-3795(90)90379-Q]

• Christopher King, What are these generalizations of the principles of omniscience called?, MathOverflow, 15 February 2024. (web)

category: disambiguation