A relational summary

A relational summary

Here we present the relational calculus as a specialization of the predicate calculus: to the latter we add two operators and one constant.

To begin with we introduce a unary prefix operator, which -following Hesselink- we call the "estrangement" and denote by *". It is given the same high binding power as 7 - i.e. higher than all infix operators except functional application - under the usual rule that unary prefix operators are right associative.

The estrangement is introduced by the following two axioms. (Note: A summary of formulae is given at the end of this paper.)

(0) $\left\lbrack {P \Rightarrow {xQ}}\right\rbrack \equiv \left\lbrack Q \Rightarrow {xP}\right\rbrack$ (1) $[P \Leftarrow Q] \equiv [Q \Leftarrow P]$

From (0) follow

(2) $\left\lbrack {\text{false} \equiv \text{true}}\right\rbrack$ and (3) $\left\lbrack {*\left( {EQ:Q}\right) \equiv \left( {{HQ} : * Q}\right) }\right\rbrack$

From (1) follow

(4) $\left\lbrack {\star \text{true} \equiv \text{false}}\right\rbrack$

(5) $\left\lbrack {*\left( {AQ}\right) : Q}\right) \equiv \left( {{EQ} : * Q}\right) \rbrack$

Proof of (2): [false = true]

$$ \begin{array}{l} = {\text {p r e d . c a l c .} } \ [ t r u e \Rightarrow * f a l s e ] \ = {(0) } \ [ f a l s e \Rightarrow * t r u e ] \ = {\mathrm {p r e d . c a l c .} } \ t r u e \quad (E n d o p P r o o f o p (2)) \ \end{array} $$

Proof of (3): We observe for any $P$ ,and $Q$ ranging over some set,

$$ \begin{array}{l} [ P \Rightarrow * (\exists Q: Q) ] \ = {() } \ [ (E Q:: Q) \Rightarrow * P ] \ = {\text {p r e d . c a l c .} } \ [ (A Q: Q \Rightarrow * P) ] \ = {\mathrm {i n t e r c h a n g e} } \ (A Q: [ Q \Rightarrow * P ]) \ = {() } \ (A Q: [ P \Rightarrow * Q ]) \ = {\mathrm {i n t e r c h a n g e} } \ [ (A Q:: P \Rightarrow * Q) ] \ = {\text {p r e d . c a l c .} } \ [ P ^ {\prime} \Rightarrow (\neg Q:: * Q) ] \ \end{array} $$

and since the equivalence of first and last

lines hold for any $P$ , (3) follows.

(End of Proof of (3))

Note. Formula (2) follows from (3) by choosing

From both axioms we conclude

(6) $\left\lbrack {P \equiv * Q}\right\rbrack \equiv \left\lbrack {Q \equiv * P}\right\rbrack$

$$ \begin{array}{l} \mathrm {P r o o f} \quad [ P \equiv * Q ] \ = {\text {p r e d . c a l c .} } \ [ P \Rightarrow * Q ] \land [ P \Leftarrow * Q ] \ = {(0) a n d (1) } \ [ Q \Rightarrow * P ] \land [ Q \Leftarrow * P ] \ = {\mathrm {p r e d . c a l c .} } \ [ Q \equiv * P ] \ \end{array} $$

(End of Proof.)

Instantiating (6) with $Q \mathrel{\text{:=}} * P$ yields

(7) $\left\lbrack {P \equiv * * P}\right\rbrack$ ,

i.e. the estrangement is an involution.

Next we introduce an asymmetric binary operator called "composition" and denoted by an infix $^ { \text{喜} } ; ^ { \text{喜} }$ , which - following Scholten- we give a binding power less than the unary operators and higher than the binary logical operators. Composition occurs in three axioms, viz.

(8) $\left\lbrack {{P}_{j}\left( {Q;R}\right) \equiv \left( {P;Q}\right) ;R}\right\rbrack$ ,

which states that composition is associative;

$$ [ P; Q \Rightarrow D ] \equiv [ P \Rightarrow * Q ], \tag {9} $$

which links composition and estrangement to the constant D - following Hesselink called "the diversity"-" and

$$ (1 0) \quad [ * (* P; * Q) \equiv \neg (\neg Q; \neg P) ], $$

which links composition and estrangement to the negation.

