Pronouncing "≤" constructively
A type with a relation is partially ordered if it obeys the following rules (reflexivity, transitivity, and antisymmetry):
How are we to pronounce the symbol ? In most contexts, I hear it pronounced as “less than or equal to”; that is, is read as “ is less than or equal to ”. 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 ! That is, we have the implications
but not necessarily the other way around.
That is, if is less than or equal to , then certainly , and if , then is not greater than . 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 as interpreted in Brouwer’s intuitionism.
Another way to read , perhaps in rarer use than the previously mentioned ways, is as “ is at most ”. 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 “ is at most ” 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, ) 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 .