analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
basic constructions:
strong axioms
further
In real analysis, there is a principle on the Cauchy real numbers which is equivalent in strength to the limited principle of omniscience for natural numbers, and states that the pseudo-order on the Cauchy real numbers is a decidable relation, or that the Cauchy real numbers have decidable tight apartness. This principle can be generalised from the Cauchy real numbers to all notions of real numbers, such as the Dedekind real numbers, and is hence called the analytic limited principle of omniscience, or the analytic LPO. In classical mathematics, all of these are implied by excluded middle; however, in neutral constructive mathematics, the different analytic LPO are different principles of different strength, because the Cauchy and Dedekind real numbers and any other notion of real numbers between the Cauchy and Dedekind real numbers cannot be proven to coincide.
There are many different notions of real numbers in constructive mathematics. What all these real numbers have in common are that they are an Archimedean ordered field extension of the field of (sequential, modulated) Cauchy real numbers ; i.e. there are unique ring homomorphisms of ordered fields
where is the ordered field of Dedekind real numbers - the homomorphism into always exists since is the terminal Archimedean ordered field. In general the ring homomorphisms are not provably isomorphisms unless the Dedekind real numbers and Cauchy real numbers coincide. Thus, there are many different notions of the analytic limited principle of omniscience; the analytic limited principles of omniscience are defined for each Archimedean ordered field extension of the Cauchy real numbers.
Let be an Archimedean ordered field extension of the field of (sequential, modulated) Cauchy real numbers . The analytic LPO for states that the usual apartness relation on decidable ( or ), or equivalently trichotomy for ( or or ), or equivalently, that is a discrete field.
Warning. Given an Archimedean ordered field extension of the field of (sequential, modulated) Cauchy real numbers, the analytic limited principle of omniscience for is not to be confused with the limited principle of omniscience for - the latter is the statement that for every function from to the boolean domain, either there exists an element in such that , or for all elements in , . For the Cauchy real numbers, the analytic LPO for the Cauchy real numbers is equivalent to the LPO for the natural numbers, while the LPO for the Cauchy real numbers is much stronger than the LPO for the natural numbers.
Let be any Archimedean ordered field extension of the Cauchy real numbers. The analytic LPO also makes sense for any Archimedean ordered local Artinian -algebra as well, where the relation is in general only a strict weak order instead of a pseudo-order, the preorder is not a partial order, and the equivalence relation derived from the preorder holds if and only if is nilpotent. In this case, the analytic LPO for the Weil -algebra says that the strict weak order on is a decidable relation, or that the apartness relation is a decidable relation, or invertibility is decidable, and the quotient of by its nilradical is the field of real numbers satisfying the analytic LPO.
The analytic LPO for the (sequential, modulated) Cauchy real numbers implies the LPO for natural numbers.
Let be a function from the natural numbers to the boolean domain. Define the sequence on the rationals as
This sequence is a Cauchy sequence with a modulus of continuity, so taking the limit of this Cauchy sequence yields a Cauchy real number . The analytic LPO on the Cauchy reals states that either or . In the former case, for some natural number so there exists an such that , and in the latter case, for all . Thus, the LPO for natural numbers hold.
Suppose that there is an Archimedean ordered field which is a field extension of the Cauchy real numbers . Then the analytic LPO for implies that is isomorphic to
Every Archimedean ordered field is a subfield of the Dedekind real numbers, which means that by coercion one can consider the elements of any Archimedean ordered field to be Dedekind real numbers, which are Dedekind cuts. Theorem 10.6.3 of Booij 2020 says that any Dedekind real number (i.e. Dedekind cut) for which there exists a locator is a Cauchy real number. This implies that given an Archimedean ordered field , if for every element in there exists a locator, then every element in is a Cauchy real number, and is a subfield of the Cauchy real numbers. If is also a field extension of the Cauchy real numbers, then is isomorphic to the Cauchy real numbers, since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms in the category of Archimedean ordered fields.
The analytic LPO implies that corollary 11.4.3 of UFP 2013 can be proven: If analytic LPO holds then “ can be proved: either or . In the former case we are done, while in the latter we get because .” Therefore, we get a locator for every element of , which then implies that is isomorphic to the Cauchy real numbers.
Suppose that there are two Archimedean ordered fields and such that both are field extensions of the Cauchy real numbers and is a field extension of . Then, the analytic LPO for implies the analytic LPO for .
Analytic LPO for implies that is isomorphic to the Cauchy real numbers, which implies that any subfield of which is a field extension of the Cauchy real numbers is isomorphic to , since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms in the category of Archimedean ordered fields. Since this is true of , this implies that the analytic LPO for also holds, since and are isomorphic fields.
Suppose that there is an Archimedean ordered field which is a field extension of the Cauchy real numbers . Then, the analytic LPO for implies the LPO for natural numbers.
Since the field of Cauchy real numbers is a (trivial) field extension of itself, the analytic LPO for implies the analytic LPO for the Cauchy real numbers, which implies the LPO for the natural numbers.
Let be the initial -frame. It is a sub--frame of the frame of truth values. One can construct a set of Dedekind real numbers out of Dedekind cuts in valued in the initial -frame (see section 11.2 of UFP 2013), where then one has ring homomorphisms
The LPO for natural numbers is equivalent to the boolean domain being the initial -frame .
…
Thus, one can use the decidable Dedekind cuts to construct the Dedekind real numbers, since is the initial -frame.
The LPO for natural numbers implies the analytic LPO for subset of Dedekind real numbers constructed out of Dedekind cuts in valued in the initial -frame .
LPO for the natural numbers implies that for each rational number , the left and right Dedekind cuts for an element of , evaluated at , and , are both decidable propositions. In addition, LPO for the natural numbers implies that any existential quantification of a decidable predicate over the rational numbers is itself a decidable proposition. The pseudo-order relation on is defined as
Since and are both decidable, the conjunction is also decidable, and so is the existential quantifier by LPO for the natural numbers, and by definition the strict order on , which is the analytic LPO for .
The LPO for natural numbers, the -analytic LPO, and the -analytic LPO are equivalent to each other.
We showed that the the -analytic LPO implies the LPO for natural numbers, that the -analytic LPO implies the -analytic LPO, and the LPO for natural numbers implies the -analytic LPO. By transitivity of implication, the converses also hold, so all three statements are equivalent to each other.
Suppose that there is an Archimedean ordered field which is a field extension of the Cauchy real numbers . Then the analytic LPO for implies that is equivalent to and .
Analytic LPO for implies the LPO for natural numbers, which implies that is equivalent to . Theorem 11.2.14 in UFP 2013 states that given the initial -frame , every Archimedean ordered field which is admissible for is a subfield of . The LPO for natural numbers implies the initial -frame is the boolean domain, which means that analytic LPO for implies that is admissible for the boolean domain, and hence a subfield of . This means that coincides with both and , since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms.
Suppose that there is an Archimedean ordered field which is a field extension of the Cauchy real numbers . Then the analytic LPO for implies that is sequentially Cauchy complete.
Analytic LPO for implies that is equivalent to . Since is constructed out of Dedekind cuts (valued in the initial -frame ), theorem 11.2.12 and corollary 11.2.13 of UFP 2013 states that is sequentially Cauchy complete, which then implies that is sequentially Cauchy complete.
Finally, let be the HoTT book real numbers, which are the initial sequentially Cauchy complete Archimedean ordered field. Then,
The LPO for natural numbers and the analytic LPO for are equivalent to each other.
There is a ring homomorphism because is Cauchy complete and is initial in the category of Cauchy complete Archimedean ordered fields, and there is a ring homomorphism because the rational numbers are a subset of , and is the limit of Cauchy sequences of rational numbers (with modulus), while is the limit of Cauchy sequences of elements of , implying that embeds in .
Since the LPO for natural numbers is equivalent to the analytic LPO for , this in turn implies that and are isomorphic fields, which implies that is isomorphic to , since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms in the category of Archimedean ordered fields. Thus, the analytic LPO for is equivalent to the analytic LPO for and equivalent to the LPO for natural numbers.
Thus, one has a hierarchy of analytic limited principles of omniscience, where
The analytic LPO for the (sequential, modulated) Cauchy real numbers, for the Escardo-Simpson real numbers/HoTT book real numbers, and for the subset of the Dedekind real numbers whose Dedekind cuts are valued in the initial -frame, are all the weakest and equivalent to the LPO for the natural numbers;
The analytic LPO for the Dedekind real numbers is the strongest.
For any other Archimedean ordered field extension of the Cauchy real numbers which is neither equivalent to the Cauchy real numbers or the Dedekind real numbers, the analytic LPO for are intermediate in strength between the Cauchy-analytic LPO and the Dedekind-analytic LPO.
Given an Archimedean ordered field extension of the Cauchy real numbers, there are other statements related to the analytic LPO for :
That the floor and ceiling partial functions are total functions on is equivalent to the analytic LPO for .
That coincides with the prealgebra real numbers is equivalent to the analytic LPO for .
The analytic for implies the fundamental theorem of algebra for .
That every apartness relation on a set is decidable implies that analytic LPO for :
The analytic LPO for both Cauchy real numbers and Dedekind real numbers fails in Johnstone’s topological topos, since it contradicts Brouwer's continuity principle which holds for both the Cauchy real numbers and the Dedekind real numbers.
The analytic LPO for Dedekind real numbers fails in the cohesive types of Mike Shulman‘s real-cohesive homotopy type theory, which model Euclidean-topological infinity-groupoids, since it contradicts Brouwer's continuity principle which holds for the Dedekind real numbers. However, the analytic LPO for Cauchy real numbers holds in the cohesive types, since the LPO for natural numbers hold and is equivalent to the analytic LPO for Cauchy real numbers.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke Booij, Analysis in Univalent Type Theory (2020) [etheses:10411, pdf, pdf]
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)
The phrase “analytic LPO” is mentioned in the following paper, although in that paper it actually refer to the analytic WLPO (the reals have decidable equality) instead of the actual analytic LPO (the reals have decidable tight apartness). In addition, it makes the wrong statement that LPO is equivalent to Cauchy reals having decidable equality; it is WLPO which is equivalent to Cauchy reals having decidable equality (i.e. analytic WLPO for Cauchy reals), while LPO is equivalent to Cauchy reals having decidable tight apartness.
Last revised on August 20, 2024 at 22:47:36. See the history of this page for a list of all contributions to it.