The design of a proof of equality (Mathematical Methodology)

The design of a proof of equality

In this chapter we deal with real variables.

Let $p,x,y$ satisfy

(0) $\;\left( {\underline{A}w : p \leq w}\right. \equiv \;x \leq w \land y \leq w)$

such triples exist for any pair $x,y :$ take,for instance,for $p$ the maximum of $x$ and $y$ .

Let $q,x,y$ satisfy

$\left( 1\right) \;\left( {A,w : w \leq q \equiv w \leq x \vee w \leq y}\right)$

such triples exist for any pair $x,y$ : take,for instance,for $q$ the maximum of $x$ and $y$ .

The purpose of this chapter is to design the formal argument that derives

$p = q$

from (0) and (1)

As a heuristic device, we apply what is known as "the nabla trick" - "nabla" is the name of the character

trying to prove (2) from (3) and (4), which have been obtained from (0) and (1), respec- tively, by replacing $\leq$ by the unknown rela- tional operator

(3) $\left( {R + w}\right) \cdot p{v}{w} \equiv x{v}{w} \land y{v}{w}$ (4) $\left( {A{w}{1} : {wv}{q}{1} = {wv}{x}{1}v{w}{2}{y}{1}}\right)$

As we go along, we discover which properties of

Remark The nabla trick serves more than one purpose. Firstly, because the as yet undefined operator $\nabla$ defies interpretation of (3) and (4) in terms of some model, the nabla trick assists us in manipulating formulae without interpreting them. Secondly, the nabla trick is a means for collecting those properties of that are needed to derive (2) from (0) and (1); it is quite possible that, besides , other relations have those properties as well and , therefore, could be chosen for $\nabla$ . The nabla trick is an aid in keeping track of what is needed for our arguments, and that is also what this chapter is about. (End of Remark.)

How do we derive (2), i.e. $p = q$ ? The first

observation is that, since there exist different real numbers, $p = q$ cannot be established without constraints on both $p$ and $q$ . Since (3) and (4) are the only constraints given on $p$ and $q$ , both (3) and (4) are needed. In these formulae, $p$ and $q$ only occur as operands of $\nabla$ while we have to establish $p = q$ , i.e., we need some property of $\nabla$ that relates it to $=$ . Remembering for a short moment that eventually $\leq$ should be an acceptable instantiation for $\nabla$ , we postulate that nabla is antisymmetric, i.e., satisfies for any $p, q$

$$ (5) \quad p = q \Leftrightarrow p \nabla q \wedge q \nabla p. $$

Remark Relation (5) is a constraint imposed on $\nabla$ ,and that is why we have not written the needlessly stronger

$$ p = q \equiv p \nabla q \wedge q \nabla p $$

though this relation would have been satisfied with $\leq$ for $\nabla$ . Not requiring more than needed is the rule of the game in this chapter. (End of Remark.)

By virtue of (5), demonstrating $p = q$ has been reduced to the independent demonstrations

of the conjuncts $p{\nabla q}$ and $q{\nabla p}$ . Focussing our attention on the first one, $p{\nabla q}$ ,then we see that this term is an instantiation of the left-hand sides of both (3) and (4). We therefore split them up: let it be given that for all $w$

(3c) $p \nabla w \Leftarrow x \nabla w \land y \nabla w$ (3b) $p \nabla w \Rightarrow x \nabla w \land y \nabla w$ $\left( {4a}\right) \cdot w{\nabla q} \Leftarrow w{\nabla x} \vee w{\nabla y}$ $\Rightarrow {w}{\nabla x} = {w}{\nabla y}$

We expect the proof of $p \nabla q$ to use (3a) and (4a), but not the two b-formulae. To prove $p \nabla q$ for any $p$ satisfying (3a) and any $q$ satisfying (4a), we observe

$\Leftrightarrow \;{p}^{ \vee }q = 1.$ $x{v}_{9}$ $\Leftarrow \;\left{ \begin{matrix} { {4a}} & \text{ with } \ \; & \text{ with } \end{matrix}\right.$ $w \mathrel{\text{:=}} x\;;\;\left( {4a}\right)$ with

$$ (x \nabla x \vee x \nabla y) \wedge (y \nabla x \vee y \nabla y) $$

$\Leftrightarrow \;{$ pred.ca $c} .$

$$ (x \nabla x \wedge y \nabla y) $$

$= \left{ \left( 6\right) \text{ with }w : x;\left( 6\right) \text{ with }w : y}$

true

where nabl is postulated to be reflexive, i.e.

(6) $w \Delta {v}_{w}$

Remark For completeness' sake we show what would have happened, had we applied (3a) and (4a) in the other order: we would have arrived at another strengthening of $p \nabla q$ , for the demonstration of which (6) does not suffice.

$$ \begin{array}{l} \Leftrightarrow \quad \begin{array}{l} p \nabla q \ \left{\mathrm {(4 a) w i t h} w := p \right} \end{array} \ p \nabla x \vee p \nabla y \ \Leftrightarrow {3 a) w i t h w := x; (3 a) w i t h w := y } \ (x \nabla x \wedge y \nabla x) \vee (x \nabla y \wedge y \nabla y) \ = {(6) } \ y \nabla x = v \times \nabla y \ \end{array} $$

(End of Remark.)

Let us now focus our attention on establishing the second conjunct, $q\bar{\nabla} p$ . There are good reasons to expect the proof of $q\bar{\nabla} p$ to use (3b) and (4b), but not the two a-formulae. The simplest and most general reason for this expectation is the fact that, in contrast to the a-formulae, the b-formulae have not been used yet, but this is only as compelling as our conviction that the b-formulae have to be used indeed. The con-