Axiom (8) we exploit by omitting semantically superfluous parentheses in continued compositions. Axiom (9), which is our only axiom about the constant $D$ , is mainly used to rewrite implications.

$$ (1 1) \quad [ P; Q \Rightarrow D ] \equiv [ Q; P \Rightarrow D ] $$

$$ \begin{array}{l} \mathrm {P r o o f} \quad [ P; Q \Rightarrow D ] \ = {(9) } \ [ P \Rightarrow * Q ] \ = {(0) } \ [ Q \Rightarrow * P ] \ = {(9) \mathrm {w i t h} P, Q := Q, P } \ [ Q; P \Rightarrow D ] \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

what in (11) might look like an inter- change of $P$ and $Q$ is better interpreted as a rotation. We leave to the reader to show, for instance, the equivalence of

(i) $\left\lbrack {{P}{j}{Q}{j}R \Rightarrow D}\right\rbrack$ , (ii) $\left\lbrack {Q;R;P \Rightarrow D}\right\rbrack ,$ and (iii) $[\mathbb{R};\mathbb{P};\mathbb{Q}\Rightarrow \mathbb{D}]$

The proof has to use the associativity of the composition. In hints, I intend to refer to (ii) and its generalizations under the name "rotation".

Our second use of (9) is to rewrite

$$ (\underline {{A}} Z: [ P \Rightarrow Z ] \equiv [ Q \Rightarrow Z ]) \equiv [ P \equiv Q ] $$

From predicate calculus. Because $\star$ is an involution - i.e. (7) - we may rewrite the left-hand side of the above as

$$ (\exists Z: [ P \Rightarrow * Z ] \equiv [ Q \Rightarrow * Z ]) $$

On account of (9) we deduce

(12) $\left( {A;Z : \left\lbrack {P,Q \Rightarrow D}\right\rbrack \equiv \left\lbrack {Q;Z \Rightarrow D}\right\rbrack }\right) \equiv \left\lbrack {P \equiv Q}\right\rbrack$ .

Now it is simple to show that $* D$ is the (left- and right-hand) identity of composition, i.e.

(13) $[\star D; P \equiv P]$ (14) $\left\lbrack {{P}_{j} * D \equiv P}\right\rbrack$

Proof. We observe for any $Z$

$$ [ * D; P; Z \Rightarrow D ] $$

$$ \begin{array}{l} = {\mathrm {r o t a t i o n} } \ [ P; Z; * D \Rightarrow D ] \ \end{array} $$

$$ \begin{array}{l} = {(9) \mathrm {w i t h} P, Q := P; Z, * D } \ [ P; 2 \Rightarrow * * D ] \ \end{array} $$

$$ \begin{array}{l} = {(7), i. e. * i s a n i n v o l u t i o n } \ [ P; 2 \Rightarrow D ] \ \end{array} $$

which, according to (12), establishes (13). The very similar proof of (14) is left as an exercise to the reader.

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

We now explore with the aid of (9) the boolean expression

$$ [ X; Y \Rightarrow Z ] $$

We observe for any $X, Y, Z$

$$ [ X; Y \Rightarrow Z ] $$

$$ = {\ast i s a n i n v o l u t i o n } $$

$$ [ X; Y \Rightarrow * * Z ] $$

$$ = {(9) } $$

$$ [ X; Y; * Z \Rightarrow D ] $$

$$ \begin{array}{l} = {(9) } \ [ X \Rightarrow * (Y; * Z) ] \ = {\mathrm {r o t a t i o n} } \ [ Y; * Z; X \Rightarrow D ] \ = {(9) } \ [ Y \Rightarrow * (* Z; X) ] \ \end{array} $$

and thus we have derived

$$ \begin{array}{l} [ X; Y \Rightarrow Z ] = [ X \Rightarrow * (Y; * Z) ] (15) \ a n d - u s i n g \Leftarrow a n d r e n a m i n g - \ [ X \Leftarrow Y; Z ] \equiv [ * (* X; Y) \Leftarrow Z ] (16) \ \end{array} $$

Next, we use the above to show that com- position is universally disjunctive in both arguments. In order to show that composition is universally disjunctive in its left operand, we define for fixed $Y$ the functions

$$ [ f. X \equiv X; Y ] \quad a n d \quad [ g. Z \equiv * (Y; * Z) ], $$

and shall derive the universal disjunctivity

