Predicate calculus revisited

0. Expressions versus their representations

The following deals with a universe of expressions, the syntax of which will be given as we go along.

We shall represent expressions by linear strings of characters and shall manipulate expressions by manipulating the strings representing them. It should be understood, that the expressions, rather than their linear representations, form our universe of discourse. The linear representation of an expression is rarely unique, as follows from conventions (i) through (iii). (i) In the case of a symmetric infix operator, such as $+$ from arithmetic, the linear order of the two operands is irrelevant: "a + b" and "b + a" are deemed to represent the same expression. (ii) In the case of an associative infix operatior, such as $+$ from arithmetic, $\left( {a + b}\right) + c$ , " $a + \left( {b + c}\right)$ ",and " $a + b + c$ " are deemed to repre- sent the same expression. (iii) In our linear representation, we shall introduce a so-called "ranking of binding power" as a means of reducing the number of parenthesis pairs needed. With $*$ ,of greater binding power than $+$ , " $a + \left( {b * c}\right)$ " and " $a + b * c$ " are deemed to represent the same expression.

Conventions (i) through (ii) deal with trivial equi- valences of representations of expressions. They absorb the most trivial choices one has to make while choosing a linear representation. The above list of conventions is not necessarily exhaustive; we can expect it to be extended as our syntax gets extended.

Note. The distinction between expressions and their (not necessarily unique) linear representations is purely a matter of convenience. In what follows we shall introduce a more subtle notion of equivalence of expressions. Had not expressions but the linear strings been our universe of discourse, we would only have introduced a notion of equivalence of linear strings. Though from a conceptual point of view it could be argued that this would have been simpler, the mixture of trivial and subtle reasons for equivalence would have been a calculational disadvantage. We warn the reader that our choice of universe of distinct expressions, some of which will turn out to be equivalent, is somewhat arbitrary. (End of Note.)

1. Our way of presenting the syntax

A small number of expressions will be introduced by postulate. The rest of the expressions are defined as their so-called "synthetic descendants".

With $A, B,$ and $C$ standing for expressions, and $P, Q,$ and $R$ being variables, $A(B / P)$ stands

in the following for the expression formed by replacing in A each occurrence of P by B - also expressed as "formed by substituting B for P in $A^{\prime \prime} -$ . The syntactic descendants of A are given by

(i) For any $B$ and $P,A\left( {B/P}\right)$ is a syntactic descendant of $A$ (ii) Syntactic descendants of syntactic. descendants of $A$ are syntactic descendants of $A$ (iii) All syntactic descendants of $A$ are so on account of (i) and (ii).

Note that for any $P$ that does not occur in $A$ , expressions $A$ and $A(B / P)$ are the same. It is poshulated that for any given $A$ we can always invent a $P$ not occurring in it; hence each expression is its own syntactic descendant.

Whether the linear representation of the result of the substitution requires pairs of parentheses or not, depends on the associativity of the operators and their relative binding powers, as is shown by the following examples. (with $a, b, c, \ldots$ as variables).

Were "a + b" with associative + an expression, "a + a + b" would represent one of its syntactic descendants.

Were "a - b" with non-associative

pression, " $a - \left( {a - b}\right)$ " would represent one of its syntactic descendants.

Were "a + b" and "c * d" expressions, with $\star$ having a greater binding power than + , "a + c * d" and "(a + b) * d" would represent expressions.

Note that, with "c+d" an expression, "a + (c+d) * (c+d)" is a syntactic descendant of "a + e * f"; it is also a syntactic descendant of "a + e * e". Note that, since syntactic descendants are formed by replacing each occurrence of a variable by the same expression, all syntactic descendants of "a + e * e" are of the form, colloquially described as "a sum, the last addendum of which is a square".

We leave to the reader to convince him self -in whatever way he likes- of the following.

