nLab locator




In the real numbers

A locator for a real number cc \in \mathbb{R} is an element of the indexed cartesian product

l a b([{d|a<d<c}][{d|c<d<b}]) [{d|a<d<b}]l \in \prod_{a \in \mathbb{Q}} \prod_{b \in \mathbb{Q}} \left([\{d \in \mathbb{R} \vert a \lt d \lt c\}] \uplus [\{d \in \mathbb{R} \vert c \lt d \lt b\}]\right)^{[\{d \in \mathbb{R} \vert a \lt d \lt b\}]}

where ABA \uplus B is the disjoint union of two sets AA and BB, B AB^A is the set of functions from AA to BB, [A][A] is the support of AA, and the indexed cartesian product is defined in set theory as

aAB(a)={f( aAB(a)) A|a,f(a)B(a)}\prod_{a \in A} B(a) = \{f \in \left(\bigcup_{a\in A} B(a)\right)^A \vert \forall a, f(a) \in B(a) \}

for family of sets (B(a)) aA(B(a))_{a \in A}.

Equivalently, a locator is an element of the indexed cartesian product

l a b[{d|a<d<c}] [{d|a<d<b}]×[{d|c<d<b}] [{d|a<d<b}]l \in \prod_{a \in \mathbb{Q}} \prod_{b \in \mathbb{Q}} [\{d \in \mathbb{R} \vert a \lt d \lt c\}]^{[\{d \in \mathbb{R} \vert a \lt d \lt b\}]} \times [\{d \in \mathbb{R} \vert c \lt d \lt b\}]^{[\{d \in \mathbb{R} \vert a \lt d \lt b\}]}

In arbitrary dense linear orders

Given a dense linear order (A,< A)(A, \lt_A), the open interval in AA between elements aAa \in A and bBb \in B is the set

OpenInt(a,b)={cA|a<c<b}\mathrm{OpenInt}(a,b) = \{c \in A \vert a \lt c \lt b\}

Given a countable dense linear order (B,< B)(B, \lt_B) such that BAB \subseteq A and for all elements aAa \in A and bAb \in A where a<ba \lt b, there exists cBc \in B such that a<c<ba \lt c \lt b, a BB-indexed locator for an element cAc \in A is an element of the indexed cartesian product

l aB bB([OpenInt(a,c)][OpenInt(c,b)]) [OpenInt(a,b)]l \in \prod_{a \in B} \prod_{b \in B} \left([\mathrm{OpenInt}(a,c)] \uplus [\mathrm{OpenInt}(c,b)]\right)^{[\mathrm{OpenInt}(a,b)]}

In dependent type theory

In dependent type theory, given a real number r:r:\mathbb{R}, a locator on the Dedekind real numbers is a dependent function

l: p: q:(p<q)((p<r)+(r<q))l:\prod_{p:\mathbb{Q}} \prod_{q:\mathbb{Q}} (p \lt q) \to ((p \lt r) + (r \lt q))

This above type is equivalent to the types

p: q:(p<q) b:bool((b=1)(p<r))×((b=0)(r<q))\prod_{p:\mathbb{Q}} \prod_{q:\mathbb{Q}} (p \lt q) \to \sum_{b:\mathrm{bool}} ((b = 1) \to (p \lt r)) \times ((b = 0) \to (r \lt q))
p: q:(p<q) b:bool((b=0)(p<r))×((b=1)(r<q))\prod_{p:\mathbb{Q}} \prod_{q:\mathbb{Q}} (p \lt q) \to \sum_{b:\mathrm{bool}} ((b = 0) \to (p \lt r)) \times ((b = 1) \to (r \lt q))


Principle of locators

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: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: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.


Last revised on February 13, 2024 at 01:56:07. See the history of this page for a list of all contributions to it.