$$ [ p. x \Rightarrow z ] \equiv [ x \Rightarrow g. z ] \mathrm {f o r a l l} X, Z (*). $$

In order to show that composition is uni- versally disjunctive in its right operand, we define for fixed Y the functions

$$ [ f Z \equiv Y; Z ] a n d [ g. X \equiv * (X; Y) ], $$

and shall derive the universal disjunctivity of $f$ from the rewritten (16):

$$ [ X \Leftarrow P, Z ] \equiv [ g. X \Leftarrow Z ] \quad f o r a l l X, Z \quad (*) $$

Note that, $X$ and $Z$ being dummies, the two formulae marked (*) express the same constraint

on $f$ and $g$ . That for an $p$ and $g$ satisfying (*) , $f$ is universally dis- junctive is a well-known theorem, whose proof is given below. Note that in the design of this proof, one has hardly any freedom : at each step, there is only one thing one can do.

Proof In order to derive for any range of $P$

$$ [ f. (\underline {{E P}}; \cdot P) \equiv (\underline {{E P}}; \cdot f. P) ] $$

we observe for any $\mathcal{R}$

$$ \begin{array}{l} [ f. (E P: P) \Rightarrow R ] \ = {(\ast) } \ [ (\underline {{E P}}: P) \Rightarrow g. R ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{A ^ {\prime} P}}: P \Rightarrow g, R) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} P: \colon [ P \Rightarrow g, R ]) \ = {(\star) } \ (\underline {{A}} P: [ f, P \Rightarrow R ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{\underline {{A}}}} P: f. P \Rightarrow R) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\exists P: f. P) \Rightarrow R ] \ \end{array} $$

From which observation the demonstrandum

follows.

(End of Proof.)

(17) ; is universally disjunctive in both operands.

The reader is supposed to be familiar with the best-known consequences of $f$ being universally disjunctive: $[f.\text{false} \equiv \text{false}]$ and $f$ is monotonic with respect to $\Rightarrow$ .

We now turn to (10), our third and last axiom about composition. It connects estrange- ment and negation, and does so in a sym- metrical way. One of our near purposes is to show that negation and estrangement commute, but because the constant D is so closely associated with composition, we first investigate whether we can find a nice, simple relation between $$ , 7 , and D . Because * and 7 are involutions and $D$ is the identity element of composition, (10) is likely to have an instantiation that admits simplification. It has indeed. (Note that the instantiation of (10) is all but dic- tated by the desire to exploit at both sides that $*D$ is the identity element of composi- tion.) We observe

true

$$ \begin{array}{l} = {(1 0) \mathrm {w i t h} P, Q := 7 \times D, D } \ [ * () D; * D) \equiv \neg (\neg D; \neg \neg * D) ] \ = {(1 4); 7 \mathrm {i s a n i n v o l u t i o n} } \ [ * \times 7 * D \equiv 7 (7 D; * D) ] \ = {\ast i s a n i n v o l u t i o n; (1 4) } \ [ 7 * D \equiv 7 7 D ] \ = {7 \mathrm {i s a n i n v o l u t i o n} } \ \end{array} $$

$$ [ * D \equiv \neg D ] $$

Thus we have derived

$$ [ * D \equiv \neg D ] \quad . \tag {18} $$

And now we are ready to show that $\neg$ and

$$ (1 9) \quad [ \neg * X \equiv * \neg X ]. $$

Proof Aiming to apply (12), we observe for arbitrary $x, z$

$$ \begin{array}{l} [ * \vdash X; Z \Rightarrow D ] \ = {\ast \text {i s a n i n v o l u t i o n , t w i c e} } \ [ * * (x \neg X; * x Z) \Rightarrow D ] \ = {(1 0) \mathrm {w i t h} P, Q := \neg X, * Z } \ [ * \neg (\neg * 2; \neg \neg X) \Rightarrow D ] \ {(1) } \ [ * D \Rightarrow \neg (\neg * Z; \neg X) ] \ {(1 8); \neg \text {i s a n i n v o l u t i o n} } \ [ \neg D \Rightarrow \neg (\neg * Z; X) ] \ {\mathrm {c o n t r a p o s i t i v e} } \ [ \neg * Z; X \Rightarrow D ] \ = {(9) \mathrm {w i t h} P, Q := 7 * Z, X } \ [ 7 * 2 \Rightarrow * X ] \ {\mathrm {c o n t r a p o s i t i v e} } \ [ \neg X \Rightarrow * Z ] \ = {(9) \mathrm {w i t h} P, Q := 7 * X, 2 } \ [ \neg X; Z \Rightarrow D ] \ \end{array} $$