Variable P occurs in $A\left( {B/P}\right)$ if $P$ occurs in both $A$ and $B$ and in no other case; any other variable Q occurs in $A\left( {B/P}\right)$ if Q occurs in $A$ ,or if $P$ occurs in $A$ and Q occurs in $B$ ,and in no other case.

1. The beginning of the syntax

For the sake of completeness we start our syntax with

Syntax 0: Any variable represents an expression.

With Syntax 0 as our only rule the process of taking syntactic descendants yields no new expres. sions. With $A$ an expression, so is A(Q/P): within an expression, the actual choice of variables is irrelevant, distinctness and sameness being their only relevant attribute.

More interesting is

Syntax 1: [P] represents an expression

With $[P]$ for $A$ , $A(A / P)$ yields $[{P}]$ , i.e. we can now generate an infinite number of new expressions, viz.

[P] ,[[P]] ,[[[P]]],...

Syntax 1 provides the only way of introducing a square bracket into an expression, and as a result square brackets occur in expressions in nicely nested pairs, each matching pair surround-ing an expression.

We proceed by extending our syntax with Syntax 2: P represents an expression which provides the only way of introducing the unary operator ? . In combination with Syn- tax 1 it yields syntactic descendants such as

[P], [P], [P] etc.

all by itself it yields the syntactic descendants $P,{77}P,{777}P,\ldots ,$

in which the convention that $\neg$ is right-associative -viz. that $7!P$ could be written as $7(7P)$ - makes the introduction of parentheses superfluous. Note that the convention of right- asso-ciativity corresponds to the order of the sub-stituation process that generated $7!P$ as ex-pression.

Our next four operators are symmetric and associative infix operators. The first two are introduced by

Syntax 3: $P \equiv Q$ and $P \neq Q$ represent expressions and, besides being symmetric and associative, $\equiv$ and $\neq$ are also mutually associative.

The mutual associativity means that $(P \equiv Q) \neq R$ , $P \equiv (Q \neq R)$ , and $P \equiv Q \neq R$ all represent the same expression. Together with their symmetry this means that in such a linear representation, the operands may be freely permuted and the operators may be freely permuted, all without any change in expression represented. By convention, $\equiv$ and $\ncong$ have the lowest binding power, whereas $\neg$ has the highest one: $\neg P \equiv Q$ and $(\neg P) \equiv Q$ represent the same expression, $\neg P \equiv Q$ and $\neg (P \equiv Q)$ represent different expressions.

Syntax 4: PvQ and PwQ represent expressions, and v and $\wedge$ are symmetric and associative.

By convention, $v$ and $\land$ have a smaller binding power than $\neg$ and a greater binding power than $\equiv$ and $\neq$ . Consequently, $\neg P \land Q$ and $(\neg P) \land Q$ represent the same expression, whereas $\neg (P \land Q)$ represents a different one; $PvQ \equiv R$ and $(PvQ) \equiv R$ represent the same expression, whereas $Pv(Q \equiv R)$ represents a different one.

Contrary to custom, we do not give $\land$ a greater binding power than $\lor$ ; we shall write $(P \land Q) \lor R$ or $P \land (Q \lor R)$ - which, for lack of mutual associativity represent different expressions - and do not regard $P \land Q \lor R$ as a linear representation of an expression.

Our syntax gives rise to two problems. The one is whether a finite string of variables and operators represents an expression; this question can be solved by a simple syntactic check. The other is: given two expressions, is the one a syntactic descendant of the other? The latter question is much harder to answer.

(See EWD863-22)

Dark expressions

We shall try to treat the development of the part of mathematics we are interested in as the development of (part of) a subset of expressions, the so-called "dark expressions". As will be shown in a moment, the rules of coherence of the dark subset are more subtle, the justification of one expression's darkness depending on the darkness of other ex- pressions.

