A theorem proved by John Segers

A theorem proved by John Segers

On Tuesday 25 January 1994, the ETAC (= Eindhoven Tuesday Afternoon Club) was invited/challenged to prove the following theorem (that had been proved and communicated by John Segers).

(0) $\left\lbrack {{47} - {47} + {4y} \equiv - {4y} + {4y}}\right\rbrack$ for all $y$ ,

where $\psi$ (read: " dagger") denotes the non-reflexive transitive closure, i.e. $\psi p$ denotes the strongest solution of $p$ , for instance: $x: [p \vee x; x \Rightarrow x]$ . We use

(1) $\left\lbrack {p \Rightarrow {4p}}\right\rbrack$ (2) $\left\lbrack {{\varphi }{p};{\varphi }{p} \Rightarrow {\varphi }{p}}\right\rbrack$ (3) $\left\lbrack {p;{P}{P} \Rightarrow {P}_{P}}\right\rbrack$ (4) $\left\lbrack {p \Rightarrow x}\right\rbrack \land \left\lbrack {p;x \Rightarrow x}\right\rbrack \; \Rightarrow \left\lbrack {{4p} \Rightarrow x}\right\rbrack ,$

all for all $p,x$ .

of Note.)

The EtAC met the challenge. We give our proof before discussing it.

We begin by introducing $b$ and $c$ by

(5) $\left\lbrack {b \equiv - 4 - 4 - y}\right\rbrack ,\left\lbrack {c \equiv - 4 - y}\right\rbrack ,\left\lbrack {b = - 4 - c}\right\rbrack$ ,

which allows us to rewrite our demon-

strandum (0) as $\left\lbrack {{4b} \equiv b}\right\rbrack$ ,for the

proof of which we observe

$$ \begin{array}{l} [ \psi b = b ] \ = {\text {p r e d . c a l c .} } \ [ 4 b ^ {\prime} \Rightarrow b ] \land [ b \Rightarrow 4 b ] \ = {(1) \mathrm {w i t h} p := b } \ [ \psi b \Rightarrow b ] \ \Leftrightarrow {4) w i t h p, x := b, b } \ [ b \Rightarrow b ] \land [ b; b \Rightarrow b ] \ = {\mathrm {p r e d . c a l c} } \ [ b; b ^ {\prime} \Rightarrow b ] \ = {5 } \ [ \neg \Psi c; \neg \Psi c \Rightarrow \neg \Psi c ] \ = {\mathrm {p r e d . c a l c} } \ [ \psi_ {c} ^ {\prime} \Rightarrow \neg (\neg \psi_ {c}; \neg \psi_ {c}) ] \ \Leftrightarrow {4) w i t h p, x := c, 7 (7 4 c; 7 4 c) \ [ c \Rightarrow \neg (\neg \psi_ {c}; \neg \psi_ {c}) ] \land \ [ c; \neg (\neg \psi_ {c}; \neg \psi_ {c}) \Rightarrow \neg (\neg \psi_ {c}; \neg \psi_ {c}) ] \ \end{array} $$

We now deal with these two conjuncts

separately. For the last conjunct we observe

$$ \begin{array}{l} [ c; \neg (\neg \psi_ {c}; \neg \psi_ {c}) \Rightarrow \neg (\neg \psi_ {c}; \neg \psi_ {c}) ] \ = {\mathrm {r e l . c a l c . , R E X i n p a r t i c u l a r} } \ [ \sim c; \neg \psi c; \neg \psi c \Rightarrow \neg \psi^ {\prime} c; \neg \psi c ] \ \Leftrightarrow {\quad ; i s a s s o c i a t i v e a n d m o n o t o n i c } \ [ \sim c; \neg \psi c \Rightarrow \neg \psi c ] \ \end{array} $$

$$ \begin{array}{l} [ \sim c; \neg \psi c \Rightarrow \neg \psi c ] \ = {\mathrm {R E X} } \ [ c; \psi c \Rightarrow \psi c ] \ = {3) \mathrm {w i t h} p := c } \ t r u e \ \end{array} $$

so, the last conjunct has been proved, in- dependent of the internal structure of c We now proceed on the assumption that the proof of the first conjunct does require the internal structure of c as given in (5) : [c ≡ ?y] . That c is a negation of a predicate is irrelevant , for this holds for any predicate. However, [7c ≡ 4y], i.e. the fact that 1c is a transitive closure of y could

be relevant. Since y only occurs in

(1) through (4) for those properties of

$\psi$ that contain $p$ only in the combina- tion 4p , i.e. (2). We observe therefore

$$ \begin{array}{l} \begin{array}{r l} & {\mathrm {t r u e}} \ {=} & {{\left(2\right) \mathrm {w i t h} p := y }} \ & {\left[ 4 y; 4 y \Rightarrow 4 y \right]} \ {=} & {{\left(5\right), \mathrm {i . e .} [ 1 c \equiv 4 y ] }} \end{array} \ (6) \quad [ 7 c; 7 c \Rightarrow 7 c ] \ \end{array} $$

in other words: if the internal structure of c plays a role, it has to do so via (6). We now observe for the first conjunct

$$ \begin{array}{l} [ c \Rightarrow \neg (\neg \psi_ {c}; \neg \psi_ {c}) ] \ = {\text {p r e d . c a l c .} } \ [ \neg \psi_ {c}; \neg \psi_ {c} \Rightarrow \neg c ] \ \Leftrightarrow \quad {(6) } \ [ \neg \psi c; \neg \psi c \Rightarrow \neg c; \neg c ] \ \Leftarrow \quad {j m o n o t o n i c } \ [ \neg \psi_ {c} \Rightarrow \neg c ] \ = {\text {p r e d . c a l c .} } \ [ c \Rightarrow \psi c ] \ = {1) w i t h p := c } \ f r u e \ \end{array} $$

And this concludes the proof.

The introduction of $b$ is justified be- cause the first 4 steps of the proof are independent of $b$ 's internal structure. At the ETAC session of 1994.01.25, we "pealed off" the operators one at a time, i.e. our next step was to introduce $[d \equiv 4 \neg 4y]$ and eliminate $b$ by $[b \equiv 7d]$ , but, though correct, I consider in retrospect the introduction of $d$ overdone: admittedly, the introduction of $d$ postpones the introduction of a few daggers but it is mathematically void since any $b$ is the negation of something. We also used the "confront" -the conjugate of composition - because the subexpression $7(7d;7d)$ asked for it, but in retrospect it was not worth

the trouble.

When we performed the second step, viz. " ${;$ is associative and monotonic $3 ^ { \prime }$ in the proof of the second conjunct, we felt we were doing something absolutely standard: in our experience, an appeal to the associa-tivity of composition is almost always in- dicated when a composition becomes an argument of a composition.

In the proof of the first conjunct, the appeal to (6) - which we had not formu- lated in advance- came as a surprise. I had not seen that (6) is the only way to exploit that $\psi y$ is a transitive closure. (Note (x is transitive) $\equiv$ (x is a transitive closure).)

Austin, 9 February 1994

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