Predicate Z being arbitrary, (19) now follows on account of (12) from the equivalence of the first and last terms above.

(End of Proof.)

Inspired by the commutativity of $x$ and 7, we now introduce a special symbol and name for their functional composition. It is denoted by the tilde $\sim$ and called the "transposition". It is formally defined by

(20) $[\sim P \equiv * P] \quad [\sim P \equiv 2 * P]$ .

Also $\sim$ is an involution and it commutes with $*$ and 7. More precisely

(20) $\left\lbrack {\sim \sim P \equiv P}\right\rbrack$

(20) $\left\lbrack {\star P \equiv \sim \sim P}\right\rbrack \;\left\lbrack {\star P \equiv \sim \sim P}\right\rbrack$ (20) $\left\lbrack {\neg P \equiv \sim * P}\right\rbrack \;\left\lbrack {\neg P \equiv * \sim * P}\right\rbrack \;$ ;

the proofs are left to the reader. Formulae

(10) and (18) can be rewritten as (21) $[\sim (P;Q)\equiv \sim Q;\sim P]$ (22) $\left\lbrack {\sim D \equiv D}\right\rbrack$

Finally, we introduce the constant $J$ satisfying

(23) $\left\lbrack {J \equiv \neg D}\right\rbrack \;\left\lbrack {J \equiv * D}\right\rbrack \;\left\lbrack J \equiv \sim J\right\rbrack$ (24) $[J;P\equiv P][P;J\equiv P]$

the feeling being that the identity element of the composition deserves its own name.

We observe for any range of $Q$

$$ \begin{array}{l} \sim (\mathrm {E Q}: \mathrm {Q}) \ = {(2 0), d e f i n i t i o n o f \sim } \ \eta * (E Q: Q) \ = {(3) } \ \lnot (\neg Q:: * Q) \ = {\mathrm {d e} M o r g a n } \ (E Q: \neg * Q) \ = {(2 0) } \ (E Q: \sim Q), \ \end{array} $$

i.e. transposition distributes over existential quantification (i.e. is universally disjunctive).

Since -see (20)- transposition distributes over negation as well and negation and existential quantification suffice for all logical expressions, we have derived

(25) transposition distributes over the logical operators and the quantifications

Remark Note that composition -see (21) is excluded from the logical operators; composition is a relational operator. (End of Remark.)

By definition

(26) ( $P$ is a precondition) $\equiv \left\lbrack {P;{true} \equiv P}\right\rbrack$

$$ (P \mathrm {i s a} ^ {\prime} p o s t c o n d i t i o n) \equiv [ t r u e; P \equiv P ] $$

the proof of

(27) ( $P$ is a postcondition)

$$ (\sim P i s a p r e c o n d i t i o n) $$

is left to the reader. In what follows we shall deal with postconditions; the exploration of the dual theorems is left to the reader.

An important theorem about postconditions is that a logical expression of postconditions is again a postcondition. As in the proof of (25), we prove it for the special cases of existential quantification and negation. First we show that if $P$ ranges over a set of postconditions - i.e. $(\underline{AP} : [true; P \equiv P])$

$$ [ \mathrm {t r u e}; (\underline {{E}} P:: P) \equiv (\underline {{E}} P:: P) ] $$

Proof We observe for $P$ ranging over postconditions

$$ \begin{array}{l} t r u e; (E P:: P) \ = {\quad ; i s u n i v e r s a l l y d i s j u n c h i v e } \ (E P::: t r u e; P) \ = {\mathcal {P} \mathrm {i s a p o s t c o n d i t i o n} } \ (E P: P) \ \end{array} $$

(End of Proof.)

To prove that the negation of a postcondition is a postcondition, we first observe

$$ \begin{array}{l} [ t r u e; P \equiv P ] \ = {\text {p r e d . c a l c .} } \ [ t r u e; P \Rightarrow P ] \land [ t r u e; P \Leftarrow P ] \ = {2 4 } \ [ t r u e; P \Rightarrow P ] \land [ t r u e; P \Leftarrow ]; P ] \ = {[ t r u e \Leftrightarrow ] } a n d; i s m o n o t o n i c } \ [ t r u e; P \Rightarrow P ] \ \end{array} $$