Remark Again, the rules for darkness are somewhat arbitrary. It is, for instance, quite permissible to introduce such a rich collection for darkness that all expressions become dark. The general consensus among mathematicians, however, is that this would spoil the fun. The logicians call a definition of darkness such that all expressions are dark "inconsistent". (End of Remark.)

There are primarily two rules. The first and simple one could be called the Rule of Inheritance:

Rule of Inheritance: The syntactic descendants of a dark expression are dark.

The second one is much more complicated. It is known as Leibniz's Rule.

Leibniz's Rule: For expressions $A,B$ ,and $C$ ,and variable $R$ such that $\left\lbrack {B \equiv C}\right\rbrack$ is dark, either or neither of $A\left( {B/R}\right)$ and $A\left( {C/R}\right)$ is dark.

With [R] for A , we get

Leibniz's Corollary: For expressions $B$ and $C$ such that

$\left\lbrack {B \equiv C}\right\rbrack$ is dark ,either or neither of

[B] and [C] is dark .

In order to get started, a few syntactic descendants of $\left\lbrack {P \equiv Q}\right\rbrack$ are postulated to be dark. To begin with, the disjunction $v$ will be our only further operator.

Our first expression postulated to be dark is $\left\lbrack {P \equiv P \equiv Q \vee Q \equiv Q}\right\rbrack$ (0)

Let us now apply Leibniz's Rule with $\left\lbrack {P \equiv R}\right\rbrack$ for $A$ ,

These choices yield. $\begin{array}{l l} {[ P \equiv P \equiv Q \lor Q \equiv Q ]} & {\mathrm {f o r} [ B \equiv C ],} \ {[ P \equiv P ]} & {\mathrm {f o r} A (B / R), \mathrm {a n d}} \ {[ P \equiv P \equiv Q \lor Q \equiv Q ]} & {\mathrm {f o r} A (C / R).} \end{array}$

The first and the last one being dark on account of (0), Leibniz's Rule allows us to conclude the darkness of

$$ [ P \equiv P ] \tag {1} $$

(Normal mathematical parlance refers to the darkness of (1) by stating that the equivalence is reflexive.)

Let us now apply Leibniz's Corollary with

[\text{P} \equiv \mathrm{P}\;\text{for}\mathrm{B}\text{,and}]

These choices yield

$$ \begin{array}{l} [ P \equiv P \equiv Q \vee Q \equiv Q ] \ f o r [ B \equiv C ], \ [ P \equiv P ] \ f o r [ B ] \quad , a n d \ [ Q \vee Q \equiv Q ] \ f o r [ C ] \ \end{array} $$

The first two being dark on account of (o) and (1) respectively, Leibniz's Corollary allows us to conclude the darkness of

$$ [ Q \vee Q = 0 ] \tag {2} $$

(Normal mathematical parlance refers to the darkness of (2) by stating that the disjunction $\vee$ is idempotent.)

From the darkness of (1) we derive

Theorem 0: For any expressions $A,B$ ,and $C$ such that $\left\lbrack {B \equiv C}\right\rbrack$ is dark, and any variable $R$ ,

$$ [ A (B / R) \equiv A (C / R) ] $$

is dark.

Proof. Let $R'$ be a fresh variable - i.e., different from $R$ and not occurring in the expressions $A, B, C$ and $C$ . Then the choice

$$ [ A (B / R) \equiv A (R ^ {\prime} / R) ] \quad f o r A ^ {\prime} $$

yields

$$ \begin{array}{l} [ A (B / R) \equiv A (B / R) ] \quad f o r A ^ {\prime} (B / R ^ {\prime}), a n d \ [ A (B / R) \equiv A (C / R) ] \quad \mathrm {f o r} A ^ {\prime} (C / R ^ {\prime}). \ \end{array} $$

The first of these expressions, being a syntactic descendant of (1), is dark. Applying Leibniz's Rule (with ${A}^{\prime }$ for $A$ and ${R}^{\prime }$ for $R$ ) yields the con-

conclusion. (End of Proof.)

