Well-foundedness and the transitive closure (with A.J.M. van Gasteren)

Well-foundedness and the transitive closure

The transitive closure of relation $\mathcal{R}$ is defined as the strongest relation that satisfies for all $x, y$ (in the domain of $\mathcal{R}$ )

(0) $x{S}{y} \equiv x{R}{y}v\left( {{E}{z} : z{R}{y} : {x{S}_{z}}}\right)$

A corollary of the following theorem is that the restriction to the strongest relation can be omitted in the case of well-founded $\mathbb{R}$ .

Theorem 0 For well-founded $R$ ,at most 1 relation

Proof. Well-foundedness of $R$ means that for any predicate $P$ (on the domain of

(1) $\left( {{A}{y} : {P}{y}}\right) \Leftarrow \left( {{A}{y} : {P}{y}}\right) \Leftarrow \left( {{A}{x} : {x}{Ry} : {P}_{x}}\right) )$ , a formula that captures the notion of proof by mathematical induction over the domain of $R$ .

Let $S$ and ${S}^{\prime }$ satisfy (0). We prove our demonstrandum $S = {S}^{\prime }$ ,that is

$$ (\underline {{A}} x: (\underline {{A}} y: \times S _ {y} \equiv \times S _ {y} ^ {\prime})) $$

by proving for any $x$

$$ (A y: \times S y \equiv x S ^ {\prime} y) $$

by mathematical induction over $y$ . Accord

Starting with the consequent, we observe

$$ \begin{array}{l} (x S y \equiv x S ^ {\prime} y) \Leftarrow (\underline {{A}} z: z R y: x S z \equiv x S ^ {\prime} z) \ x S y \equiv x S ^ {\prime} y \ = {S a n d S ^ {\prime} s a t i s f y (0) } \ x R y \vee (\underline {{E}} z: 2 R y: x S z) \equiv \ x \tilde {R} y \vee (\underline {{E}} _ {2}: z \tilde {R} y: x S ^ {\prime} z) \ \Leftarrow {\text {L e i b n i z} } \ (\underline {{E}} z: 2 R y: x S _ {z}) \equiv (\underline {{E}} z: 2 R y: x S _ {z} ^ {\prime}) \ \Leftrightarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} _ {2}: \mathbf {z} R y: \times S _ {2} \equiv \times S ^ {\prime} _ {2}) \ \end{array} $$

(End of Proof.)

Examples Let $R$ be a relation on the natural

numbers. With ${x}_{Ry} \equiv x + 1 = y$ ,the only

$S$ satisfying $\left( 0\right) \;{S}{1}x{S}{y} = x < y\;\left( {With}\right)$

${x}^{R}{y}^{c} = {x}^{c}{y}^{R}$ 的 strongest

satisfying (0) $x{y}{1} \leq {x}^{2}{y}{0}$ ; in this

case, however, (0) is also satisfied

${x}_{S}y \equiv {true}.\;$ Our first $R$ is well founded,

our second, R, being reflexive, is not.

(End of Examples.)

The significance of Theorem 0 is that, for a well-founded relation, its transitive closure need not be handled as extreme solution.

This is illustrated in the proof of our next theorem.

Theorem 1 The transitive closure of a well-founded relation is well-founded.

Proof With R and S satisfying (0) and (1) we have to prove for any P (1) with R:=S, i.e. - naming the most complicated subexpression-

$\left( 3\right) \;\left( {{By} : {P}{y}}\right) \Leftarrow \left( {{A}{y} : {P}{y} \Leftarrow {Q}{y}}\right)$ with ${Q}{y} \equiv \left( {\underline{A}x : x{S}{y} : P\left( x\right) }\right)$

Since the occurrence of $S$ is confined to $Q$ ,we start manipulating $Q.y$ :

$$ \begin{array}{l} Q, y \ = {\langle 4 \rangle } \ (\underline {{A}} x: \times S y: P x) \ = {(0) } \ (\underline {{A}} x: x R y \vee (\underline {{E}} z: z R y: x S z): P _ {x}) \ = {\text {s p l i t t i n g t h e r a n g e} } \ (\underset {\sim} {A x}: \underset {\sim} {x R y}: \underset {\sim} {P x}) \wedge (\underset {\sim} {A x}: (\underset {\sim} {E z}: \underset {\sim} {z R y}: \underset {\sim} {x S z}): \underset {\sim} {P x}) \ = {\mathrm {t r a d i n g a n d} v \mathrm {d i s t r i b u t e s o v e r} A } \ (\underline {{A x}}: \times \underline {{R y}}: \overline {{P _ {x}}}) \wedge (\underline {{A x}}: (\underline {{A z}}: \overline {{z R y}} \wedge \overline {{x S z}}: \overline {{P _ {x}}})) \ = {\mathrm {r e n a m i n g}; \mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s} } \ (\underline {{A}} z: z R y: \overline {{P}} _ {z}) \wedge (\underline {{A}} z: z R y: (\underline {{A}} x: x S _ {z}: P _ {x})) \ = {\mathrm {c o n j o i n g t h e t e r m s}; (4) \mathrm {w i t h} y := z } \ (\underline {{A}} z: \underline {{z}} R y: P. z \wedge Q. z) \ \end{array} $$

Thus we have established $-\frac{1}{2}$ from (0).

(5) ${Q}{1}y \equiv \left( {{A}{2} : {2Ry} : {P}{2} \land {Q}{2}}\right)$

Our gain from the above use of (0) is that, whereas (4) expressed in terms of $S$ , (5) expresses $Q$ in terms of $R$ , which is well-founded.

To prove (3) we now observe

$$ (\underline {{A}} y: \quad P _ {y} \Leftarrow Q _ {y}) $$

$$ \begin{array}{l} = {\langle 5 \rangle } \ (\underline {{A}} y: \underline {{P}}. y \Leftarrow (\underline {{A}} z: z \underline {{R}} y: \underline {{P}}. z \wedge Q. z)) \ = {(5) a n d p r e d. c a l c., p r e p a r i n g f o r (1) } \ (\underline {{A}} y: P _ {y} \wedge Q. y \Leftarrow (\underline {{A}} z: Z R y: P _ {z} \wedge Q _ {z})) \ \Rightarrow {R i s w e l l f o u n d e d: (1) w i t h P. y := P. y \wedge Q. y } \ (A y: P y \wedge Q y) \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ (\underline {{A}} y: \underline {{P}}. y) \ \end{array} $$

(End of Proof.)

We would like to stress that from the point of view of manipulation, the structure of the above proof is very nice. The first part uses (0) - which connects R and S - to eliminate S and to introduce R . The second part then uses (1), which states R's relevant property. We also think we greatly benefitted from the introduction of the identifier Q . The frequency with which it occurs gives an idea of how much Q has shortened the

text. Moreover it highlights that in a number of steps the internal structure of Q and a fortiori the choice between (4) and (5) - is totally irrelevant. In the second part of the proof, we first replaced the antecedent and then conjoined the consequent with Q.y to show the heuristics for the latter operation. Starting with

$\left( {A,y : P,y \Leftrightarrow Q,y}\right)$

$$ (\underline {{A}} y: P. y \land Q. y \Leftarrow Q. y) $$

would have reduced the number of appeals to (5), but the above first step is more of a rabbit.

Finally we prove

Theorem 2 If the transitive closure of a relation is well-founded, so is the relation itself.

Proof We have to prove (1), given (0) and the fact that $S$ is well-founded. To this end we observe for any $P$

$$ (\underline {{A}} y: P _ {y} \Leftarrow (\underline {{A}} x: X R y: P _ {x})) $$

$\Rightarrow { {f}{\text{rem }}\left( 0\right) : x{Ry} \Rightarrow x{S}{y}$ ,antimonotonicity twice

$$ (\underline {{A}} y: \underline {{P}}. y) \Leftarrow (\underline {{A}} x: \times S y; \underline {{P}}. x) $$

$\Rightarrow { S$ is well-founded

$$ (A y: P, y) $$

(End of Proof.)

We point out that one can base the proofs of theorems 1 and 2 on an alternative definition of well-foundedness, viz. that all decreasing chains are of finite length. (In that setting, theorem 1 is simpler to prove than theorem 2!) One may be under the impression that the alternative proofs are shorter and simpler than the ones developed here, but that impression could very well be wrong. For a fair comparison, the alternative proofs should be as explicit as ours on what they use; we mention arithmetic, the notion of infinity, and the connection between decreasing chains for the original relation and its transitive closure.

Finally, please note that we have established the equivalence between the classical mathematical induction with base and step, and "course of values induction: with $xRy \equiv x + 1 = y$ , the transitive closure $S'$ is $xSy \equiv x < y$ .

Austin, 28 April 1990

dr.A.J.M.van Gasteren Edelweislaan 20 5582 BW WAALRE The Netherlands

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