Hence our proof obligation is

$$ [ t r u e; P \Rightarrow P ] \equiv [ t r u e; \neg P \Rightarrow \neg P ] $$

Proof We observe for any $P$

$$ \begin{array}{l} [ t r u e; \neg P \Rightarrow \neg P ] \ = {(1 6) \mathrm {w i t h} X, Y, Z := \neg P, \mathrm {t r u e}, \neg P } \ [ * (* \neg P; t r u e) \Leftarrow \neg P ] \ = {\mathrm {c o n t r a p o s i t i v e}, (2 0) } \ [ \sim (\sim P; t r u e) \Rightarrow P ] \ = {(\mathbf {2 1}), (\mathbf {2 0}) a n d [ t r u e \equiv \sim t r u e ] } \ [ \mathrm {t r u e}; P \Rightarrow P ] \ \end{array} $$

$$ (\mathrm {E n d o f P r o o f}) $$

Find thus we have established

(28) logical expressions built from postcondi

fions are postconditions

Next we prove

$$ (2 9) [ t r u e; P \Rightarrow P ] \Rightarrow [ X; (Y \wedge P) \equiv X; Y \wedge P ] $$

Proof The proof of the equivalence is by mutual implication. The one direction uses that $P$ is a postcondition, the other one that $\neg P$ is one. In both cases we use the lemma

$$ (*) \quad (Q \mathrm {i s a p o s t c o n d i t i o n}) \Rightarrow [ X; Q \Rightarrow Q ] $$

which follows from the monotonicity of $\operatorname{com}$ position.

$$ \begin{array}{l l} \frac {L H S \Rightarrow R H S}{p o s k c o n d i t i o n} & \mathrm {W e o b s e r v e f o r a n y} X, Y \mathrm {a n d} \ & P \end{array} $$

$$ X _ {j} (Y _ {n}, P) $$

$$ \begin{array}{l} \Rightarrow \begin{array}{l} {{\left[ Y _ {1} P \Rightarrow Y \right], [ Y _ {2} P \Rightarrow P ], m o n o t o n i c i t y o f; }} \ {X _ {1} Y \wedge X _ {2} P} \end{array} \ \Rightarrow \frac {{(*) \mathrm {w i t h} Q = P ; \mathrm {m o n o l o n i c i t y o f} P \wedge }}{X ; Y \wedge P} \ \end{array} $$

$$ \begin{array}{l} L H S \Leftarrow R H S \ X; (Y \land P) \lor \neg P \ \Leftarrow {(*) \mathrm {w i t h} Q := \neg P } \ X; (Y, P) \vee X; \neg P \ = {\text {； d i s t r i b u t e s o v e r} v } \ X: ((Y \wedge P) \vee \neg P) \ = {\mathrm {p r e d . c a l c .} } \ X; (Y, \neg P) \ \Leftrightarrow {[ Y v, P \Leftarrow Y ] a n d m o n o t o n i c i t y o f ; 3 \ X; Y \quad (\mathrm {E n d o f P r o o f .}) \ \end{array} $$

Notational Convention From now onwards the reader is supposed to be so familiar with (20) that in the use of $\texttt{\textbf{I}}\texttt{\textbf{}}$ and $\sim$ the composition of any two will immediately be rendered by the third. Prior to the introduction of $\sim$ , one has the choice between $\texttt{I}\texttt{}\texttt{X}$ and $\texttt{*}\texttt{I}\texttt{X}$ ; the introduction of the "superfluous" $\sim$ enables us to introduce $\sim X$ as the canonical representa- tation. I should have introduced this nota- tional convention earlier. (End of Notational Convention.)

In order to relate the above to Tarshi's Axiomatization, we derive as a theorem Tarshi's axiom

$$ [ P; Q \land \sim R \equiv f a l s e ] \equiv [ Q; R \land \sim P \equiv f a l s e ] $$

Proof We observe for any $P, Q, R$

$$ [ P; Q \land \sim R \equiv f a l s e ] $$

$= \left{ {\left( {\text{predicate and }}\right) \text{relational calculus}}\right}$

$$ {\mathrm {p r e d i c a t e c a l c u l u s} } $$

$$ [ P; Q \Rightarrow * R ] $$

$= \left{ {\text{relational calculus}}\right}$

$$ [ P; Q; R \Rightarrow D ] $$

$= \left{ {{rota} + {rata}}\right}$

$$ [ Q; R; P \Rightarrow D ] $$

$= \left{ {\text{as above}}\right}$

$$ \begin{array}{l} [ Q; R \land \sim P \equiv \mathrm {f a l s e} ] \ (E n d o f P r o o f.) \ \end{array} $$

To quote Hoare and He Jifeng on Tarski's formulation: "Replacement of this last axiom will not be lamented. (To this I can add that, by our current standards, also notationally Tarski's text is atrocious.)