From the darkness of (1) we further derive

Theorem 1: If for any expressions $B$ and $C$ ,

Proof. [B=C=B=C] is dark, being a syntactic descendant of (1); on account of Leibniz's Corollary, either or neither of [B] and [C=B=C] is dark and, [B] being dark, we conclude that [C=B=C] is dark. Hence Leibniz's Corollary again - either or neither of [C] and [B=C] is dark; [C] being dark, the conclusion follows. (End of Proof.)

Leibniz's Corollary and Theorem 1 state together that any expression B such that [B] is dark, acts as the identity element for the equivalence as far as darkness is concerned. It is convenient to introduce a canonical representation for it, just as in arithmetic it is nice to have a zero instead of having to choose between 1-1, 2-2, 3-3, etc. To this end we extend our syntax with

Syntax 5: black is an expression

and postulate the darkness of

[black] (3)

Note that black is not a variable: it is an ex- pression in which no variable occurs. The intro- duction of black is nothing deep, it is just a convenience: we could have written instead "Funny ≡ Funny" under the proviso that the variable "Funny" is used nowhere else. We would have observed the darkness of

$$ [ P \equiv f u n n y \equiv P \equiv f u n n y ] \quad , $$

this being a syntactic descendant of (1); we would have rewritten this as

$$ [ P \equiv P \equiv f u n n y \equiv f u n n y ] $$

and eventually as

$$ [ P \equiv P \equiv b l a c k ] \tag {4} $$

the darkness of which expresses with Leibniz's Rule-, when parsed $[P\equiv (P\equiv black)]$ , that black is the identity element for the equivalence. When parsed $[P\equiv P\equiv black]$ ,(3) would have followed from (1), using Leibniz's Corollary.

Obviously, the darkness of (0) can never yield the darkness of a formula in which $v$ is ap- plied to two different arguments. For this we need something new; we postulate the darkness of

$$ [ (P \equiv Q) \vee R \equiv P \vee R \equiv Q \vee R ] \tag {5} $$

(Normal mathematical parlance refers to the darkness of (5) by stating that disjuncti. distributes over equivalence.)

Note that the postulated darkness of (5) is compatible with the postulated symmetry and associativity of $\equiv$ : no matter whether we parse $P \equiv Q \equiv S$ as $\left( {P \equiv Q}\right) \equiv S$ or as $P \equiv \left( {Q \equiv S}\right)$ ,in either case repeated application of (5) yields the dark expression $\left\lbrack {\left( {P \equiv Q \equiv S}\right) \vee R \equiv {PvR} \equiv QvR \equiv {SvR}}\right\rbrack .\left( {5}^{\prime }\right)$

From (5), we deduce the darkness of its syn- tactic descendant - substitute $P$ for $Q -$

$$ [ (P \equiv P) \vee R \equiv P \vee R \equiv P \vee R ] \quad , $$

and hence, using (4) twice, the darkness of

$$ [ b l a c k \vee R \equiv b l a c k ] \tag {6} $$

or, using (4) another time, the shorter

$$ [ b l a c k \vee R ] \quad . \tag {7} $$

We shall return to these properties of black and the disjunction later. We prefer to draw attention to a very different consequence of (5) first.

Theorem 2. For any expression $A$ that contains $\equiv$ and $\vee$ as only operators, there exists an expression $B$ such that

(i) $\left\lbrack {A \equiv B}\right\rbrack$ is dark. (ii) $B$ is black,or a term or a continued equivalence of different terms,where each term is a variable or a continued disjunction of different variables.

Proof. The proof is constructive in the sense that we show how to construct a $B$ for a given $A$ .

We start with expression $A$ . As long as our expression contains an $V$ with an equivalence as one of its operands, we distribute $V$ over $\equiv$ ; the result is a continued equivalence of disjunctions and variables or black. Here we have used (5).

By using (2) we can see to it that each of these disjunctions contains each variable at most once.

