# Pronouncing "≤" constructively

Posted on May 13, 2016

A type $X$ with a relation $\le : X \to X \to \mathcal{P}$ is partially ordered if it obeys the following rules (reflexivity, transitivity, and antisymmetry):

$\frac{ }{x \le x}$

$\frac{x \le y \qquad y \le z}{x \le z}$

$\frac{x \le y \qquad y \le x}{x = y}$

How are we to pronounce the symbol $\le$? In most contexts, I hear it pronounced as “less than or equal to”; that is, $x \le y$ is read as “$x$ is less than or equal to $y$”. Another alternative that I’ve heard is “not greater than”, which is a bit more concise.

Neither are particular concise for such an important concept, but more egregiously, from a constructive viewpoint, they each mean something different from $\le$! That is, we have the implications

$x < y \vee x = y \quad \Longrightarrow \quad x \le y \quad \Longrightarrow \quad \neg (x > y),$

but not necessarily the other way around.
That is, if $x$ is less than or equal to $y$, then certainly $x \le y$, and if $x \le y$, then $x$ is not greater than $y$. But constructively, each of these implications is potentially strict. For instance, each of these implications is strict for the partial ordering on the real numbers $\mathbb{R}$ as interpreted in Brouwer’s intuitionism.

Another way to read $x \le y$, perhaps in rarer use than the previously mentioned ways, is as “$x$ is at most $y$”. I am surprised it has not caught on, given its concision. Moreover, it doesn’t have the classical bias of the other ones. Particularly, if you are working constructively, I strongly recommend saying “$x$ is at most $y$” rather than the alternatives to avoid the cognitive dissonance of the other phrases to a constructive audience.

There is a preponderance of code abbreviating the relation of a partial order (that is, $\le$) as “le”, including LaTeX, Coq, and many other software tools and programming languages. But we need not perpetuate the mistake! The simple two-letter abbreviation “am”, for “as most”, is a fitting replacement, and its lexicographic neighbor, “al” (“at least”), can be used for $\ge$.