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
…
…
A locator for a real number $c \in \mathbb{R}$ is an element of the indexed cartesian product
where $A \uplus B$ is the disjoint union of two sets $A$ and $B$, $B^A$ is the set of functions from $A$ to $B$, $[A]$ is the support of $A$, and the indexed cartesian product is defined in set theory as
for family of sets $(B(a))_{a \in A}$.
Equivalently, a locator is an element of the indexed cartesian product
Given a dense linear order $(A, \lt_A)$, the open interval in $A$ between elements $a \in A$ and $b \in B$ is the set
Given a countable dense linear order $(B, \lt_B)$ such that $B \subseteq A$ and for all elements $a \in A$ and $b \in A$ where $a \lt b$, there exists $c \in B$ such that $a \lt c \lt b$, a $B$-indexed locator for an element $c \in A$ is an element of the indexed cartesian product
In dependent type theory, given a real number $r:\mathbb{R}$, a locator on the Dedekind real numbers is a dependent function
This above type is equivalent to the types
A locator is equivalent to having the structure of a Cauchy sequence with modulus of convergence. This is stronger than merely being a modulated Cauchy real number.
That every Dedekind real number has a $\mathbb{Q}$-indexed locator implies the weak limited principle of omniscience.
Note: The “principle of locators” or “axiom of locators” are placeholder names for a principle or axiom which may or may not have an already existing name in the mathematics literature.
The principle of locators state that every real number $x:\mathbb{R}$ merely has a locator (i.e. the support of the locator has an element), and implies that the Cauchy real numbers is the terminal Archimedean ordered field, and coincides with the Dedekind real numbers. This is true in classical mathematics, as is in constructive mathematics which also uses countable choice.
However, in general constructive mathematics, while theorem 6.10.3 of Booij 2020 states that a real number is a Cauchy real number if and only if it merely has a locator, not every real number is necessarily a Cauchy real number, so it is not necessarily true that every real number has a locator. In that case, this principle becomes the axiom of locators, which says that every element $x:\mathbb{R}$ of the terminal Archimedean ordered field $\mathbb{R}$ merely has a locator, making it coincide with the Cauchy real numbers. We use terminal Archimedean ordered field since in predicative mathematics the Dedekind real numbers may not exist.
Auke Booij, Analysis in univalent type theory (2020) $[$etheses:10411, pdf$]$
Steve Vickers, Locators point-free (pdf)
Last revised on February 13, 2024 at 01:56:07. See the history of this page for a list of all contributions to it.