The calculus of boolean structures (Part 0)

Copyright Notice

The following manuscript

EWD 1001: The calculus of boolean structures (Part 0)

is a draft of Chapter 5 (pp. 30-62) of

E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, 1990.

Permission to reproduce the manuscript here has been granted by Springer-Verlag New York.

The calculus of boolean structures (Part 0)

We refer by the catchword "Leibniz" to the principle enunciated by Leibniz that a function applied to equal arguments yields equal values. This is usually expressed by the formula

$$ x = y \Rightarrow f. x = f. y $$

Legenda It is generally understood that this for- mula holds for any function $f$ and to any arguments x and y to which f is applicable. We have used an infix period to denote Functional application; it has the highest binding power of all infix operators. The equality $=$ has a higher binding power than the implication $\Rightarrow$ . Hence the above formula is a shorthand for

$$ (x = y) \Rightarrow ((f. x) = (f. y)) $$

(End of Legenda.)

We shall appeal to the principle of Leibniz for named functions; most frequently, however, our appeal to it will be justified by the fact that all expressions we write down are functions of their subexpressions.

We recall our convention that, for $x$ and $y$ structures of some shape, $x = y$ stands for a boolean structure of that same shape; also, $f$

could be a structure-valued function. In order to adapt the principle of Leibniz to that convention we rewrite it as

$$ [ x = y ] \Rightarrow [ f. x = f. y ] $$

(Since a non-structure can always be viewed as a structure on the trivial space consisting of the one anonymous point, our first formulation is a special instance of the above.)

In the following, we shall use the capital letters of the end of the alphabet - primarily X, Y, and Z - as variables of type boolean structure. For the equality between boolean operands we introduce the alternative symbol ≡ , which from a syn- tactical point of view distinguishes itself from = only by the fact that (for reasons of convenience) it has been given a much lower binding power than = . An expression of the form X≡Y is called "an equivalence" and is read as "X equivalent Y" or as "X equivales Y". The justification for a special symbol and a special name in the case of boolean operands is to be found in the circum- stance that equivalence enjoys a property not en- joyed by the equality in general: equivalence is associative, i.e. we have for any X, Y, and Z

$$ [ (X \equiv (Y \equiv Z)) \equiv ((X \equiv Y) \equiv Z) ] $$

Together with Leibniz's principle, (o) indeed expresses

associativity: it implies that wherever we have a subexpression parenthesized as at the left-hand side of (o)'s central $\equiv$ sign, the parentheses may be rearranged as at its right-hand side without changing the value of the total expression. For brevity's sake we shall never carry out these shunting operations in detail, justifying each step by an explicit appeal to (o). Instead, we shall feel free to insert into or remove from such continued equivalences parenthesis pairs as we see fit.

The other important property of the equivalence - remember that $\equiv$ is only an alternative for $=$ - is that it is symmetric; under the convention of omitting redundant parentheses we can state this by

$$ [ X \equiv Y \equiv Y \equiv X ] $$

In combination with the assocativity of the equivalence, (1) is a rich formula: - parenthesized as $[ (X \equiv Y) \equiv (Y \equiv X) ]$ it expresses the symmetry of the equivalence - parenthesized as $[ X \equiv (Y \equiv Y \equiv X) ]$ it expresses that $Y \equiv Y$ is a left-identity element of the equivalence

• parenthesized as $\left\lbrack {\left( {X \equiv Y \equiv Y}\right) \equiv X}\right\rbrack$ ; it expresses that $Y \equiv Y$ is a right-identity element of the equi- valence.

Since for an infix operator that has a left- and a right-hand identity element, the identity element is unique, we can give it a name. In the case of the equivalence, its customary name is "true", a convention properly captured by

(2) $\left\lbrack {X \equiv \operatorname{true} \equiv X}\right\rbrack$

Remark Here one could have the lurking suspicion that the equivalence has as many distinct identity elements as we can have spaces on which to define structures. Fortunately, we can also read the above introduction of true as stating that it is the identity element of the equivalence, whatever the underlying space (including the trivial one). The constant true is as unique as the zeroes in $0 + \sin x$ and in $0 + \cos y$ are the same zero; the constant true is, in fact, as unique as the equivalence and the square brackets themselves. (End of Remark.)

The square brackets denote a unary operator operating on the enclosed, more precisely a function from boolean structures to the traditional boolean domain. Hence (0), (1), and (2) are normal boolean expressions, and, true being the identity element of the equivalence, we could have written instead of (2)

