“Less than” in terms of “at most”

"Less than" in terms of "at most"

If, $a$ in the case of comparing reals, $\leq$ is a total order, $<$ is most simply defined by

$x < y \equiv \neg \left( {y \leq x}\right)$

The "transitivity" rule

$a \leq b \land b < c \Rightarrow a < c$

is then a direct consequence of the transi

$$ \begin{array}{l} a \leq b \land b < c \Rightarrow a < c \ = {0, \mathrm {t w i c e} } \ a \leq b \land \neg (c \leq b) \Rightarrow \neg (c \leq a) \ = {\mathrm {s h u n t i n g}, \mathrm {t w i c e} } \ c \leq a \land a < b \Rightarrow c \leq b \ = {\leqslant t r a n s i t i v e } \ t r u e \ \end{array} $$

If $\leq$ is not a total order, this does not work, and I used to use the definition

$x < y \equiv x \leq y \land x \neq y$ (2)

The proof of (1) is then as follows:

$$ \begin{array}{l} a \leq b \land b < c \Rightarrow a < c \ = {(2), \mathrm {t w i c e} } \ a \leq b \land b \leq c \land b \neq c \Rightarrow a \leq c \land a \neq c \ { \leq i s t a n s i t i v e } \ \end{array} $$

$$ \begin{array}{r l} & {a \leq b \land b \leq c \land b \neq c \Rightarrow a \neq c} \ {=} & {{\mathrm {s h u n t i n g , t w i c e} }} \ & {a \leq b \land b \leq c \land a = c \Rightarrow b = c} \ {=} & {{\mathrm {L e i b n i z} }} \ & {c \leq b \land b \leq c \land a = c \Rightarrow b = c} \ {=} & {{\leq \mathrm {r e f l e x i v e} }} \ & {\mathrm {t r u e}} \end{array} $$

In [gs94] "A logical approach to discrete math" by Gries & Schneider - I found the much nicer definition:

$x < y \equiv x \leq y \land !\left( {y \leq x}\right)$

The proof of (1) is now very clear :

$$ \begin{array}{l} \begin{array}{r l} & {a \leq b \land b < c \Rightarrow a < c} \ {=} & {{(3), \mathrm {t w i c e} }} \ & {a \leq b \land b \leq c \land \neg (c \leq b) \Rightarrow a \leq c \land \neg (c \leq a)} \end{array} \ \Leftrightarrow \quad {p r e d. c a l c. } (a \leq b \land b \leq c \Rightarrow a \leq c) \land \ (c \leq a \land a \leq b \Rightarrow c \leq b) \ = { \begin{array}{l} \leq \mathrm {t r a n s i t i v e}, \mathrm {t w i c e} \end{array} } \ \end{array} $$

The moral of the story is that the conjunct $x \neq y$ in (2) is awkward: it forces in general, in one way or another, an appeal to Leibniz, and in this special case also an appeal to the reflexivity of $p$ . Definition (3) is much nicer because it

uses only.

In retrospect I am amazed that I did not come up with (3) myself, for it is a straightforward strengthening of (0), with which I grew up.

Nuenen, 11 August 1994

prof. dr. Edsger W. Dykstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA