The transitive closure of a wellfounded relation

The transitive closure of a wellfounded relation

Transitive closures can be defined in many ways, but today we define the nonreflexive transitive closure s of a relation r as the strongest satisfying

(0) $\left[ \begin{array}{lll}r & v & r;s \end{array} \right] = s\bigg]$

From (0) alone - i.e. not using that

(1) $\left\langle {\forall x : \lbrack x \equiv s;x\rbrack \Rightarrow \lbrack x \equiv r;x\rbrack }\right\rangle$

Proof We observe for an $x$ satisfying

(2) $[x \equiv s; x]$

$$ \begin{array}{l} \equiv \begin{array}{l} \times \ {(2) } \end{array} \ s; x \ \equiv {() } \ (r \vee r; s); x \ \equiv {\colon o v e r \vee a n d a s s o c i a t i v e } \ r; x \vee r; s; x \ = \left{ \begin{array}{l} (2) \end{array} \right} \ r; x \vee r; x \ = {\text {p r e d . c a l c .} } \ r; x \ \end{array} $$

(End of Proof)

One of the formulations of "r is left-wellfounded' is

(3) $\left\langle {\forall x : \left\lbrack {x \equiv r;x}\right\rbrack \Rightarrow \left\lbrack {-r - x}\right\rbrack }\right\rangle$

Thanks to (1), (3) implies

$$ \langle \forall x: [ x \equiv s; x ] \Rightarrow [ \neg x ] \rangle $$

in other words: if a relation is left- wellfounded, so is its nonreflexive transitive closure.

${S}{1} = \left( {{a}{1} + {a}{2} + {a}{3}}\right) = {764}$

(4) $\left\langle {\forall x : \left\lbrack {x \Rightarrow r;x}\right\rbrack \Rightarrow \left\lbrack {x \Rightarrow s;x}\right\rbrack }\right\rangle$

Proof We observe for any $x$

$$ [ x \Rightarrow s; x ] $$

[\left\lbrack {x \Rightarrow \left( {r \vee r;s}\right) ;x}\right\rbrack ]

$\Leftrightarrow \;\left{ \begin{array}{l} \text{pred. calc. and monotonicty of };} \ \left\lbrack {x \Rightarrow r;x}\right\rbrack \end{array}\right.$

$$ (E n d o f P r o o f.) $$

Thanks to Knaster-Tarski, an alter-native formulation of "s is left- wellfounded " is

(5) $\langle \forall x : [x \Rightarrow s; x] \Rightarrow [7x] \rangle$

From (4) and (5) we derive

$$ \langle \forall x: [ x \Rightarrow r; x ] \Rightarrow [ - 1 x ] \rangle $$

in other words: if the nonreflexive transitive closure of a relation is left- wellfounded, so is the relation itself.

Remark It is worth noting that the proofs of the crucial implications (1) and (4) use neither wellfoundedness nor the fact that is the strongest satisfying (0). (End of Remark.)

For left. wellfounded (0) determines

(6) $[r \vee r; s \equiv s]$ (7) $\left\lbrack {r \vee r;t \equiv t}\right\rbrack$ (8) $\left\langle {\forall x : \left\lbrack {x \Rightarrow r;x}\right\rbrack \Rightarrow \left\lbrack {-1 - x}\right\rbrack }\right\rangle$

we have to prove $\left\lbrack {s \equiv t}\right\rbrack$

Proof For reasons of symmetry, it suffices to prove $\left\lbrack {t \Rightarrow s}\right\rbrack$ . We observe

$$ [ t \Rightarrow s ] $$

$\equiv \;\left{ {\text{pred. calc.}}\right}$

$\Leftrightarrow \;\left{ \begin{array}{ll} \left( 0\right) & \text{ with }x \mathrel{\text{:=}} t \land s} \end{array}\right.$

$$ \begin{array}{l} \begin{array}{r l} & {\left[ t \wedge \neg s \Rightarrow r; (t \wedge \neg s) \right]} \ {=} & {{\mathrm {s h u n t i n g a n d (6)} }} \ & {\left[ t \Rightarrow r \vee r; s \vee r; (t \wedge \neg s) \right]} \end{array} \ \equiv \left{ \begin{array}{l l} i o v e r & v a n d p r e d. c a l c. \ t \Rightarrow r v & r; (t v s) \end{array} \right} \ \iff \begin{array}{l} {{m o n o t o n i c i t y o f ; }} \ {[ t \Rightarrow r v r; t ]} \end{array} \ \equiv \begin{array}{l} {{(7) }} \ {\mathrm {t r u e}} \end{array} \qquad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

The above is a considerable streamlineing of Avg 88/EWD1079 dd 28 April 1990 (which made no use of the relational calculus).

I gratefully acknowledge the contribution of Rutger M. Dgkstra (viz. the isolation of the theorem $(0) \Rightarrow (1)$ ) and that of Wim Feigen and Netty van Gasteren (viz. the final proof of unicity). I thank the ETAC in general for its willingness to discuss this old problem.

$$ N u e n e n, 2 8 J u n e 1 9 9 6 $$

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