Read-back: the existence of a two-sided invariant total order

This is a rendering, in ordinary mathematical language, of exactly what one declaration asserts. Everything the declaration depends on is expanded here, so that the reader need not consult the source. The declaration takes no arguments of any kind — no universally quantified data, no hidden (implicit) arguments and no structural assumptions. It is a single closed assertion.

The objects involved

The interval. Let

$$I \;=\; [0,1] \;=\; \{t \in \mathbb{R} : 0 \le t \le 1\},$$

regarded as an ordered set with the order it inherits from $\mathbb{R}$: for $x, y \in I$ one has $x \le y$ exactly when the corresponding real numbers satisfy $x \le y$.

The maps. By an order isomorphism of $I$ is meant a bijection $f : I \to I$ such that for all $x, y \in I$,

$$x \le y \quad\Longleftrightarrow\quad f(x) \le f(y).$$

That is the whole requirement: a bijection of $I$ onto itself which, together with its inverse, preserves the order. No continuity, differentiability or piecewise structure is part of this notion, and no topology on $\mathbb{R}$ enters. Write $\mathrm{Aut}(I)$ for the set of all order isomorphisms of $I$.

The group law. $\mathrm{Aut}(I)$ is a group under composition, with the convention

$$(f \cdot g)(x) \;=\; f\bigl(g(x)\bigr) \qquad \text{for all } x \in I,$$

so that in a product the right-hand factor acts first. The identity element is the identity map of $I$, and the inverse of $f$ is the inverse bijection $f^{-1}$.

Dyadic numbers. A real number $x$ is called dyadic here if

$$x \;=\; \frac{m}{2^{k}} \quad\text{for some integer } m \in \mathbb{Z} \text{ and some natural number } k \in \mathbb{N}.$$

The exponent $k = 0$ is allowed, so every integer — positive, negative or zero — is dyadic, and $m$ is an arbitrary integer, so the dyadic numbers here are exactly the usual dyadic rationals (including those outside $[0,1]$).

The piecewise-linearity condition. Say that an order isomorphism $f$ of $I$ is of Thompson type if the following holds:

There exists a finite set $B \subseteq \mathbb{R}$, every element of which is dyadic, such that for all $x, y \in I$ with $x < y$ and

$$(x,y) \cap B \;=\; \varnothing,$$

there exist an integer $n \in \mathbb{Z}$ and a real number $c \in \mathbb{R}$ with

$$f(z) \;=\; 2^{n} z + c \qquad \text{for every } z \in I \text{ with } x \le z \le y .$$

Several features of this condition are worth spelling out, because the quantifiers include them silently.

• The slope $2^{n}$ ranges over the integer powers of two, negative exponents included and read as genuine reciprocals ($2^{-1} = 1/2$, $2^{-3} = 1/8$); every such slope is positive.
• The intercept $c$ is an arbitrary real number. Nothing in this condition requires the intercepts to be dyadic; only the elements of $B$ are required to be dyadic.
• The set $B$ is a finite set of real numbers, not required to lie inside $[0,1]$ and not required to be non-empty. The empty set is a permitted choice of $B$, in which case the displayed requirement applies to every pair $x < y$ in $I$.
• The set $B$ is required to miss only the open interval $(x,y)$; the endpoints $x$ and $y$ themselves may belong to $B$. The affine formula, by contrast, is asserted on the closed interval, i.e. at the endpoints as well as inside.
• The exponent $n$ and the intercept $c$ are chosen after $x$ and $y$, so they may differ from one such interval to another; the condition does not assert a single global formula.
• The numbers $x$ and $y$ are quantified over the points of $I$ only, so the condition never tests intervals reaching outside $[0,1]$.

The group $F$. Let $\mathcal{T} \subseteq \mathrm{Aut}(I)$ be the set of all order isomorphisms of $I$ that are of Thompson type in the above sense, and let

$$F \;=\; \text{the subgroup of } \mathrm{Aut}(I) \text{ generated by } \mathcal{T},$$

