An alternative of the ETAC to EWD1163

About relation

(0) $\left\langle {\forall x,y : x = y \equiv x \leq y \land y \leq x}\right\rangle$ (1) $\left\langle {\forall x,y : \left\langle {\exists w : \left\langle {\forall z : w \leq z \equiv x \leq z \land y \leq z}\right\rangle }\right\rangle }\right\rangle$

Remark (0) is equivalent to the statement that $\leq$ is reflexive $(\Rightarrow)$ and antisymmetric $(\Leftarrow)$ ; it implies that the $w$ in (1) is unique. In contrast to EWDI163, the argument of the ETAC, reported below, does not use this uniqueness. (End of Remark.)

We are invited to prove that $\leq$ is transitive.

The most common way of expressing monotonicity is

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

shunting gives the (not uncommon)

$$ a \leq b \Rightarrow (b \leq c \Rightarrow a \leq c), $$

which has the advantage that the universal quantification over $c$ can be localized to the consequent, which is attractive in view of (1). The ETAC decided to formu

late the demonstrandum

$$ (2) \quad a \leq b \Rightarrow \langle \forall c: b \leq c \Rightarrow a \leq c \rangle \quad f o r a n y a, b. $$

The proof is constructed by designing a strengthening chain from (2)'s consequent to its antecedent. Given (1) is exploited by introducing, for the $a,b$ under consideration, a w satisfying

$$ (3) \quad \langle \forall c: w \leqslant c \equiv a \leqslant c \land b \leqslant c \rangle . $$

The pivot of the calculation is its only intrinsically weakening step, viz. an appeal to Leibniz's Principle, which is used to eliminate the universal quantification. Prior to that pivotal step, (3) is used to introduce w; after the pivotal step, (3) is used (twice) to eliminate w again, while (0) is used to introduce and remove the $\leq$ - signs.

We observe for arbitrary $a,b$ ,and $w$ introduced according to (3)

$$ \begin{array}{l} \langle \forall c: b \leqslant c \Rightarrow a \leqslant c \rangle \ = {\mathrm {p r e d . c a l c . , h e a d i n g f o r} (3) } \ \langle \forall c: a \leq c \land b \leq c \equiv^ {\sim} b \leq c \rangle \ = { \begin{array}{l} (3) \end{array} } \ \langle \forall c: w \leq c \equiv b \leq c \rangle \ \end{array} $$

$$ \begin{array}{l} \langle \forall c:: w \leq c \equiv b \leq c \rangle \ \Leftrightarrow {\text {L e i b n i z} } \ w = b \ = {0, t o r e i n t r o d u c e \leq , r e q u i r e d f o r \ a p e a l s \quad t o \quad (3) \quad t o \quad e l i m i n a t e \quad w } \ w \leq b ^ {\prime} \land b \leq w \ = {b \leq w, f r o m (3) w i t h c := w, a n d \leq r e f l e x i v e } \ w \le b \ = {(3) \mathrm {w i t h} c := b, \mathrm {a n d} \leq r e f l e x i v e } \ a \leq b \ \end{array} $$

Nuenen, 6 January 1994

p r o p. d r. Eds g e r W. D yksta

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188

USA