Well-foundedness and the relational calculus

In a well-founded set, all decreasing chains are of finite length. In general, we cannot guarantee finite lengths for increasing chains, i.e. the transpose of a well-founded relation is, in general, not well-founded. Yet, there is something special about that transpose: its transpose is well-founded! This suggests the introduction of two forms of well-foundedness, which we may call "left-founded" and "right-founded", with the general connection

(S is left-founded) $\equiv$ (S is right-founded).

For "S is left-founded" we propose the definition -P and S being of type relation-

(0) $\langle {\forall P\therefore \left\lbrack P\right\rbrack \Leftarrow \left\lbrack {P \vee {S}_{i} \upharpoonright P}\right\rbrack }\rangle$ (See Appendix.)

Legend a We follow the convention that seems in the process of being established of giving "i" a binding power between the unary "7" and "w" on the one hand and the binary "v" and "A" on the other. (End of Legend a.)

For "S is right.founded" we propose

$$ \langle \forall P: [ P ] \Leftarrow [ P \vee \neg P; S ] \rangle $$

The proof of the general connection is left as an exercise for the reader, who needs

$\left\lbrack X\right\rbrack \equiv \left\lbrack { \sim X}\right\rbrack$ $\left\lbrack {X \equiv \sim \sim X}\right\rbrack$

$\left\lbrack {\sim \left( {X,Y}\right) \equiv \sim Y;\sim X}\right\rbrack$ $\sim$ distributes over boolean operators (in particular over $v$ and 7).

In the sequel, we confine our attention to the notion of left-foundedness.

We define the transitive closure of $f$ as the strongest $R$ satisfying

(1) $\left\lbrack {R \equiv S \vee S;R}\right\rbrack$

Remark Alternatively, one can replace, in the above definition, (1) by $[R \equiv S \lor R; S]$ or by $[R \equiv S \lor R; R]$ . The equivalence of these three definitions of the transitive closure of $S$ falls outside the scope of this note. A consequence of this equivalence is that the transitive closure of this equivalence is that the transitive closure of the transpose of a relation equals the transpose of its transitive closure. (End of Remark.)

Theorem 0 For left-founded $S$ ,(1) determines

Proof. With $U$ satisfying

(2) $[U \equiv S \vee S; U]$

we have to show that $\left\lbrack {U \equiv R}\right\rbrack$ follows from

(0),(1),(2) We observe

$$ [ U \equiv R ] $$

$\Leftrightarrow { \left( 0\right)$ with $P \mathrel{\text{:=}} U \equiv R : S$ is left-founded

$$ \begin{array}{l} [ (U \equiv R) \vee S; (U \neq R) ] \ = {1, (2) } \ [ (S \vee S; U \equiv S \vee S; R) \vee S; (U \neq R) ] \ = {v d i s t r i b u t e s o v e r \equiv } \ [ S \vee (S; U \equiv S; R) \vee S; (U \neq R) ] \ = {\vee d i s t r i b u t e s o v e r = } \ [ S \vee (S; U \vee S; (U \neq R) \equiv S; R \vee S; (U \neq R)) ] \ = {\quad ; d i s t r i b u t e s o v e r v } \ [ S \vee (S; (U \vee (U \neq R)) \equiv S; (R \vee (U \neq R))) ] \ = {\mathrm {p r e d . c a l c .}: [ X \vee (X \neq Y) \equiv X \vee Y ] } \ [ S \vee (S; (U \vee R) \equiv S; (U \vee R)) ] \ = {\text {p r e d . c a l c .} } \ t r u e \ \end{array} $$

(End of Proof.)

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

Proof With S and R satisfying (0) and (1) we have to show

(3) $\langle {\forall P\therefore \left\lbrack P\right\rbrack \Leftarrow \left\lbrack {P \vee R;{P}^{\prime }}\right\rbrack }\rangle$

To this end we first observe for any $P$

$$ \begin{array}{l} R; \neg P \ = (S ^ {{1 }} v S; R); \neg P \ = {; d i s t r i b u t e s o v e r v } \ \end{array} $$

$$ \begin{array}{l} {\quad ; \quad d i s t i b u t e s o v e r \quad v } \ = S; (\neg P \vee R; \neg P) \ {d e \mathrm {M o r g a n} } \ = S _ {j} \cap (\overline {{P}} \wedge \cap (R; \mathcal {P})) \ \end{array} $$

i.e. we have used (1) to establish

(4) $\left\lbrack {{R}{i} \upharpoonright P \equiv {S}{i}\nmid \left( {{P}{i} \land \left( {{R}{i} \upharpoonright P}\right) }\right) }\right\rbrack$

This formula relates on $R;?$ to an $S;?$ . We now proceed

$$ \begin{array}{l} [ P \vee R _ {j} \neg P ] \ = \begin{array}{l} {\left[ \mathrm {p r e d . c a l c . , t o s t r e n g t h e i n d u c t i o n h y p o t h e s i s} \right]} \ {\left[ (\mathcal {P} \wedge \neg (\mathcal {R}; \neg P)) \vee \mathcal {R}; \neg P \right]} \end{array} \ = {(4) } [ (P \land \neg (R; \neg P)) \lor S; \neg (P \land \neg (R; \neg P)) ] \ \Rightarrow \begin{array}{r l} & {{0) w i t h P := P \wedge \neg (R; \neg P) }} \ & {[ P \wedge \neg (R; \neg P) ]} \end{array} \ \Rightarrow \begin{array}{l} {{\mathrm {p r e d . c a l c .} }} \ {[ P ]} \end{array} \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

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

