A simple theorem?

A simple theorem?

In this note I use square brackets to denote universal quantification over the free variables occurring in the enclosed.

Theorem Let $w, x, y$ ,and $z$ be variables ranging over the same non-empty domain and let $p$ be a two-place predicate on that domain. Let the two-place predicate $Q$ be the strongest solution of

$$ X: [ X, x, y ] \equiv p. x. y \vee (E z: p. x. z \wedge X. z. y) ]; \quad (0) $$

let the two-place predicate $R$ be the strongest solution of

$$ X: [ X. x. y \equiv p. x. y \vee (E w: X. x. w \wedge p. w. y) ] \quad . \quad (1) $$

Then

$$ [ Q. x. y \equiv R. x. y ] \quad (2) $$

The above theorem belongs to the folklore I grew up with in the sense that I never bothered to prove it, because it was so obvious. Regard the elements of the domain as the nodes of a graph and attach to p.x.y. the meaning "there is an arrow from x to y"; then, "obviously" Q.x.y means "there is a non-empty path from x to y" and so does R.x.y. hence (2). I always felt that, when challenged, I would be able to prove it, say by mathematical induction over the path length. When I tried to prove the theorem - secundum regulas artis- the latter hunch turned out to be wrong.

Proof The right-hand sides of (0) and (1) being monotonic functions of $x$ , the strongest solutions of these equations exist - Knaster. Tarski - and are also the strongest solutions of the corresponding equations with replaced by $\Leftarrow$ , i.e.

$$ \begin{array}{l} [ Q ^ {\prime}. x. y \Leftarrow p. x. y \vee (E z: p. x. z \wedge Q ^ {\prime}. z. y) ] \ \Rightarrow [ Q. x. y \Rightarrow Q! x. y ] \quad (3) \ \end{array} $$

$$ \begin{array}{l} [ R ^ {\prime}. x. y \leq p. x. y \vee (\underline {{E}} w: R ^ {\prime}. x. w \wedge p. w. y) ] \ \Rightarrow [ R, x, y \Rightarrow R ^ {\prime}, x, y ] \quad . (4) \ \end{array} $$

Predicates Q and R being defined as strongest solutions, we prove (2) by showing that each side implies the other.

$$ [ Q, x, y \Rightarrow R, x, y ] $$

$$ \begin{array}{l} 0 \Leftarrow {Q ^ {\prime} := R i n (3) } \ [ R. x. y \Leftarrow P. x. y v (E z: P. x. z \land R. z. y) ] \ 1 = {\mathrm {s i n c e} R \mathrm {s o l v e s} (1): [ R. x. y \not \in p. x. y ] } \ [ R. x. y \in (E z: p. x. z \land R. z. y) ] \ 2 = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ R, x, y \leqslant p, x. z \land R, z, y ] \ 3 = {\text {p r e d i c a t e c a l c u l u s} } \ [ R, z, y \Rightarrow R, x, y \vee \neg p. x. z ] \ 4 = {\mathrm {r e n a m i n g t h e d u m m i e s :} x, z := z, x } \ [ R, x, y \Rightarrow R, z, y \vee \neg p, z, x ] \ 5 \Leftarrow {R ^ {\prime}. x. y := R. z. y \vee 7 p. z. x i n (4) } \ [ R. z. y \vee \neg p. z. x \Leftarrow \ p. x. y ^ {\prime} \vee (\underline {{E w}}: (R. z. w \vee \neg p. z. x) \wedge p. w. y) ] \ 6 \Leftarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ R. 2. y \Leftarrow (p. 2. x \land p. x. y) \lor (\equiv w: R. 2. w \land p. w. y) ] \ 7 \Leftarrow {\left{f r o m (1): [ R. 2. x \leqslant p. 2. x ] \right} \ [ R. 2. y \Leftarrow (R. 2. x \land p. x. y) \lor (\underline {{E}} w: R. 2. w \land p. w. y) ] \ \end{array} $$

8 = {predicate calculus}

$$ [ R. z. y \Leftarrow (E w: R. z. w \wedge p. w. y) ] $$

$= { R$ solves (1) $}$

true

The proof of $[Q.x.y\leqslant R.x.y]$ is too similar to be given in full.

(End of Proof.)

I was surprised by the amount of shuffling in- volved, but very pleased because all the steps were -by now- so familiar and so clearly suggested by the circumstances:

step 0 : Here we have no choice: for the demonstrandum it is irrelevant that $Q$ is a solution of (0) as it would also hold, were $Q$ stronger; the conclusion has to be drawn from the knowledge what $Q$ implies. i.e. (3). The step is the substitution dictated by the circumstances.

step 1: This is the recognition that of our two in- dependent proof obligations, one is trivial.

step 2: A syntactical simplification.

step 3: Known as "the shunting trick", useful because it enables us to get in the demonstrandum an isolated $R$ as the antecedent, a form required for the application of (4)

step4: A clerical precaution so as to avoid errors in a nested substitution.

step 5: The actual substitution in the application

step G: "Unshunting" to begin with, as it allows the

simplification of omitting the disjunct "7 p.z.x" from the existentially quantified expression. By then I saw the job was done and could afford to omit the conjunct p.z.x from the existential quantification.

step 7: This step has been introduced to separate the explicit appeal to $R$ being a solution of (1) from the next step. step 8: This subsumes the one proof obligation in the other. step 9: A final appeal to (i) settles the question.

Because in the original demonstrum it is clearly irrelevant that $\mathbb{R}$ has been defined as a strongest solution the later appeal to (4) may surprise the reader. That appeal, however, occurs after step 0 , in which we could not avoid to strengthen the demonstrum.

Austin, 1 November 1985

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