By using (4) we can see to it that the continued equivalence contains no duplicates. (End of Proof.)

By substituting in (5) Q for $R$ ,and applying

$$ [ (P \equiv Q) \vee Q \equiv P \vee Q \equiv Q ] \quad , \tag {8} $$

a formula which is of interest on account of the following theorem

Theorem 3 For any $A, B,$ and $C$ , such that $[A \vee B \equiv B]$ and $[B \vee C \equiv C]$ are dark, $[A \vee C \equiv C]$ is dark as well.

Proof. The darkness of $\left\lbrack {A{v}^{B} \equiv B}\right\rbrack$ allows us to replace in the dark $\left\lbrack {{BVC} \equiv C}\right\rbrack$ the $B$ by(A v B),yielding the equally dark $\left\lbrack {\left( {A{v}^{B}}\right) {v}^{C} \equiv C}\right\rbrack$ ,or equivalently $\left\lbrack {A{v}\left( {B{v}^{C}}\right) \equiv C}\right\rbrack$ . The darkness of $\left\lbrack {{BVC} \equiv C}\right\rbrack$ allows us to replace in the latter (BVC) by $C$ ,yielding the dark $\left\lbrack {A{VC} \equiv C}\right\rbrack$ . (End of Proof.)

Note. Hence, the darkness of $\left\lbrack {A \vee B \equiv B}\right\rbrack$ expresses a transitive relation between $A$ and $B$ ,read as "A implies "B" and written as $\left\lbrack {A \Rightarrow B}\right\rbrack ;\left( 2\right)$ tells us that implication is reflexive. (End of Note.)

Note that beyond Leibniz's Rule we used no more than the associativity of $v$ . In general, each associative operator yields in this fashion a transitive relation; it is, however, not always interesting. On account of (2) we conclude that implication is reflexive.

Our next postulated darkness of

$$ [ P \wedge Q \equiv P \equiv Q \equiv P \vee Q ] \tag {9} $$

defines the operator $\land$ ,the conjunction. By parsing it $\left\lbrack {\left( {P \land Q}\right) \equiv \left( {P \equiv Q \equiv P \vee Q}\right) }\right\rbrack$ ,and remembering the symmetry of $\equiv$ and $v$ ,we see that also

$\wedge$ is symmetric.

of Substituting $P$ for $Q$ in (g) yields the darkness

hence on account of (4) and (2)

$$ [ P \land P \equiv P ] \tag {10} $$

i.e. conjunction is said to be idempotent.

Substituting $Q \land R$ for $Q$ in (g) yields

$$ [ P \wedge (Q \wedge R) \equiv P \equiv Q \wedge R \equiv P \vee (Q \wedge R) ] $$

Applying (9) twice more yields

$$ \begin{array}{l} [ P \wedge (Q \wedge R) \equiv P \equiv Q \equiv R \equiv Q \vee R \equiv \ P \vee (Q \equiv R \equiv Q \vee R) ] \ \end{array} $$

which yields with (5) the darkness of

$$ \begin{array}{l} [ P \wedge (Q \wedge R) \equiv P \equiv Q \equiv R \equiv \ Q v R \equiv P v Q \equiv P v R \equiv \ \left. \begin{array}{l} P \vee Q \vee R \end{array} \right] \quad , \ \end{array} $$

which, together with the symmetry and associativity of $\equiv$ and $v$ allows us to conclude that $\land$ is associative as well.

Next we observe the darkness of the following ex- pressions: on account of (7)

$$ [ b l a c k \vee R ] $$

Hence on account of (9)

$$ [ (P \wedge Q) \equiv P \equiv Q \equiv P \vee Q) \vee R ] $$

Hence, on account of (5)

$$ [ (P \wedge Q) \vee R \equiv P \vee R \equiv Q \vee R \equiv P \vee Q \vee R ] $$

Hence, on account of (2)