that is, literally, the intersection of all subgroups of $\mathrm{Aut}(I)$ that contain $\mathcal{T}$ — equivalently, the set of all maps expressible as a composite of finitely many elements of $\mathcal{T}$ and inverses of elements of $\mathcal{T}$.

Note that this is a generated subgroup: nothing here asserts that $\mathcal{T}$ is already closed under composition and inversion, and consequently an element of $F$ is not, on the strength of anything said here, itself of Thompson type. $F$ is a group, and it contains the identity map of $I$, so it is non-empty. In what follows, "element of $F$" means a member of that group, and the product $ab$ of two elements of $F$ is their composite in $\mathrm{Aut}(I)$, again an element of $F$.

What the declaration asserts

There exists a linear order on the set of elements of $F$ — call the relation $\preceq$ — such that for all elements $a$, $b$, $c$ of $F$:

$$a \preceq b \quad\Longrightarrow\quad \bigl(\, c a \preceq c b \ \ \textbf{and}\ \ > a c \preceq b c \,\bigr).$$

Here linear order means a relation $\preceq$ on the elements of $F$ that is

• reflexive: $a \preceq a$ for all $a$;
• transitive: $a \preceq b$ and $b \preceq c$ imply $a \preceq c$;
• antisymmetric: $a \preceq b$ and $b \preceq a$ imply $a = b$ (equality of elements of $F$, i.e. equality of the underlying maps of $I$);
• total: for all $a, b$, either $a \preceq b$ or $b \preceq a$.

The following points of logical form are part of the assertion and should not be rounded off.

• The order is existentially quantified, and it is otherwise arbitrary. The assertion is only that some such relation exists. No relationship is required between $\preceq$ and any order on the maps themselves — in particular $\preceq$ need not be the pointwise comparison $a(x) \le b(x)$, nor any order canonically attached to $F$. It is simply some total order on the underlying set of $F$.
• The invariance is an implication, not an equivalence. What is asserted is that $a \preceq b$ implies $ca \preceq cb$ and $ac \preceq bc$; the converse implications are not part of the statement.
• Both sides at once, with one order. The same single relation $\preceq$ is required to be compatible with multiplication on the left and on the right; the conclusion is a conjunction of the two comparisons, not a disjunction, and not two separate orders.
• The three elements are quantified independently over all of $F$, with no further hypotheses on them; in particular $c$ ranges over every element of $F$, including the identity, and $a$, $b$, $c$ need not be distinct.
• Product order. Because a product means "apply the right factor first", $ca$ is the map $x \mapsto c(a(x))$ and $ac$ is the map $x \mapsto a(c(x))$. (The condition as a whole is symmetric in the two sides, so it makes the same demand whichever composition convention a reader has in mind, but the individual conjuncts are as just described.)
• Strict inequality is not mentioned. The statement is phrased entirely with the non-strict relation $\preceq$; no claim about $\prec$ appears, and no claim that the order is non-trivial, dense, discrete, or anything else.
• Nothing is asserted about uniqueness. It is an "there exists", not a "there exists exactly one"; and nothing is said about how many such orders there are or how they are related.

One further piece of fine print: what "a linear order" carries

In the formal system used, "a linear order on a type" is a bundled structure, not merely a relation. Besides the relation $\preceq$ and the four axioms above, such a structure also carries:

• a strict relation $\prec$, tied to $\preceq$ by the requirement that $a \prec b$ hold exactly when $a \preceq b$ and not $b \preceq a$;
• binary minimum and maximum operations, required to agree with the order (the minimum of $a$ and $b$ is $a$ if $a \preceq b$ and $b$ otherwise, and dually for the maximum);
• a three-valued comparison function, required to agree with $\prec$ and equality;
• decision procedures for the relations $\preceq$ and $\prec$ and for equality of elements — that is, effective data resolving each comparison, not merely the classical fact that each comparison holds or fails.

So the existential quantifier of the declaration ranges over such packages, and asserts that one of them exists whose relation $\preceq$ satisfies the two-sided invariance displayed above. The invariance condition constrains only the relation $\preceq$; the remaining components are constrained only by their own coherence requirements just listed.