The Archimedean property states that every positive element in a strictly weakly ordered cancellative commutative monoid is bounded above by a natural number.

So an object satisfying the Archimedean property has no infinite elements. If the strict weak order is additionally a connected relation and thus a pseudo-order, every infinitesimal element is equal to zero.

Let $(\mathbb{N}^+,1:\mathbb{N}^+,s:\mathbb{N}^+\to \mathbb{N}^+)$ be the set of positive integers.

Let $(A,\lt, +, 0)$ be a strictly ordered cancellative commutative monoid. The positive integers are embedded into the function monoid $A \to A$; there is an injection $inj:\mathbb{N}^+\to (A \to A)$ such that $inj(1) = id_A$ and $inj(s(n)) = inj(n) + id_A$ for all $n:\mathbb{N}^+$.

The **archimedean property** states that for every $a,b:A$ such that $0 \lt a$ and $0 \lt b$, then there exist $n:\mathbb{N}^+$ such that $a \lt inj(n)(b)$.

By uncurrying $inj$ one gets an action $act: (\mathbb{N}^+\times A) \to A$ such that $act(1,a) = a$ and $act(s(n),a) = act(n,a) + a$ for all $n:\mathbb{N}^+$ and $a:A$. The archimedean property then states that for all $a,b:A$ such that $0 \lt a$ and $0 \lt b$, there exist $n:\mathbb{N}^+$ such that $a \lt act(n,b)$.

For ordered fields $F$, since $\mathbb{Q}$ is the initial ordered field, there exists a unique ordered field homomorphism $i:\mathbb{Q} \to F$ for all ordered fields $F$. Then the **archimedean property** for $F$ states that the rational numbers are dense in $F$:

- for all $x \in F$ and $y \in F$ such that $x \lt y$, there exists a rational number $q:\mathbb{Q}$ such that $x \lt i(q) \lt y$.

In dependent type theory, both definitions of the usual archimedean property above use the phrase “there exists…”. This existence in the definitions is mere existence; i.e. using the existential quantifier rather than the dependent sum type. The untruncated version of the archimedean property using dependent sum types can be called **archimedean structure**.

Archimedean structure for strictly ordered cancellative commutative monoids $(A,\lt, +, 0)$ using the positive natural numbers says that

- for every $x:A$, $y:A$ such that $0 \lt x$ and $0 \lt y$, then there exist as structure a positive natural number $n:\mathbb{N}^+$ such that $x \lt \mathrm{inj}(n)(y)$.

$\prod_{x:A} \prod_{y:A} (0 \lt x) \times (0 \lt y) \to \sum_{n:\mathbb{N}^+} x \lt \mathrm{inj}(n)(y)$

Defining the type of positive elements in $A$ as $A^+ \coloneqq \sum_{x:A} 0 \lt x$, by uncurrying and using the type theoretic axiom of choice, one gets the equivalent statement

$\prod_{x:A^+} \prod_{y:A^+} \sum_{n:\mathbb{N}^+} x \lt \mathrm{inj}(n)(y)$

which by the type theoretic axiom of choice is the same as saying that

- there exists as structure a function $M:(A^+ \times A^+) \to \mathbb{N}^+$ such that for every $x:A^+$ and $y:A^+$, $x \lt \mathrm{inj}(M(x, y))(y)$

$\sum_{M:(A^+ \times A^+) \to \mathbb{N}^+} \prod_{x:A^+} \prod_{y:A^+} x \lt \mathrm{inj}(M(x, y))(y)$

These functions can be called the **archimedean modulus** in parallel to the modulus of convergence and modulus of continuity which are defined for the untruncated versions of the definitions of Cauchy sequence and continuous function.

Similarly, archimedean structure for ordered fields states that

- for all $x:F$ and $y:F$ such that $x \lt y$, there exists as structure a rational number $q:\mathbb{Q}$ such that $x \lt i(q) \lt y$.

$\prod_{x:F} \prod_{y:F} x \lt y \to \sum_{q:\mathbb{Q}} (x \lt i(q)) \times (i(q) \lt y)$

One could construct archimedean structure for any Archimedean ordered field where every element has a locator. See lemma 6.7.3 of Booij20.

In particular, one could construct archimedean structure for any Archimedean ordered field satisfying trichotomy, that for all $x:F$ and $y:F$, exactly one of $x \gt y$, $x \lt y$, $x = y$ is true.

Suppose the Archimedean ordered field $F$ satisfies trichotomy. Then, the ceiling $x \mapsto \lceil x \rceil$ and floor $x \mapsto \lfloor x \rfloor$ are well defined functions over the entire domain of $F$. By definition of the ceiling and the fact that $x \lt y$, we have that

$\left\lceil\frac{2}{y - x}\right\rceil \geq \frac{2}{y - x}$

and thus

$\left\lceil\frac{2}{y - x}\right\rceil (y - x) = \left\lceil\frac{2}{y - x}\right\rceil y - \left\lceil\frac{2}{y - x}\right\rceil x \geq 2$

so we have

$\left\lceil\frac{2}{y - x}\right\rceil x \lt \frac{\left\lceil \left\lceil\frac{2}{y - x}\right\rceil x \right\rceil + \left\lfloor \left\lceil\frac{2}{y - x}\right\rceil y \right\rfloor}{2} \lt \left\lceil\frac{2}{y - x}\right\rceil y$

Since $x \lt y$, $0 \lt \left\lceil\frac{2}{y - x}\right\rceil$, and so it is possible to divide all sides by $\left\lceil\frac{2}{y - x}\right\rceil$ and keep the elements in the inequality in order.

$x \lt \frac{\left\lceil \left\lceil\frac{2}{y - x}\right\rceil x \right\rceil + \left\lfloor \left\lceil\frac{2}{y - x}\right\rceil y \right\rfloor}{2 \left\lceil\frac{2}{y - x}\right\rceil} \lt y$

Thus, if the Archimedean ordered field satisfies trichotomy, then the Archimedean ordered field has Archimedean structure. In classical mathematics, as well as in constructive mathematics in which the analytic LPO for the terminal Archimedean ordered field is true, every Archimedean ordered field has Archimedean structure.

- Archimedean group
- Archimedean ordered field
- Archimedean ordered integral domain
- Archimedean ordered local ring

- Wikipedia,
*Archimedean property*

The alternative definition of the Archimedean property for ordered fields using the rational numbers is defined in section 11.2.1 of

and in section 4.3 of

- Auke Booij,
*Analysis in univalent type theory*(2020) $[$etheses:10411, pdf$]$

Last revised on January 21, 2024 at 15:49:19. See the history of this page for a list of all contributions to it.