(2') $[X \equiv \text{true} \equiv X] \equiv \text{true}$

for brevity's sake, we prefer (2).

Furthermore we equate a boolean value with a boolean structure on the trivial space consisting of the one anonymous point. Because the square brackets have all the properties of universal quantification over the underlying space, they reduce to the identity function when applied to a boolean expression. So we could have written as further alternatives to (2)

$$ [ [ X \equiv \mathrm {t r u e} \equiv X ] ] $$

$$ [ [ X \equiv \mathrm {t r u e} \equiv X ] \equiv \mathrm {t r u e} ] $$

again, we don't regard these as an improvement over (2)

Because $[X]$ is a boolean expression and, applied to a boolean expression, the square brackets reduce to the identity function, we have

$$ [ [ X ] ] \equiv [ X ] \tag {3} $$

the square bracketing is idempotent.

Formulae (0) through (3) state properties of $\equiv$ , true, and []. We use them as axioms - later, when we introduce more connectives, we shall give more axioms-. We use them to com. pute values as implied by their truth, as illustra- ted by the following (simple) proof.

Theorem. Equivalence is reflexive, i.e. we have for any boolean structure $X$

(4) $[X \equiv X]$

Proof We observe for any $X$

$$ \begin{array}{l} [ X = X ] \ = \left{ \begin{array}{l l} (2), \mathrm {p a r e n t h e s i z e d} & [ X \equiv (\mathrm {t r u e} \equiv X) ] \ [ X \equiv \mathrm {t r u e} \equiv X ] & \end{array} \right. \ = {(2), o r (2 ^ {\prime}), i f y o u p r e f e r } \ \end{array} $$

(End of Proof.)

Remark Note how, in the first hint, we did not need to identify the subexpression being replaced. (End of Remark).

Finally we derive for the identity element of the equivalence

(5) [true]

by calculating for some $X$

$$ \begin{array}{l} [ t r u e ] \ = {(2), \mathrm {p a r s e d} [ \mathrm {t r u e} \equiv (X \equiv X) ] \ [ X \equiv X ] \ = {(4) } \ f r u e \ \end{array} $$

a result in accordance with an earlier announced property of square bracketing. So much for the equivalence.

It is time to introduce our next infix operator; it is called the disjunction, it is written as "v" and read as "or". We give it a higher binding power than the equivalence.

The disjunctio is postulated to be symmetric, i.e. we have for any $X$ and $Y$

(6) $\left\lbrack {X \vee Y \equiv Y \vee X}\right\rbrack$

to be associative, i.e. we have for any $X, Y$ , and $Z$

(7) $[X \vee (Y \vee Z) \equiv (X \vee Y) \vee Z]$ ;

to be idempotent , i.e. we have for any $X$

(8) $[X \vee X \equiv X]$

to distribute over equivalence, i.e. we have for any $X, Y$ , and $Z$

$\left\lbrack {X - V}\right\rbrack = Z) \equiv X - V \equiv X - V}$

Theorem The constant true is the zero-element of the disjunction, i.e. we have for any $X$

(10) $\left\lbrack {X \vee \text{true} \equiv \text{true}}\right\rbrack$

Remark The shorter statement $[Xv\text{true}]$ would have disguised the zero-element. (End of Remark.)

Proof We observe for any $X$ and $Y$

$$ \begin{array}{l} X \vee \mathrm {t r u e} \ = {(2) \mathrm {w i t h} X := Y } \ \end{array} $$

$$ \begin{array}{l} X \vee (Y \equiv Y) \ = {(9) \mathrm {w i t h} Z := Y } \ X \vee Y \equiv X \vee Y \ = {(2) \mathrm {w i t h} X := X \vee Y } \ t r u e \ \end{array} $$

(End of Proof.)

At this stage we can use (6), (7), and (8)

to show the following

Theorem The disjunction distributes over itself, i.e. we have for any $X,Y,$ and $Z$

(II) $[X \vee (Y \vee Z) \equiv (X \vee Y) \vee (X \vee Z)]$

Proof. We observe for any $X, Y, Z$

$$ \begin{array}{l} (X \vee Y) \vee (X \vee Z) \ = {(7), i. e. v i s a s s o c i a l i v e } \ X \vee (Y \vee X) \vee Z \ = {(6), i. e. v i s s y m m e t r i c } \ X \vee (X \vee Y) \vee Z \ = {(7), i. e. v i s a s s o c i a t i v e } \ (X \vee X) \vee (Y \vee Z) \ = {(8), i. e. v i s i d e m p o t e n t } \ X \vee (Y \vee Z) \ \end{array} $$

(End of Proof.)

Remark In the above we have written more

parentheses than we shall do in the future.

The "auto-distribution" holds for any operator that is symmetric, associative, and idempotent.

(End of Remark.)

It is time to introduce a next operator. The shortest total argument would result from introducing the negation first and then defining the conjunction in terms of negation and disjunction (i.e. by postulating one of the Laws of de Morgan.) We shall not do so, firstly because it is the usual order -and it is always nice to show an alternative-, and secondly because it disguises the fact that conjunction can be introduced prior to the introduction of the negation.

Our next infix operator is called the conjunction ; it is written as "A" and read as "and". For reasons of symmetry (which will become apparent later) we give it the same binding power as the disjunction. The con- junction is defined by postulating for any

$$ (1 2) \qquad [ X \wedge Y \equiv X \equiv Y \equiv X \vee Y ] $$

(also known as "The Golden Rule").

Theorem The conjunction is symmetric, i.e. we have

$$ (1 3) \quad [ X \wedge Y \equiv Y \wedge X ] $$

Proof We observe for any $X, Y$

$$ \begin{array}{l} X \wedge Y \ = {1 2 } \ X \equiv Y \equiv X \vee Y \ \end{array} $$

$$ \begin{array}{l} = \begin{array}{l} {\mathrm {a s s o c i a t i v i t y a n d s y m m e t r y} \varphi \equiv ; \ \mathrm {s y m m e t r y} \varphi \lor \exists \end{array} \ Y \equiv X \equiv Y _ {v} X \ = {1 2) w i t h X, Y := Y, X } \ Y \wedge X \ \end{array} $$

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

Theorem The conjunction is associative, i.e. we have for any $X,Y,Z$

$$ [ X \wedge (Y \wedge Z) \equiv (X \wedge Y) \wedge Z ] \tag {14} $$

Proof We observe for any $X, Y, Z$

$$ \begin{array}{l} X \wedge (Y \wedge Z) \ = {\mathrm {G o l d e n R u l e} } \ X \equiv Y \wedge Z \equiv X \vee (Y \wedge Z) \ = {\mathrm {G o l d e n R u l e} } \ X \equiv Y \wedge Z \equiv X \vee (Y \equiv Z \equiv Y \vee Z) \ = {G o l d e n R u l e; \vee d i s t r i b u t e s o v e r \equiv } \ X \equiv Y \equiv Z \equiv Y \vee Z \equiv X \vee Y \equiv X \vee Z \equiv X \vee Y \vee Z \ \end{array} $$

which, thanks to the associativity and symmetry of $\equiv$ and $v$ ,is symmetric in $X,Y$ ,and $Z$ ; this last observation concludes the proof.

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

Theorem The conjunction is idempotent, i.e. we have for any $X$

$$ (1 5) \quad [ X \wedge X \equiv X ] $$

Proof We observe for any $X$

$$ \begin{array}{l} X \wedge X \ = {(1 2) \mathrm {w i t h} Y := X } \ x \equiv x \equiv x \vee x \ = {(2), i. e. i d e n t i t y e l e m e n t o p \equiv 3 \ \begin{array}{c} \times \sim \times \end{array} \ = {(s), i. e. i d e m p o t e n c y o f v } \ \begin{array}{c c} \times & \ & \cdot \end{array} \ \end{array} $$

(End of Proof.)

Theorem The constant true is the identity element of the conjunction, i.e. we have for any $x$

(16) $\left\lbrack {X \land \text{true} \equiv X}\right\rbrack$

Proof We observe for any $x$

$$ \begin{array}{l} X \wedge \mathrm {f r u e} \ = {(1 2) \mathrm {w i t h} Y := \mathrm {t r u e} } \ X \equiv \mathrm {t r u e} \equiv X \vee \mathrm {t r u e} \ = {(1 0), i. e. z e r o e l e m e n t o p v } \ X \equiv \mathrm {t r u e} \equiv \mathrm {t r u e} \ = {\mathrm {i d e n t i t y e l e m e n t} o p = } \ \begin{array}{c c} \times & \cdot \ \hline \end{array} . \ \end{array} $$

(End of Proof.)

Theorem We have for any $X, Y$ the Laws of Absorption

(17) $\left\lbrack {X \land \left( {X \sim Y}\right) \equiv X}\right\rbrack$ (18) $[X \vee (X \wedge Y) \equiv X]$

Proof We observe for any $X, Y$

$$ \begin{array}{l} X \wedge (X \vee Y) \ = {G o l d e n R u l e } \ X \equiv X _ {v} Y \equiv X _ {v} X _ {v} Y \ = {\mathrm {i d e m p o t e n c e} o f v } \ X \equiv X _ {v} Y \equiv X _ {v} Y \ = {\mathrm {i d e n t i t y e l e m e n t o f} \equiv } \ \begin{array}{c c} \times & ; \end{array} \ \end{array} $$

the other proof is like the above, but with $v$ and $\Lambda$

interchanged.

(End of Proof.)

Theorem DisjunctiOn distributes over conjunction, i.e. we have for any $X,Y,Z$

(19) $\left\lbrack {\mathrm{X} \vee \left( {\mathrm{Y} \land \mathrm{Z}}\right) \equiv \left( {\mathrm{X} \vee \mathrm{Y}}\right) \land \left( {\mathrm{X} \vee \mathrm{Z}}\right) }\right\rbrack$

Proof We observe for any $X, Y, Z$

$$ \begin{array}{l} (X \vee Y) \wedge (X \vee Z) \ = {G o l d e n R u l e } \ X \vee Y \equiv X \vee Z \equiv X \vee Y \vee X \vee Z \ = {p r o p e r t h i e s o f v } \ X \vee Y \equiv X \vee Z \equiv X \vee Y \vee Z \ = {v d i s t r i b u t e s o v e r \equiv } \ X \vee (Y \equiv Z \equiv Y \vee Z) \ = {\mathrm {G o l d e n P r u l e} } \ X \vee (Y \wedge Z) \ \end{array} $$

(End of Proof.)

Theorem Conjunction distributes over disjunctio, i.e.

$$ [ X \wedge (Y \vee Z) \equiv (X \wedge Y) \vee (X \wedge Z) ] \tag {20} $$

Proof We observe for any $X, Y, Z$

$$ \begin{array}{l} (X \wedge Y) \vee (X \wedge Z) \ = {(1 9) \mathrm {w i t h} X, Y := (X \land Y), X } \ ((X \land Y) \lor X) \land ((X \land Y) \lor Z) \ = {(1 9) \mathrm {w i t h} Z := X; (1 9) \mathrm {w i t h} X, Z := Z, X } \ (X \vee X) \wedge (X \vee Y) \wedge (X \vee Z) \wedge (Y \vee Z) \ = {\vee i s i d e m p o t e n t } \ X \wedge (X \vee Y) \wedge (X \vee Z) \wedge (Y \vee Z) \ = {(1 7), i. e. a b s o r p h i c } \ X \wedge (X \vee Z) \wedge (Y \vee Z) \ = {\mathrm {o b s o r p h i o n a g a i n} 3 \ x \wedge (Y \vee Z) \ \end{array} $$

(End of Proof.)

Remark Whereas disjunction distributes over equivalence, conjunction, in general, does not. This is the reason why we have proved the last two theorems separately. In connection with the negation we shall discuss the extent to which conjunction distributes over equivalence; then we shall see that the last proof with $\vee$ and $\wedge$ interchanged demonstrates the preceding theorem. (End of Remark.)

It is time to introduce the prefix operator called negation; it is written "7" and read as "non". We give it a higher binding power than $\vee$ and $\wedge$ . We postulate separately its properties with respect to the equivalence and the disjunction; its properties with respect to the conjunction will then be derived.

Negation and equivalence are connected in that we have for any $x, y$

(21) $[\neg (X\equiv Y)\equiv \neg X\equiv Y]$

Theorem We have for any $X, Y$

(22) [7X ≡ Y ≡ X ≡ 7Y]

Proof We observe for any $X, Y$

$$ \lnot X \equiv Y $$

$$ = {(2 1) } $$

$$ \lnot (X \equiv Y) $$

$= \left{ {{sym}{m}{1} \Rightarrow {OF} \equiv 3\text{; (21) with}{X}{1}{Y}{1} \vDash {Y}{1}{X}_{3}}\right}$

$$ X \equiv \neg Y $$

(End of Proof)

Theorem Negation is its own inverse, i.e. we have for any $X$

$$ [ \neg X \equiv X ] $$

Proof We observe for any $X$

$$ \begin{array}{l} \lnot X \equiv X \ = {(2 2) \mathrm {w i t h} Y := 7 X } \ \lnot X \equiv \lnot X \ = {\mathrm {i d e n t i l y e l e m e n t o} p \equiv } \ t r u e \ \end{array} $$

(End of Proof.)

Negation and disjunctio are connected by the famous law of the Excluded Middle, i.e. we have for any $X$

(23) $\left\lbrack {X \vee \neg X}\right\rbrack$

In order to investigate what we can derive from (21) and (23) together, we substitute in (23) $(X \equiv Y)$ for $X$ , i.e.

we observe for any $X,Y$

true

$$ \begin{array}{l} = {(2 3) \mathrm {w i t h} X := (X \equiv Y) } \ [ (X \equiv Y) \vee \neg (X \equiv Y) ] \ = {(2 1) } \ [ (X \equiv Y) \vee (\neg X \equiv Y) ] \ = {v d i s t r i b u t e s o v e r \equiv } \ [ X \vee \neg X \equiv Y \vee \neg X \equiv X \vee Y \equiv Y \vee Y ] \ = {(2 3); i d e n t i f y e l e m e n t o f \equiv 3 \ [ Y \vee \neg X \equiv X \vee \neg Y \equiv Y \vee Y ] \ = {\mathrm {i d e m p o t e n c e} o f v } \ [ Y \vee \neg X \equiv X \vee Y \equiv Y ] \ \end{array} $$

$$ \begin{array}{l} = {G o l d e n R u l e } \ [ Y _ {v}, X \equiv X \wedge Y \equiv X ] \ \end{array} $$

Thus we have proved the

Theorem. We have for any $X, Y$

(24) $[7X \vee Y \equiv X \vee Y \equiv Y]$ (25) $\left\lbrack {{7x} \vee Y \equiv {x\wedge Y} \equiv X}\right\rbrack$

Remark For the variation we have chosen to ex- plore a calculational opportunity, just to see what theorems we would come up with. Platonists would say that we have "discovered" two new theorems. (End of Remark.)

Theorem We have for any $X, Y$

(26) $\left\lbrack {\neg X \vee \neg Y \equiv \neg \left( {X \land Y}\right) }\right\rbrack$ (27) $\left\lbrack {\neg X \land \neg Y \equiv \neg \left( {X \vee Y}\right) }\right\rbrack$

known as the Laws of Augustus de Morgan (who, ironically, lacked a notation for the negation of an arbitrary expression: he had to name it with a single letter and the corresponding letter from the other -i.e. upper or lower- case would then stand for its negation).

Proof We observe for any $X, Y$

$$ \begin{array}{l} i X \cdot v \cdot Y \ = {(2 4) w i t h Y := ? Y } \ X \vee \neg Y \equiv \neg Y \ = {(2 4) \mathrm {w i t h} X, Y := Y, X } \ \end{array} $$

$$ \begin{array}{l} Y \vee X \equiv X \equiv \neg Y \ = {(2 1) } \ \lnot (Y \lor X \equiv X \equiv Y) \ = {\mathrm {G o l d e n P r u l e} } \ \lnot (X \land Y) \ \end{array} $$

With the aid of (22), (27) is easily calculated.

From (26)

(End of Proof.)

With the constant false defined by

(28) [false = ? true]

we can formulate the

Theorem The constant false is the identity

element of the disjunction and the zero element

(29) $\left\lbrack {X \vee \text{false} \equiv X}\right\rbrack$ (30) $\left\lbrack {X \land \text{false} \equiv \text{false}}\right\rbrack$

We leave the proofs to the reader.

For the sake of completeness we mention yet another infix operator, called the discrepancy, written as "≠" and read "differs from." It is symmetric and associative; being mutually associative with the equivalence, it has been given the same low binding power. It is defined by

[XY=Y（X=Y）]

Theorem The constant false is the identity element of the discrepancy, i.e. we have for any $x$

$$ (3 2) \qquad [ X \neq f a l s e \equiv X ] $$

Theorem The conjunction distributes over the discrepancy, i.e. we have for any $X, Y, Z$

$$ [ X \wedge (Y \neq Z) \equiv X \wedge Y \neq X \wedge Z ]. $$

The last theorem is about the only reason for mentioning the discrepancy at all. The proofs are left to the reader.

Remark Nothing in our axioms prevents us from choosing for the negation the identity operator. From the Excluded Middle we immediately derive for any X [X] - or [X ≡ true], if we wish to be more explicit. The only thing wrong with the model in which true is essentially the one and only predicate is that it is void of interest. Hence our interest is restricted to those models in which [X] holds only for X the predicate true and for none of the other predicates, of which at least one exists. The rejection of the noninteresting model is more than we care to formalize. (End of Remark.)

In the above we have gone in great detail

through about three dozen formulae. Some might even argue that we spent more pages than the topic deserves. This, however, is not confirmed by the general experience (of us and of others). In the teaching of this material, two handicaps are quite common.

The one handicap consists in an audience that has used boolean expressions in programming and therefore believes that it knows all these things already. Upon closer inspection, it usually knows the connectives -e.g. by way of a "truth table" but has very few of their properties at its fingertips. And it is these properties, i.e. the rules of manipulation, that are the topic of this chapter and that we wish to convey.

The other handicap consists in an audience which has been introduced to logic by philosophers. Such an audience can become very uneasy about our use of the associativity of the equivalence, because that use does not reflect human reasoning, which, according to some philosophers, logic has to model. Without denying the associativity of the equivalence, some people argue against its use because it is "unnatural" or counterintuitive.

We grant the latter in that (at least Western)

languages are rather poor at expressing equivalence. By all linguistic standards the sentence "Tom can see with both eyes if and only if Tom can see with only one eye if and only if Tom is blind." is -probably for its blatant syntactic ambiguity- total gibberish. But for us this is no reason to disqualify the equivalence. On the contrary, if our formalism allows simple calculations that are beyond the unaided mind because their verbal rendering would be too baffling, so much the better. In this respect we are totally pragmatic, and it was in that vein that we stressed the algebraic nature of the calculus.

It is here that we would like to make two remarks in connection with the Golden Rule. The first remark is concerned with set theory.

A possible model for our boolean structures is provided by the boolean functions defined on some space, with all logical operators to be applied point-wise. The next step is to associate with each boolean structure the subset of points of which it is the characteristic function. (Or, the other way round, we associate with each subset of points its membership function as its corresponding boolean structure.)

We can now try to translate our logical con.

nectives in set-theoretical notation. For the disjunction and the conjunction this is easy: disjunction corresponds to the union U and conjunction to the intersection $\cap$ . With the equivalence we have the problem that it would yield -for two operands- the set of points belonging to both sets or to neither, and set theory shuns operators that yield sets containing elements that don't belong to at least one of the operands. Fortunately, there is what is called "the symmetric set difference" $\div$ - known in electrical engineering as "the exclusive or"- : the elements belonging to one set but not to the other; it corresponds to our discrepancy $\neq$ and in set theory the associativity of the symmetric set difference is known.

In order to render the Golden Rule in standard set-theoretical notation, we have to replace two equivalences by discrepancies, whereas the last one is replaced by the equality sign that has to carry the burden of the square brackets. In books on set theory we may thus find the following "different" theorems

$$ A = B \div (A \cap B) \div (A \cup B) $$

$$ A \div B = (A \cap B) \div (A \cup B) $$

$$ (A \cap B) = A \div B \div (A \cup B) $$

$$ (A \cup B) = A \div B \div (A \cap B) $$

$$ A \div (A \cup B) = B \div (A \cap B) $$

in which we recognize five clumsy renderings of the Golden Rule. The above is a striking example of how inadequate notation can generate spurious diversification. We hope it reinforces our urgent recommendation not to translate our formulae into set-theoretical notation and concepts so as to make them "easier to understand".

Our second remark aims at removing some of the surprise that the Golden Rule usually evokes at first encounter. Remember the stage we were in when we had equivalence and disjunction, both symmetric and associative, and disjunction idempotent and distributing over equivalence. When we raise the question: "What nice new expressions can we now write down?," the distributivity tells us that we can confine ourselves to (continued) equivalences of (single variables and) disjunctions of single variables. In two variables $X$ and $Y$ , $X \equiv Y \equiv X \vee Y$ is the only new one that is symmetric, and this observation invites the study of that expression for which we introduce the short-hand notation $X \wedge Y$ . So, whereas the introduction of the negation was the introduction of something really new, the introduction of the conjunction was in essence no more than a study of what we already

had.

The above is such a nice way of coming up with the conjunction that it immediately raises the question whether we can repeat the game. Given $\equiv$ and v, can we think of another nice expression? The remark that we can confine ourselves (continued) equivalences of (single variables and) disjunctions still holds, but we can forsake symmetry and consider $X\vee Y\equiv Y$ . Is it nice? Apart from being asymmetric, it is nice, as follows from the little theory, given below. (We give the little theory in isolation because it is perfectly general. For simplicity's sake, we formulate it for non-structures, so we don't need to bother about square brackets.)

Little Theory We consider an infix operator $\bullet$ and a binary relation $\rightarrow$ , defined in terms of $\bullet$ by $x \rightarrow y \equiv x \cdot y = y$

(Here the order of decreasing binding power of the operators is $\bullet , \rightarrow$ and $= , \land$ and $\lor , \equiv$ .)

Theorem (is idempotent) $\equiv$ (→ is reflexive), i.e.

$$ (\underline {{A}} x: \quad x \cdot x = x) \equiv (\underline {{A}} x: \quad x \rightarrow x) $$

Proof We observe

$$ \begin{array}{l} (A x: \quad x \cdot x = x) \ = {\ast w i t h y := x } \ (A x: \quad x \rightarrow x) \ \end{array} $$

(End of Proof)

Theorem (is associative) $\Rightarrow$ (→ is transitive)

Proof We observe for any $x,y,z$

$$ \begin{array}{l} x \rightarrow y \land y \rightarrow z \ = {\ast ; \ast w i t h x, y := y, z } \ x \cdot y = y \wedge y \cdot z = z \ \Rightarrow {\mathrm {L e i b n i z} } \ (x \cdot y) \cdot z = z \wedge y \cdot z = 2 \ = {\cdot \mathrm {i s a s s o c i a t i v e} } \ x \cdot (y \cdot z) = z \wedge y \cdot z = z \ \Rightarrow {L e i b n i z } \ x \cdot z = 2 \ = {x \mathrm {w i t h} y := z } \ x \rightarrow z \ \end{array} $$

(End of Proof.)

Theorem (is symmetric) $\Rightarrow \left( {\rightarrow \text{ is antisymmetric }}\right)$

(antisymmetry of $\rightarrow$ means that for any $x,y$

$$ (x \rightarrow y \land y \rightarrow x) \Rightarrow (x = y). $$

Proof. We observe far any $x, y$

$$ x \rightarrow y \land y \rightarrow x $$

$$ {x; x \mathrm {w i t h} x, y := y, x } $$

$$ x \cdot y = y \wedge y \cdot x = x $$

$$ = {\bullet s y m m e t r i c s $$

$$ x \cdot y = y \wedge x \cdot y = x $$

$$ \Rightarrow {\mathrm {L e i b n i z} } $$

$$ x = y $$

(End of Proof.)

Theorem With $\infty$ a unary prefix operator

(cosubutesover·)⇒

$\left( {0\text{ is monotonic with respect to } \rightarrow }\right)$ .

Proof We observe for any $x,y$

$$ \begin{array}{l} \cos x \rightarrow \cos y \ = {\ast \mathrm {w i t h} x, y := \cos , \cos y } \ \cos x \cdot \cos y = \cos y \ = {\in d i s t r i b u t e s o v e r \cdot } \ \cos (x \cdot y) = \sin y \ \Leftrightarrow {L e i b n i z } \ x \cdot y = y \ = {\ast } \ x \rightarrow y \ \end{array} $$

(End of Proof.)

Since -as we have seen in connection with $v$ -

Corollary

(• is associative, idempotent, and symmetric) $\Rightarrow$

$\left( {\bullet \text{is monotonic with respect to} \rightarrow }\right) .$

Theorem (1 is a left-hand unit element of $\rho$ ) $=$ (1 is a left-hand extreme of $\rho \rightarrow$ )

[\text{Proof.}\;\left( {\underline{A}y \mathrel{\text{:=}} 1 \cdot y \equiv y}\right) ]

$$ (\underline {{A}} y: \quad 1 \rightarrow y) \qquad (\mathrm {E n d o f P r o o f}.) $$

Theorem (0 is a right-hand zero element of $\rho$ ) $=$ (0 is a right-hand extreme $\rho \rightarrow$ ).

[\text{Proof.}]

(End of Proof.)

This little theory, which, regrettably, is not widely known, is as beautiful as its proofs are simple. (End of Little Theory.)

Since $v$ is associative, symmetric, and idempotent, has zero element true and unit element false, the above little theory tells us that $X \vee Y \equiv Y$ is, indeed, a nice expression that begs the introduction of the asymmetric infix operator $\Rightarrow$ , called "implication" and read as "implies", by postulating

$\left\lbrack {X \Rightarrow Y \equiv {X}_{\vee }Y \equiv Y}\right\rbrack$

we give $\Rightarrow$ a higher binding power than $\equiv$ ,but lower binding power than $v$ and $\land$ We identify it with the implication as we have used it all the time.

Our little theory tells us

(35) $\left\lbrack {X \Rightarrow X}\right\rbrack$

(36) $[(X\Rightarrow Y)\land (Y\Rightarrow Z)\Rightarrow (X\Rightarrow Z)]$

(37) $\left\lbrack {\left( {X \Rightarrow Y}\right) \land \left( {Y \Rightarrow X}\right) \Rightarrow X \equiv Y}\right\rbrack$ (38) $\left\lbrack {\left( {X \Rightarrow Y}\right) \Rightarrow \left( {X \vee Z \Rightarrow Y \vee Z}\right) }\right\rbrack$ (39) [false $\Rightarrow X$ ] (40) $\left\lbrack {X \Rightarrow \text{true}}\right\rbrack$

Since the properties of the disjunction that we used are shared by the conjunction, it stands to reason to introduce analogously the consequence, written as $\Leftarrow$ and pronounced as "follows from" by

(41) $[X \Leftarrow Y \equiv X \land Y \equiv Y]$ ;

the consequence is given the same binding power as the implication. On account of (34), (41), and the Golden Rule we have

(42) $[X \Leftarrow Y \equiv Y \Rightarrow X]$

for that reason we shall abstain from deriving the analogous formulae for the consequence with the exception of the analogue of (38):

(43) $\left\lbrack {\left( {X \Leftarrow Y}\right) \Rightarrow \left( {{X \land Z} \Leftarrow {Y \land Z}}\right) }\right\rbrack$

Remark Note that the theorem "A conjunctive predicate transformer is monotonic", whose proof was used to illustrate our proof format, is a special case of the theorem about the unary operator $\infty$ from our Little Theory. (End of Remark.)

We shall close this section with a few further formulae about the implication; in view of (42), the analogous ones about the consequence are omitted.

$$ \begin{array}{l} (4 4) \quad [ X \Rightarrow Y = \neg X \vee Y ] \ (4 5) \quad [ t r u e \Rightarrow X \equiv X ] \ (4 6) \quad [ X \Rightarrow \mathrm {f a l s e} \equiv \neg X ] \ (4 7) \quad [ X \Rightarrow X \vee Y ] \ (4 8) \quad [ X \land Y \Rightarrow X ] \ (4 9) \quad [ (U \Rightarrow Y) \wedge (X \Rightarrow Z) \Rightarrow \ (U \wedge X \Rightarrow Y \wedge Z) ] \ [ (U \Rightarrow Y) \wedge (X \Rightarrow Z) \Rightarrow \ (U \vee X \Rightarrow Y \vee Z) ] \ [ (X \Rightarrow Y) \land (Y \Rightarrow X) \equiv X \equiv Y ] (51) \ [ X \land Y \Rightarrow Z \equiv X \Rightarrow \neg Y \lor Z ] (52) \ \end{array} $$

We leave their proofs as exercises for the reader.

Being asymmetric and not associative, the implication is not pleasant to manipulate: there are too many formulae for the manipulation of the implication. The situation is aggravated by

$$ [ X \Rightarrow Y \equiv \neg X \Leftarrow \neg Y ] $$

as follows immediately from (44). In our proofs, brevity is one goal; limitation of the repertoire of manipulations is another goal. For the sake of the latter, we are willing to add one or two steps if by doing so we can avoid appealing to a less attractive manipulation of the implication.

The unary operator denoted by square brackets is a function from boolean structures to the two-valued boolean domain ${\mathrm{true},\mathrm{false}}$ . It has all the properties of universal quanti. fication over a non-empty range, i.e.

(54) $\left\lbrack \text{true}\right\rbrack \equiv \text{true}$ (55) [false] = false (56) $\left\lbrack {\left\lbrack X\right\rbrack \equiv }\right\rbrack \equiv \left\lbrack X\right\rbrack$ -1.e.i.t is idempotent. (57) $\left\lbrack {X \land Y}\right\rbrack \equiv \left\lbrack X\right\rbrack \land \left\lbrack Y\right\rbrack$ - i.e. if distribuies cover $\land -$ (58) $b \vee \left\lbrack X\right\rbrack \equiv \left\lbrack {b \vee X}\right\rbrack$ -with $b \in {$ true,false $}$ .

Austin, 16 February 1987

prop. dr. Edsger W. Dyrksha Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 United States of America