In order to relate the above to the axiomatization of Hoare and He Jifeng, we shall derive as a theorem their axiom

$$ [ \neg (P \backslash Q) = (\neg Q \backslash \neg P) \backslash \neg J ] $$

where $\backslash$ is given by

$$ [ X \backslash Y \equiv * (X; * Y) ] $$

Proof We observe for any $P, Q$

$= \left{ {{elimination}\limits_{{outer}}}\right}$

$$ * ((\neg Q \backslash \neg P); \sim J) $$

$= { {\sim J}$ is identity element of $p}$

$$ * (7 Q \backslash 7 P) $$

[ = { \text{elimination}} ]

$$ \eta Q; \sim P $$

$= \left{ \begin{array}{l} {\left( {21}\right) }^{2} \ \end{array}\right}$

$= {$ introduction $}$

$$ \lnot (P \backslash Q) $$

(End of Proof)

To which I am tempted to add "Replace- ment of this last axiom will not be lamented".

Our axiomatization of the relational calculus introduced the triple $\left( {\star ;D}\right)$ , but all axioms given thus far are satisfied if we equate the triple $\left( {\star ;D}\right)$ with the triple $\left( {\neg \land \neg \text{false}}\right)$ . To distinguish the two we now introduce a last axiom for composition that is not satisfiecl by conjunction

(30) $\left\lbrack {{P}{j}\text{true}v\text{true};Q}\right\rbrack \Rightarrow \left\lbrack {{P}{j}\text{true}}\right\rbrack \vee \left\lbrack {\text{true};Q}\right\rbrack$

Remark Note, firstly, that the disjuncts are any precondition and any postcondition respectively. Note, secondly, that LHS $\Leftarrow$ RHS, so we also could have written

(30) $\left\lbrack {{P}{j}\text{true}v\text{true};Q}\right\rbrack \equiv \left\lbrack {{P}{j}\text{true}}\right\rbrack \vee \left\lbrack {\text{true};Q}\right\rbrack$ (End of Remark.)

To relate the above to Tarski we shall prove as a theorem Tarski's axiom

(31) $\left\lbrack {P;{true}\rbrack v}\right\rbrack \left\lbrack {{true};iP}\right\rbrack$

Proof We observe for any $P$

[P; true] v [true; true]

$\Leftrightarrow \;{ {30}$ with $Q \mathrel{\text{:=}} 7{P}_{2}$

$$ \begin{array}{l} [ P; t r u e \vee t r u e; \neg P ] \ \Leftrightarrow {; i s m o n o t o n i c } \ [ P; J \vee J; P ] \ = {J i s; j s u n i t } \ [ P \lor \neg P ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ t r u e \ \end{array} $$

$$ (\mathrm {E n d o f P r o o f .}) $$

Remark I did not succeed in proving (30)

From (31) (End of Remark)

Next we shall prove what C.S. Schohen

postulated to distinguish the triples:

(32) [true; 7x; true] v [X]

Proof We observe for any $X$

$$ \Leftrightarrow {(\mathrm {3 1}) \mathrm {w i t h} P := \mathrm {t r u e}; \mathrm {7 X}, \mathrm {m o n o t o n i c i t y} v } $$

$$ \begin{array}{l} [ t r u e; \neg X; t r u e ] \vee [ X ] \ [ t r u e; \neg (t r u e; \neg X) ] \Rightarrow [ X ] \ \iff {m o n o t o n i c i t y [ ] } \ [ \mathrm {t r u e}; \neg (\mathrm {t r u e}; \neg X) \Rightarrow X ] \ = {\mathrm {r e l . c a l c .} } \ [ * X; \mathrm {t r u e}; \lnot (\mathrm {t r u e}; \lnot X) \Rightarrow D ] \ = {\text {r e l . c a l c} } \ [ x; \mathrm {t r u e} \Rightarrow \sim (\mathrm {t r u e}; x) ] \ = {\mathrm {r e l . c a l c} } \ [ * X; \mathrm {t r u e} \Rightarrow * X; \mathrm {t r u e} ] \ = {\text {p r e d .} c a) c. } \ f r e e \ \end{array} $$

Q.E.D.

Finally we prove C.S. Scholten's

(33) $\left\lbrack {\neg \left( {X;{true};Y}\right) }\right\rbrack \Rightarrow \left\lbrack {\neg X}\right\rbrack \vee \left\lbrack {\neg Y}\right\rbrack$

Proof We observe for any $X$

$$ \begin{array}{l} [ \neg (X; t r u e; Y) ] \ = {\mathrm {p r e c i l . c a l c} } \ [ \neg (^ {1} X; (\mathrm {t r u e} \land \mathrm {t r u e}; Y)) ] \ = {\mathrm {t r u e}; Y \mathrm {i s a p o s t c o n d i t i o n}; (2 9) } \ [ \neg (X; t r u e \land t r u e; Y) ] \ = {\mathrm {d e} M o r g a n } \ [ \tau (X; t r u e) \vee \tau (t r u e; Y) ] \ \Rightarrow {(2 8) a n d i s d u a l; (3 0) } \ [ \tau (X; t r u e) ] \vee [ \tau (t r u e; Y) ] \ \Rightarrow {[ ] \Rightarrow \mathrm {t r u e} ] \quad \mathrm {a n d} \quad \mathrm {m o n o t o n i c i t y} } \ [ i (x; j) ] \vee [ i (j; r) ] \ = {} \ [ \neg X ] \lor [ \neg Y ] \ \end{array} $$

Rather trivially, (32) and (33) can be strengthened to