vincing reason to use the b-formulae comes from the shape of the demonstrum $q\nabla p$ How can we use our knowledge about $p$ so as to get a nabla expression with $p$ as its right-hand argument? The only way of doing so is instantiating (3) with $w:= p$ On account of (6), however, this instantiation makes (3a) vacuously true, hence useless, and (3b) is the only part that can contribute. Similarly, on account of the q in front of $\nabla$ , it is (4b) that has to be instantiated with $w:= q$ . Finally, to combine $p$ and $g$ in a single nabla expression, we postulate that nabla is transitive, i.e. satisfies for any $p,q,w$ (7) $q \nabla w \land w \nabla p \Rightarrow q \nabla p$

After the above explorations we observe

$$ \begin{array}{l} 9 \nabla p \ = {\mathrm {i d e m p o t e n c e o f} \mathrm {d i s j u n c t i o n} } \ q \nabla p \vee q \nabla p \ \Leftrightarrow {(\mathrm {7}) \mathrm {w i t h} w := x; (\mathrm {7}) \mathrm {w i t h} w := y } \ (q \nabla x \wedge x \nabla p) \vee (q \nabla y \wedge y \nabla p) \ \Leftrightarrow \quad {\mathrm {p r e d . c a l c . , h e a d i n g f o r (3 b) w i t h} w := p } \ (q \nabla x \wedge x \nabla p \wedge y \nabla p) \vee (q \nabla y \wedge x \nabla p \wedge y \nabla p) \ = {\text {p r e d . c a l c .} } \ (q \nabla_ {x} \vee q \nabla_ {y}) \wedge (x \nabla p \wedge y \nabla p) \ \Leftrightarrow \quad {(4 b) \mathrm {w i t h} w := q; (3 b) \mathrm {w i t h} w := p } \ \end{array} $$

Mathematical Methodology

$$ \begin{array}{r l} & {9 \nabla q \wedge p \nabla p} \ {=} & {{(6) \mathrm {w i t h} w := q; (6) \mathrm {w i t h} w := p }} \ & {\mathrm {t r u e}} \end{array} $$

Remark The first step is not surprising. We use idempotence to duplicate the term so as to be able to exploit the transitivity of $\nabla$ without destroying the symmetry between $x$ and $y$ . The use of the disjunction, rather than the conjunction, is not surprising either: since we are constructing a strengthening chain we choose our next intermediate result as weak as possible. Note that, with in the first step conjunction instead of disjunction, the appeal to (4b), four steps later, would have been impossible. (End of Remark.)

In order to prove $p = q\left( {3 - 4}\right)$ and

we had to postulate

is antisymmetric, l.e (5) $\nabla$ is reflexive, i.e. (6), is transitive, i.e. (7)

Relations enjoying the above three properties are known as "partial orders". We now confine our attention to relations $\nabla$ that are partial orders. However, not every partial relation $\nabla$ is such that for any $x,y$ a pair $p,q$ exists that satisfies (3) and (4) - for instance: = for $\nabla$ -

Mathematical Methodology.

Assuming that for partial order $\nabla$ and arbitrary $x, y$ , (3) and (4), and hence (2), are satisfied, we observe for any $x, y$

true

$$ \begin{array}{l} = {\nabla \mathrm {i s r e f l e x i v e} } \ p \nabla p \wedge q \nabla q \ = {(3) \mathrm {w i t h} w := p; (4) \mathrm {w i t h} w := q } \ x \nabla p \wedge y \nabla p \wedge (q \nabla x \vee q \nabla y) \ = {(2), i. e. p = q } \ x \nabla p \wedge y \nabla p \wedge (p \nabla x \vee p \nabla y) \ = {\wedge d i s t r i b u t e s o v e r v } \ (x \nabla p \wedge y \nabla p \wedge p \nabla x) \vee (x \nabla p \wedge y \nabla p \wedge p \nabla y) \ \Rightarrow {\triangledown \text {i s r e f l e x i v e a n d t r a n s i t i v e}, \text {t w i c e}) \ (x = p \wedge y \nabla x) \vee (y = p \wedge x \nabla y) \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ (x = p \vee y = p) \wedge (y \nabla x \vee x \nabla y) \ \end{array} $$

The first conjunct of the last line states that $p$ is one of the values $x, y$ ; the second conjunct $y\nabla x \vee x\nabla y$ , holding, as it does, for any $x, y$ , states that the partial order $\nabla$ is what is known as a "total order". Examples of a total order on the real numbers are $\leq$ and $\geq$ . With $\leq$ for $\nabla$ , $p$ (and $q$ ) is known as the maximum of $x$ and $y$ , and is denoted by $x\uparrow y$ . With $\geq$ for $\nabla$ , $p$ (and $q$ ) is known as the minimum of $x$ and $y$ ,

and is denoted by $x \downarrow y$ . For the maximum, we have the alternative characterizations

(8) $x \uparrow y \leq w \equiv x \leq w \land y \leq w$ (9) $w \leq x \uparrow y \equiv w \leq x\;v\;w \leq y$

and - remembering $u \geq w \equiv w \leq u -$ for the minimum

$\left( {10}\right) \;w \leq x \downarrow y \equiv w \leq x \land w \leq y$ ${x}^{ \downarrow }{y}^{ \leq }w$ $x \leq w\;v\;y \leq w$

Acknowledgement I am grateful to the anonymous referee of EWD1071 for the “Mathematische Gesellschaft in Hamburg”, a remark from whom provided the incentive to show the equivalence between the alternative characterizations for the maximum and the minimum, respectively. (End of Acknowledgement.)

Austin, 24 January 1991

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

USA