$$ [ (P \land Q) \lor R \equiv P \lor R \equiv Q \lor R \equiv (P \lor R) \lor (Q \lor R) ] $$

and, finally, using (g) once more

$$ [ (P \land Q) \lor R \equiv (P \lor R) \land (Q \lor R) ] \tag {11} $$

(Normal mathematical parlance refers to the darkness of (11) by stating that the disjunction distributes over the conjunction.)

Deriving that, conversely, the conjunction distributes over the disjuncti on requires - regrettably- a bit more. To this purpose we observe the darkness of the following expressions: on account of (1)

$$ [ (P \land R) \lor (Q \land R) \equiv (P \land R) \lor (Q \land R) ] $$

Hence, on account of (g) - twice

$$ \begin{array}{l} [ (P \wedge R) \vee (Q \wedge R) \equiv \ (P \equiv R \equiv P v R) \vee (Q \equiv R \equiv Q v R) ] \ \end{array} $$

Hence, on account of (5) - numerous times -

$$ \begin{array}{l} [ (P \wedge R) \vee (Q \wedge R) ] = \ P \vee Q \equiv P \vee R \equiv P \vee Q \vee R \equiv \ R \vee Q \equiv R \vee R \equiv R \vee Q \vee R \equiv \ P _ {v} R v Q \equiv P _ {v} R v R \equiv P _ {v} R v Q v R ] \ \end{array} $$

Hence, on account of (2)

$$ \begin{array}{l} [ (P \wedge R) \vee (Q \wedge R) ] = \ P \vee Q \equiv P \vee R \equiv P \vee Q \vee R \equiv \ R \vee Q \equiv R \equiv Q \vee R \equiv \ P \vee R \vee Q \equiv P \vee R \equiv P \vee R \vee Q ] \ \end{array} $$

Hence, on account of (4)

$$ [ (P \land R) \lor (Q \land R) ] = $$

$$ P \vee Q \equiv R \equiv P \vee Q \vee R ] $$

and finally, once more on account of (9)

$$ [ (P \land R) \lor (Q \land R) \equiv (P \lor Q) \land R ] \tag {12} $$

And thus we have shown that conjunction distributes over disjunction.

Since (g) allows us to express any expression which is a syntactic descendant of $P \land Q$ as an expression not containing $\land$ , Theorem 2 can be generalized as "For any expression $A$ that contains $\equiv$ , $\lor$ , and $\land$ as only operators". In this sense the introduction of the conjunction yields us, after we have got the $\equiv$ and $\lor$ , nothing new.

The darkness of (4) expresses that black is the identity element of the equivalence. But it is more! Substitution of black for $\alpha$ in (9) establishes the darkness of

$$ [ P \land b l a c k \equiv P \equiv b l a c k \equiv P \lor b l a c k ] $$

which, on account of (4) and (6) yields the

$$ [ P \wedge b l a c k \equiv P ] \tag {13} $$

Hence, black is also the identity element of the conjunction. An identity element for the disjunction, however, is still missing, and it is here that we need the negation, introduced by poshulating the darkness of

$$ [ P \vee \neg Q \equiv P \vee Q \equiv P ] \tag {14} $$

$$ \begin{array}{l} \mathrm {S u b s t i t u t i n g} P \mathrm {f o r} Q \mathrm {i n (1 4) a n d s i m p l i f y i n g} \ \mathrm {u s i n g (2) a n d (4) y i e l d s t h e d a r k n e s s o f} \ [ P v ] \end{array} $$

which is essentially our first dark expression not being an equivalence.

substituting black for ① in (14) yields to

$$ [ P v, b l a c k \equiv P v, b l a c k \equiv P ] $$

which, with (7) and (4) yields the darkness of

$$ [ P \vee \neg b l a c k \equiv P ] \quad , $$

in other words: if black is the identity element of the disjunction we were looking for. Calling it white, we get