Proof We have to establish (0) on account of (1) and (3). To this end we observe for any

$$ [ P \vee S; \neg P ] $$

$\Rightarrow { \left( 1\right) ,hence \left\lbrack {S \Rightarrow R}\right\rbrack ,$ and monotonicity $}$

$$ [ P \land R; \neg P ] $$

[\left( 3\right) } ]

$$ [ P ] $$

(End of Proof.)

The above theorems and proofs are essentially the same as those in Avg88/EWD1079 "Well-foundedness and the transitive closure" from 1990.04.28 . (The identifiers R and S have exchanged roles. I am sorry about that.) I have wanted for a long time to give these proofs as rendered here, but did not succeed because in (o) I had restricted the range of dummy P to left-conditions:

$$ \langle \forall P: [ P, t r u e \equiv P ]: \dots \dots \dots \dots \dots \rangle . $$

last weekend, looking again at the problem, I recovered from this mistake.

I am fascinated by the above proofs because they are carried out in our "pointless logic": no need for point predicates" or "line rela-tions"? And that is very nice if we contrast that to the other and I am afraid typical- way of defining well-foundedness.

This is done either by stating that each nonempty subset has a minimal element or by stating that all

decreasing chains are of finite length. Both formulations most explicitly refer to the indi- vidual elements. In (0), the third characteriza- tion of well-foundedness -viz. the validity of proofs by mathematical induction - is stated -as is the notion of transitive closure in (1) - in the pointless relational calculus. It is now clear why the third characterization of well- foundedness is to be preferred: whatever can be achieved without postulating "points" is more simply done without them.

I am very pleased with the above results.

Appendix

Formula (0) is the "pointless" transcription of

(5) $\left\langle {\forall P : \left\langle {\forall x,y : {xP}}\right\rangle \Leftarrow }\right.$

$$ \langle \forall x, y: x P _ {y} \vee \langle \exists z: x S z \land \neg z P _ {y} \rangle \rangle \rangle $$

In this appendix, we shall show that (5) is equivalent with (6), the traditional way of expressing that $S$ is a well-founded relation:

(6) $\langle \forall Q::\langle \forall x::Q.x\rangle \Leftarrow$

$$ \langle \forall x: Q. x \vee \langle \exists z: x S z \wedge \neg Q. z \rangle \rangle . $$

(Usually " $xS{z}^{n}$ is rendered as " $x > {z}^{n}$ or " $x \geq {z}^{n}$ ).) Our proof is by mutual implication.

(6) $\Leftarrow$ (5)

(6)

$=$ {quantification over a fresh dummy with a nonempty range is the identity operation}

$$ \begin{array}{l} \langle \forall Q:: \langle \forall x, y:: Q, x \rangle \Leftarrow \ \langle \forall x, y: Q. x \vee \langle \exists z: x S z \land \neg Q. z \rangle \rangle \rangle \ \end{array} $$

[\left{ \begin{array}{l} \text{ a predicate }Q \text{ corresponds to a relation }P \ \text{ that does not depend on the other }\text{ argument. By extending the range for }P \text{ to all relations, the universal quantification is strengthened. } \end{array}\right. ]

(5)

$$ (6) \Rightarrow (5) $$

(6)

$$ = {\mathrm {w r i t e} Q. x \mathrm {a s} X P y; " \forall Q" \mathrm {t h e n} \mathrm {b e c o m e s}" \forall P, y } $$

$$ \langle \forall P:: \langle \forall y:: \langle \forall x:: x P _ {y} \rangle \Leftarrow $$

$$ \langle \forall x: x P y \vee \langle \exists z: x S z \land \neg z P y \rangle \rangle \rangle $$

$$ \Rightarrow {\mathrm {m o n o t o n i c i t y} o f \forall } $$

(5)

(End of Appendix)

With acknowledgements to the ATAC.

Austin, 13 November 1991

prof. $d\mathrm{r}$ . Edsger w. Dgkstra

Department of Computer Sciences The University of Texas at Austin

Austin,TX 78712- 1188,USA