(32') [true; 7x; true] $\neq$ [X] and $\left\lbrack {7\left( {X;{true};Y}\right) }\right\rbrack \equiv \left\lbrack {7X}\right\rbrack \vee \left\lbrack {7Y}\right\rbrack$

A possibly useful formula , which follows rather directly from (33) is

(34) $\left\lbrack {7\left( {X;{true}}\right) }\right\rbrack \equiv \left\lbrack {7 \times }\right\rbrack$

As axioms, (30) and (33) are interchangeable.

(0) $\left\lbrack {P \Rightarrow * Q}\right\rbrack \equiv \left\lbrack {Q \Rightarrow * P}\right\rbrack$ (1) $[P \Leftarrow Q] \equiv [Q \Leftarrow P]$ (2) $\left\lbrack {\text{false} \equiv \text{true}}\right\rbrack$ (3) $[\star (\underline{\mathrm{EQ}}:Q)\equiv (\underline{\mathrm{HQ}}:\star Q)]$ (4) $\left\lbrack {\star \Rightarrow \mathrm{e} \equiv \mathrm{{false}}}\right\rbrack$ (5) $[\star (\underline{\underline{\mathbf{A}}}\mathbf{Q}:\mathbf{Q})\equiv (\underline{\underline{\mathbf{E}}}\mathbf{Q}:\mathbf{}\mathbf{Q})]$ (6) $[P \equiv Q] \equiv [Q \equiv P]$ (7) $\left\lbrack {P \equiv * * P}\right\rbrack$ (8) $[P; (Q; R) \equiv (P; Q); R]$ (9) $\left\lbrack {P;Q \Rightarrow D}\right\rbrack \equiv \left\lbrack {P \Rightarrow {}^{ * }Q}\right\rbrack$ (10) $\left\lbrack {\left( {P}{j} * Q\right) \equiv n\left( {{nQ};{nP}}\right) }\right\rbrack$ (11) $\left\lbrack {{P}{j}Q \Rightarrow D}\right\rbrack \equiv \left\lbrack {Q;P \Rightarrow D}\right\rbrack$ (12) $\left\lbrack {A : \left\lbrack {{P}_{j}Z \Rightarrow D}\right\rbrack \equiv \left\lbrack {Q;Z \Rightarrow D}\right\rbrack }\right\rbrack \equiv \left\lbrack {P \equiv Q}\right\rbrack$ (13) $\left\lbrack {D};P \equiv P\right\rbrack$ (14) $\left\lbrack {P;\frac{xD}{2D} \equiv P}\right\rbrack$ (15) $[X;Y\Rightarrow Z]\equiv [X\Rightarrow (Y;Z)]$ (16) $\left\lbrack {X \Leftrightarrow Y;Z}\right\rbrack \equiv \left\lbrack {\ast \left( {\ast X;Y}\right) \Leftrightarrow Z}\right\rbrack$ (17) ; is universally disjunctive in both operands (18) $[ * D \equiv 7D]$ (19) $\left\lbrack {7 * x \equiv * 7}\right\rbrack$

(20) $\neg$ (negation), $*$ (estrangement) and

are all three involutions - distribute over each other $\therefore$ satisfy $\left\lbrack {7 * \sim P \equiv P}\right\rbrack$ for all $P$

(21) $[\sim (P;Q)\equiv \sim Q;\sim P]$ (22) $[\sim D \equiv D]$ (23) $\left\lbrack {J \equiv \neg D}\right\rbrack \left\lbrack {J \equiv \neq D}\right\rbrack \left\lbrack J \equiv \sim J\right\rbrack$ (24) $\left\lbrack {\mathcal{J};\mathcal{P} \equiv \mathcal{P}}\right\rbrack \;\left\lbrack {\mathcal{P};\mathcal{J} \equiv \mathcal{P}}\right\rbrack$ (25) transposition distributes over the logical operators and the quantifications (26) ( $P$ is a precondition) $\equiv \left\lbrack {P,\text{ true } \equiv P}\right\rbrack$

$$ (P \mathrm {i s a} ^ {\prime} p o s t c o n d i t i o n) \equiv [ t r u e; P \equiv P ] $$

(26') $\left( {P\text{is a precondition}}\right) \equiv \left\lbrack {{P}_{;}\text{true} \Rightarrow P}\right\rbrack$

$$ (P \mathrm {i s a p o s t c o n d i t i o n}) \equiv [ \mathrm {t r u e}; P \Rightarrow P ] $$

(27) ( $P$ is a postcondition)

$$ (\sim P i s a p r e c o n d i t i o n) $$

(28) logical expressions built from postconditions are postconditions. (29) $\left\lbrack {\operatorname{true};P \Rightarrow P}\right\rbrack \Rightarrow \left\lbrack {X;{\left( Y \land P\right) }^{ \land }X;Y \land P}\right\rbrack$ (30) $\left\lbrack {{P}{j}\text{true}v\text{true};Q}\right\rbrack \Rightarrow \left\lbrack {{P}{j}\text{true}}\right\rbrack \vee \left\lbrack {\text{true};Q}\right\rbrack$ (31) $\left\lbrack {P;{true}}\right\rbrack \vee \left\lbrack {{true};\neg P}\right\rbrack$

(32) $\left\lbrack {\text{true};\forall X;\text{true}}\right\rbrack \vee \left\lbrack X\right\rbrack$ $\left( {32}^{\prime }\right) \;\left\lbrack {\text{true};7{x}{;}{\text{true}}\rbrack \neq \left\lbrack X\right\rbrack }\right\rbrack$ (33) $\left\lbrack {i\left( {{X}{j}\text{ true };Y}\right) }\right\rbrack \Rightarrow \left\lbrack {iX}\right\rbrack \vee \left\lbrack {iY}\right\rbrack$ $\left\lbrack {7\left( {{X}{j} + 1,Y}\right) }\right\rbrack \equiv \left\lbrack {7X}\right\rbrack \vee \left\lbrack {7Y}\right\rbrack$ (34) $\left\lbrack {\neg \left( {{X}{i} + \text{true}}\right) }\right\rbrack \equiv \left\lbrack {\neg X}\right\rbrack$

Acknowledgements

My indebtedness to A. Tarski, to C.A.R. Hoare and He Jifeng, to W.H. Hesselink and to C.S. Scholten is obvious. I did not much more than sort the material and present it in a homoge- neous notation.

Austin, 8 November 1990

Prof. dr. Edsger W. Dgksta Department of Computer Sciences The University of Texas at Austin Austin, TX 78750- 8138