$$ [ w h i t e \equiv \neg b l a c k ] \tag {16} $$

$$ [ P \vee \mathrm {w h i l e} \equiv P ] \tag {17} $$

substituting white for $P$ in (14) yields to begin with the darkness of

$$ [ w h i t e \vee \neg Q \equiv w h i t e \vee Q \equiv w h i t e ] \quad , $$

which, thanks to (17), yields the darkness of

$$ [ \neg Q \equiv Q \equiv \mathrm {w h i t e} ] \tag {18} $$

Substituting in (18) 7① for ② yields the

$$ [ \neg \neg Q \equiv \neg Q \equiv w h i l e ] $$

and after rewriting (18) as

$$ [ Q \equiv \neg Q \equiv \mathrm {w h i t e} ] \quad , $$

we deduce the darkness of

$$ [ 7 7 Q \equiv Q ] \tag {19} $$

i.e. negation is its own inverse.

Substituting $P \equiv Q\;$ for $Q$ in (18) yields

$$ [ \neg (P \equiv Q) \equiv P \equiv Q \equiv w h i t e ] $$

which, with (18) once more yields the darkness of

$$ [ \neg (P \equiv Q) = \neg P \equiv Q ] \tag {20} $$

which in normal mathematical parlance expresses that the unary negation and the binary equivalence are mutually associative: our decision that negation would have a greater binding power than equivalence is as far as darkness is concerned irrelevant.

For the sake of completeness we define $\neq$ by postulating the darkness of

$$ [ (P \neq Q) \equiv \neg P \equiv Q ] \quad , \tag {21} $$

which allows us to write down

$$ [ (P \neq Q) \land R \equiv P \land R \neq Q \land R ] \tag {22} $$

-i.e. conjunction distributes over the difference -

The proof of the darkness of (22) is left as an exercise to the reader, as well as that of the darkness of

$$ \begin{array}{l} [ P \vee (P \wedge Q) \equiv P ] (23) \ [ P \land (P \lor Q) \equiv P ] (24) \ [ \neg (P \land Q) \equiv \neg P \lor \neg Q ] (25) \ [ \neg (P \lor Q) = \neg P \land \neg Q ] (26) \ (S e e E W D 8 6 3 - 2 2) \ \end{array} $$

We are now in a position to generalize theorem 2. We first generalize our nomenclature. In very old days, a product was always a product of 2 or more factors; in the mean time we know that it often helps to regard a single number as "a product containing 1 factor" and to regard the number 1 -the identity element of the multiplication - as "the empty product".

Similarly we are willing to consider $P$ and black as specific instances of continued equivalences. viz. with 1 and with 0 terms respectively. And, similarly, we regard $P$ and white as continued disjunctions. The new theorem 2 is

Theorem 2'. For any expression $A$ , containing only the operators $\equiv, \vee, \wedge,$ and $\neg$ , there exists a unique expression $B$ such that

(i) $\left\lbrack {A \equiv B}\right\rbrack$ is dark (ii) $B$ is a continued equivalence of different continued disjunctions of different variables.

With $k$ variables,there are precisely ${2}^{k}$ disjunctions of different variables ("without duplici- cates",I mean). With $k$ variables,there are therefore precisely ${2}^{\left( {2}^{k}\right) }$

different expressions satisfying constraint (ii) of Theorem 2' on B.

The demonstration that for given $A$ , $B$ is unique, is omitted, though its uniqueness is a very good thing. If there were two different $B$ and ${B}^{\prime }$ , we would deduce from the darkness of $\left\lbrack {A \equiv B}\right\rbrack$ and $\left\lbrack {A \equiv {B}^{\prime }}\right\rbrack$ the darkness of $\left\lbrack {B \equiv {B}^{\prime }}\right\rbrack$ , which for different $B$ and ${B}^{\prime }$ would lead to the darkness of [white],the latter being as dark as a syntactic descendant of $\left\lbrack {B \equiv {B}^{\prime }}\right\rbrack$ .

