basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
The limited principle of omniscience () states that the existential quantification of any decidable proposition is again decidable. That is,
or equivalently
We have not stated the domain of quantification of the variable . 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 holds, then either the subsingleton is inhabited, in which holds, or the subsingleton is empty, in which holds. Thus, that holds for all subsingletons implies ; conversely, implies (over any domain). However, Bishop's takes the domain to be the set of natural numbers, giving a weaker principle than . (It appears that a realizability topos based on infinite-time Turing machines validates but not ; see Bauer (2011).) Note that propositions of the form when 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 , the limited principle of omniscience for () states that, given any function from to the boolean domain , either is the constant map to or belongs to the image of . Then Bishop's is , which applies to any infinite sequence of bits. Similarly here, if is a subsingleton corresponding to a given truth value and this principle is applied to the constant function at , then the subsingleton is decidable, since if holds, then either the subsingleton is inhabited, in which holds, or the subsingleton is empty, in which holds.
While for is a classic example of the difference between constructive and classical mathematics, holds for the set of extended natural numbers; this is related to the fact that may constructively be given a compact topology. See Escardó (2011) for this and much more.
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 () states that the existential quantification of any decidable proposition on a sete is again decidable. That is,
or equivalently
We can also state the principle set-theoretically, with explicit reference to the domain of quantification. Given a set , the limited principle of omniscience for () states that, given any function from to the boolean domain , either is the constant map to or belongs to the image of . That is,
or equivalently
In the context of dependent type theory, the usual limited principle of omniscience for a type is expressed as
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 , depending on whether the existential quantifier is truncated or untruncated, and whether the disjunction is truncated or untruncated:
holds if and only if the disjunction-untruncated holds.
By the equivalence of the definitions of decidable proposition using inclusive disjunction and exclusive disjunction, the versions of the 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:
The first projection function of the dependent sum types yields a function
meaning that the using exclusive disjunction implies the disjunction-untruncated . Finally, the disjunction-untruncated implies the using inclusive disjunction by the properties of propositional truncations.
Thus, holds if anad only if the disjunction-untruncated holds.
Assuming an arbitrary set ,
holds if and only if for every function from to the natural numbers, either there exists an element in and a natural number such that , or for all elements in , .
holds if and only if the boolean domain is the initial -overt -overt dominance.
Now, let us define an -complete lattice to be a lattice which has all -indexed joins, a lattice with a function
such that for all elements and functions ,
and for all elements and functions , if for all elements , then
and let us define an -frame to be a -complete lattice in which meets distribute over the -indexed joins: for all elements and functions ,
We say that a -frame homomorphism is a lattice homomorphism which also preserves -indexed joins.
holds if and only if the boolean domain is the initial -frame; i.e. the boolean domain is an -frame and for every other -frame , there is a unique -frame homomorphism from the boolean domain to .
When the set is the natural numbers , this yields the familiar theorem that holds if and only if the boolean domain is the initial -frame.
The next statement relate the with the axiom that tight apartness relation on the function set is a decidable tight apartness.
holds if and only if the function set has decidable tight apartness, where the tight apartness relation on the function set be defined as
Given a set , since the boolean domain is a boolean ring, the function set is also a boolean ring via pointwise addition, subtraction and multiplication of boolean-valued functions. Thus, for functions and from to , the tight apartness relation on the function set , defined by
is logically equivalent to , since is logically equivalent to .
Suppose holds. Then for functions and from to , define the function by for all . Then since says that is decidable, and is logically equivalent to , then is decidable.
Conversely, assume that is decidable. Then take to be the constant function at the boolean , and is logically equivalently to and thus . Since is decidable, then is decidable, which is .
The next two statements relate the with axioms that the tight apartness relation on certain other function sets are a decidable tight apartness.
More generally, given a finite set of cardinality , holds if and only if that the function set has decidable tight apartness, where the tight apartness relation on the function set be defined as
holds if and only if the function set has decidable tight apartness, where the tight apartness relation on the function set be defined as
There is a constant function from every subsingleton to the boolean domain taking every element to the boolean .
Given a subsingleton , suppose that holds: either there exists such that , or for all , . Then is a decidable subsingleton.
We prove by case analysis.
Suppose that there exists such that . Then is a inhabited subsingleton and thus a decidable subsingleton.
Then suppose that for all , . Then is empty and thus a decidable subsingleton.
This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.
Suppose that for sets and with decidable tight apartness relations, the tight apartness relation on the function set , defined by , is decidable. Then excluded middle holds.
Every subsingleton has a decidable tight apartness relation where is always false. The boolean domain also has a decidable tight apartness relation where is given by the denial inequality . We proved earlier in the article that is equivalent to the tight apartness relation on the function set being decidable, and implies that every subsingleton is a decidable subsingleton, which is precisely the condition of excluded middle.
There is also a constant function from every subsingleton to the boolean domain taking every element to the boolean .
Given a subsingleton , suppose that either there exists such that , or for all , . Then is a decidable subsingleton.
We prove by case analysis.
Suppose that there exists such that . Then is a inhabited subsingleton and thus a decidable subsingleton.
Then suppose that for all , . Then is empty and thus a decidable subsingleton, since by function extensionality.
This exhausts all options for decidable subsingletons, and exhausts all possible conditions in the hypothesis.
In dependent type theory, given a univalent Tarski universe , one can construct the universe of all types in which satisfy the limited principle of omniscience:
Since the type
is a mere proposition for all , is a sub-universe of .
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 such that for all elements and , .
The internal conjunction of two internal propositions and is the cartesian product of and .
The internal disjunction of two internal propositions and is the image of the unique function from the disjoint union of and to the singleton .
The internal implication of two internal propositions and is the function set between and .
The internal negation of an internal proposition is the function set from to the empty set
An internal proposition is a decidable proposition if it comes with a function from to the boolean domain .
An internal predicate on a set is a set with injection , whose family of propositions indexed by is represented by the preimages .
The internal existential quantifier of an internal predicate is the image of the unique function into the singleton .
Then the internal LPO for a family of sets is the LPO for each stated in the internal logic of the set theory:
or equivalently, as
In particular, the internal LPO for the family of all subsingletons is internal excluded middle. Similarly, given a universe , the internal LPO for the family of all sets in is excluded middle in .
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 on a set to an internal predicate , 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.
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 .
Apart from the equivalent statements stated above for the LPO for a general set , 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 with the usual untruncated version of the .
The implies the disjunction-untruncated .
Given a sequnece of booleans , the preimage of at the boolean has a choice operator.
See Rijke 2022 for a proof of the statement in dependent type theory.
The disjunction-untruncated implies the fully untruncated .
…
and fully untruncated are equivalent.
Next, we have the equivalence of the with the analytic LPO for various notions of real numbers.
The analytic LPO for the following sets of real numbers are equivalent to the LPO for the natural numbers: the Cauchy real numbers , the Escardo-Simpson real numbers/HoTT book real numbers /, and the subfield of Dedekind real numbers which are constructed out of Dedekind cuts valued in the initial -frame .
There are other equivalent statements from real analysis:
Sequential compactness of the unit interval holds if and only if holds.
Every Cauchy real number is a rational number or has an strictly non-repeating base radix expansion if and only if holds.
The Cauchy real numbers are isomorphic to the radix expansion in any base (e.g., a decimal expansion or binary expansion) iff holds.
See Feldman (2010).
Here are a few others:
Every semi-decidable proposition is a decidable proposition if and only if holds.
The -adic integers being a discrete integral domain and the -adic rationals being a discrete field are both equivalent to
The ring of rational power series being a discrete integral domain is equivalent to . Similarly, the Heyting field of rational Laurent series being a discrete field is equivalent to .
There are various other results that are related to the principles of omniscience. Here are a few:
The full bar theorem implies the .
The existence of various classical universes or models of foundations of mathematics implies the :
Any model of bounded Zermelo set theory contains a pure set of real numbers . One can collect all the pure sets of which are in and show that the resulting set is a subset of and a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying for the entire foundations. Thus, the existence of stronger models of material set theory such as ZFC also imply for the entire foundations.
For a similar reason, the existence of a constructively well-pointed Boolean W-topos implies the , since the hom-set , where is the terminal generator and is the real numbers object in , yields a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying for the entire foundations. Thus, the existence of any constructive model of ETCS also implies for the entire foundations.
Finally, in dependent type theory, there being a univalent Tarski universe closed under dependent product types, dependent sum types, and identity types and satisfying the axiom of infinity and excluded middle implies the , since one can construct an element representing the -small type of real numbers, whose type reflection is a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying 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 for the entire type theory.
Note that in all these cases, the real numbers 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.
follows from , but not conversely. If is a decidable proposition, then so is , and so gives
which implies
as is decidable.
follows from , is equivalent to fully untruncated , which implies , and follows from . 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 from . Similarly, Grossack 24 shows that Johnstone’s topological topos separates from . Thus is separated from .
Assuming that Set is a Boolean topos, then (the LPO for natural numbers) holds in any presheaf topos over and indeed in any locally connected topos over , essentially since then 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.
Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)
(in the introduction or chapter 1, I forget)
Hajime Ishihara, Reverse Mathematics in Bishop’s Constructive Mathematics, Philosophia Scientiæ, CS 6 (2006) (doi:10.4000/philosophiascientiae.406, pdf)
Michael Rathjen, Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience. [arXiv:1302.3037]
Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
Auke Booij, Analysis in univalent type theory (2020) [etheses:10411, pdf]
Francesco Ciraulo, -locales in Formal Topology, Logical Methods in Computer Science, Volume 18, Issue 1 (January 12, 2022) (doi:10.46298/lmcs-18%281%3A7%292022, arXiv:1801.09644)
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
Madeleine Birchfield, Andrew Swan (2024) on Category Theory Zulip, LPO and sigma-frame structure on booleans
Chris Grossack, Life in Johnstone’s Topological Topos 3 – Bonus Axioms (web)
Henri Lombardi, Assia Mahboubi, Théories géométriques pour l’algèbre des nombres réels sans test de signe ni axiome de choix dépendant (arXiv:2406.15218)
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.
Andrej Bauer (2011) via constructivenews, An Injection from to (pdf)
Martín Escardó (2011) via constructivenews, Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics (pdf)
Last revised on September 7, 2024 at 11:51:24. See the history of this page for a list of all contributions to it.