Inspired by ~[ x ] equiv [~ x ]

Inspired by $\sim \left\lbrack x\right\rbrack \equiv \left\lbrack {\sim x}\right\rbrack$

I had started with the relation calculus and we were exploring in class what could be derived from the axiom gal. $(\sim ,\sim)$ about the transposition (or "converse") ~. Because we could use

$$ \sim [ x ] \equiv [ \sim x ] $$

if it were a theorem, and it seemed to be so, one of my students - Daniel A. Jimenez - raised the question whether the analogy between the "everywhere" operator and universal conjunctivity was so strong that for universally conjunctive

$$ (0) \qquad f. [ x ] \equiv [ f. x ] \qquad \mathrm {f o r a n y} x. $$

Because the "everywhere" operator is of type: boolean scalar $\leftarrow$ predicate, (0) at first sight might suggest a type conflict, but this is resolved when $f$ satisfies

{f:true, ffalse} ≤ {true, false}, which is the case if -like ~!- f is uni- versally junctive. So we changed our hypothesis into the weaker "does (0)

hold for any universally junctive $f$ ?

The answer to this question is - perhaps not so surprisingly- negative. We shall demonstrate this by constructing for a two-state space a counterexample, i.e. a universally junctive $f$ that does not satisfy (0).

Let the two states of the space correspond to the point-predicates $s$ and is respectively, and let $f$ be given by the following table

[ \Rightarrow {f}^{2}x - {4x} = {4x} - {2}^{2}]

true

s true

7s false

false false

To see that (0) is not satisfied we observe:

$$ \begin{array}{l} f. [ s ] \equiv [ f. s ] \ = {\mathrm {p r e d . c a l c ; d e f . o p} f } \ f. \mathrm {p a i s e} \equiv [ \mathrm {t r u e} ] \ = {\mathrm {d e f . o f} p; \mathrm {p r e d . c a l c} } \ f a l s e \equiv t r u e \ = \begin{array}{l} {{\mathrm {p r e d . c a l c} }} \ {\mathrm {f a l s e .}} \end{array} \ \end{array} $$

Finally we have to check that $f$ is universally junctive. Since our state space is very finite this junctivity is verifiable. The relevant observations are

(i) corresponding to the empty junctions [f:true ≡ true] and [f,false ≡ false] (ii) corresponding to the nonempty junc.

$$ \begin{array}{l} [ f. (s \vee 7 s) \equiv f. s \vee f. (7 s) ] \ [ f. (t r u e \land x) \equiv f. t r u e \land f. x ] \ [ f. (t r u e v x) \equiv f. t r u e v f. x ] \ [ f. (f a l s e \land x) \equiv f. f a l s e \land f. x ] \ [ f. (\mathrm {f a l s e} v x) \equiv f. \mathrm {f a l s e} v [ f. x ]. \ \end{array} $$

Small as the example is, I did not find a really concise demonstration of the junctivities.

There was a time when I liked coun- terexamples very much because they were so "convincing", but times have changed: I don't like the above proof at all.

First of all, it is laborious: it took me,

I think, more than an hour to come up with this function $f$ and then I had still to convince myself that it was universally junctive.

Secondly, all that labour is very speci- fically geared to refuting (0). I would be much happier if I could look at the "symbol dynamics" of my rewrite rules and had laws that would allow me to conclude that with those rewrite rules it is "obviously" impossible to derive (0). I realize that this naive dream might speak of unwarranted optimism.

Austin, 4 November 1995

PS. I paid more attention to the quality of my handwriting and hope that that is appreciated. EWD.

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