Proof Let us call a continued equivalence without duplicates of continued disjunctions without duplicates in "equivalence-normal form". With $B$ and $B'$ in equivalence-normal form and different, $[B \equiv B']$ is as dark as an expression $[C]$ , with $C$ in equivalence-normal form and different from black. We shall show that with $C$ in equivalence normal form and different from black, $[C]$ has a syntactic descendant as dark as [white].

The proof is by mathematical induction over the number of variables occurring in $C$ . If no variables occur in $C$ , the only admissible

form of $C$ is white , and the conclusion holds.

If $k + 1$ variables occur in $C$ , let $R$ be a variable occurring in $C$ . If $R$ occurs in all terms of the continued equivalence, $[C(\text{white}/R)]$ is dark if $[C]$ is; on account of (17), it is as dark as an expression in equivalence normal form that differs from black but contains only $k$ variables. If $R$ does not occur in all terms of the continued equivalence $C$ , consider $[C(\text{black}/R)]$ : it is dark if $C$ is, and on account of (6) it is as dark as an expression in equivalence-normal form that differs from black but contains at most $k$ variables - viz. the continued equivalence for the terms in $C$ not containing $R$ . (End of Proof.)

Theorem 4. If [white] is dark, [A] is dark for any expression $A$ .

Proof If [while] is dark, so is

$$ [ w h i l e \equiv b l a c k ] $$

on account of (7) we have the darkness of

$$ [ A \vee b l a c k ] \quad ; $$

with Leibniz's Rule we have the darkness of

$$ [ A \cdot v. w h i t e ] $$

and with (17) that of

$$ [ A ] \quad . $$

(End of Proof.)

EWD863-6:

We could have been much more explicit about the relation between expressions and their linear representations, explaining, for instance, how to each occurrence of a variable in an expression corresponds an occurrence of that same variable in a linear representation of that expression, or how substitution corresponds in the realm of representations to a string manipulation.

We did not do so because we did not want to do so. Such explanations can be found in all texts on symbolic logic; these texts, however, serve a different purpose.

In the sequel, we let it be implicitly understood that a linear representation stands for the expression. it represents: we shall write "if $\left\lbrack {B \equiv C}\right\rbrack$ is dark" instead of "if the expression represented by

EWD 863-19:

Two further dark expressions should have been mentioned , viz.

$$ [ P \wedge w h i t e = w h i t e ] (2 7) $$

$$ [ P \land \neg P \equiv \mathrm {w h i t e} ] \tag {28} $$

We should also have mentioned that (23) and (24) are known as the Laws of Absorption, and that

(25) and (26) are known as the laws of Augushus de Morgan. They reflect the nature of the symmetry between disjunction and conjunction.

Finally we summarize eight different expressions for the implication -see EWD863-13-

$$ \begin{array}{l} [ (P \Rightarrow Q) \equiv P \vee Q ] \ [ (P \Rightarrow Q) \equiv P \vee Q \equiv Q ] \ [ (P \Rightarrow Q) \equiv P \wedge Q \equiv P ] \ [ (P \Rightarrow Q) \equiv (P \equiv Q) \vee Q ] \ [ (P \equiv Q) \equiv (P \equiv Q) \vee \neg P ] \ [ (P \Rightarrow Q) \neq (P \neq Q) \land P ] \ [ (P \Rightarrow Q) \neq (P \neq Q) \land \neg Q ] \ [ (P \Rightarrow Q) \equiv (\neg Q \Rightarrow \neg P) ] \ \end{array} $$

We shall use the implication sparingly, and only where it does not hurt that the implication is neither symmetric, nor associative.

(To be continued.)

Plataanstraat 5

5671 AL NUENEN

The Netherlands

13 October 1983

prof. dr. Edsger W. Dýksta

Burroughs Research Fellow