Mainly on our use of the predicate calculus (Draft Ch.2)

Mainly on our use of the predicate calculus (DraF 1h.2)

The purpose of this chapter is threefold: to introduce a collection of formulae that will be used throughout the book, to show how we shall use those formulae, and to explain our notational conventions.

In the following, $X, Y,$ and $Z$ will be used as "predicate variables", and $A, B,$ and $C$ as "predicate expressions" or "predicates" for short. Predicate variables are the simplest examples of predicates; operators -for instance the infix operator $\equiv$ for what is called the "equivalence"- allow us to construct "new" predicates - such as $A \equiv B-$ from "existing" ones.

The introduction of an infix operator always raises several questions. Firstly, it connects two operands, but is their order relevant? For the equivalence the answer is that it is symmetric, i.e. that we never need to distinguish between $A \equiv B$ and $B \equiv A$ . Secondly, what to do with the syntactically ambiguous expression $A \equiv B \equiv C$ : should it be parsed as $(A \equiv B) \equiv C$ or as $A \equiv (B \equiv C)$ , or is the distinction irrelevant? For the equivalence the answer is that it is associative, i.e. that we never need to distinguish between $(A \equiv B) \equiv C$ and $A \equiv (B \equiv C)$ , and that, hence, we are free to omit the parenthesis

pairs (or to introduce them as we see fit).

We can summarize symmetry and associativity of the equivalence in words by stating that the equivai- lence is defined on finite bags of predicates. (Bags are unordered collections that may contain dupli- cates; they are sometimes referred to as "multisets," though we would prefer to refer to sets as "unibags".)

Twice in the above we have called the distinction between two formulae "irrelevant", and before proceeding we would like to be a bit more precise about the question "irrelevant in what sense?" A major part of the development of a mathematical theory consists in establishing new formulae from the already established ones. We call the distinction between two formulae "irrelevant" if a simple syntactic analysis suffices to show that they are equally established. (The fact that the notion "irrelevant" is thus as relative as the notion "simple" need not concern us here.)

For formulae in predicates we shall mainly use two inference rules, referred to as "Rule of Instantiation" and "Rule of Leibniz" respectively.

Rule of Instantiation Let P.A stand for the result of substituting expression A for variable Z in formula P.Z; then P.A is an established formula

for any $A$ if $f \cdot z$ is an established formula.

Calling $\mathrm{p.A}$ a "syntactic descendant" of p.z, we can briefly state, that all syntactic descendants of an established formula are established as well.

Rule of Leibniz Let $f,A$ and $f,B$ stand for the results of substituting expressions $A$ and $B$ respectively for variable $Z$ in formula $f.Z$ ; then $f.A$ and $f.B$ are equally established if $[A\equiv B]$ is an established formula.

An immediate consequence of the Rule of Instantiation all by itself is that, since any predicate variable is a special instance of a predicate expression, the variables occurring in established formulae are completely arbitrary: establishing, for instance, $[X \equiv X]$ would amount to exactly the same thing as establishing $[Y \equiv Y]$ .

The two rules of inference together allow us to capture the associativity of the equivalence by postulating -with a lot of subsequently superfluous parentheses

\left[ \left(\left(X \equiv Y\right) \equiv Z\right) \equiv (X \equiv (Y \equiv Z)) \right]

to be an established formula.

Indeed, let $F$ be a formula that, for some

A, B, and C, contains the -fully parenthesized—subexpression $(\left(A \equiv B\right) \equiv C)$ . The Rule of Instantiation then allows us -if so desired in three steps-- to establish on account of (0)

(1) $[((A \equiv B) \equiv C) \equiv (A \equiv (B \equiv C))]$

Next we transform $F$ into $F^{\prime}$ by replacing in F an occurrence of the subexpression $(\left(A\equiv B\right)\equiv C)$ by $(A\equiv (B\equiv C))$ . This means that, for some $\beta ,F$ and $F^{\prime}$ are of the forms $p.(A\equiv B)\equiv C)$ and $p.(A\equiv (B\equiv C))$ respectively. The Rule of Leibniz then states that, since (1) is an established formula, $F$ and $F^{\prime}$ are equally established.

The moral of the story is that, if we have a fully parenthesized expression with many equivalences, we can move the parenthesis pairs freely around, and so it is much simpler not to insert them in the first place but to remember, instead, that the equivalence is associative.

Remark. Were this a treatise on logic, we would probably have proved the above moral for all expressions by induction over the grammar. Since this is not a treatise on logic, we let the moral suffice. (End of Remark.)

Adopting immediately the convention of omitting

superfluous parentheses, we can now capture the symmetry of the equivalence by postulating that

[ X \equiv Y \equiv Y \equiv X ] \tag {2}

is an established formula.

As a consequence of (2) and the Rule of Leibniz, $f_{}(X \equiv Y)$ and $f_{}(Y \equiv X)$ are equally established. With $f_{}Z$ of the form $[X \equiv Y \equiv Z]$ , $f_{}(Y \equiv X)$ reduces to the established (2), and hence we have established $f_{*}(X \equiv Y)$ , i.e.

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

Next, with $\rho .Z$ of the form $[X\equiv Z\equiv Y]$ , $\rho .(Y\equiv X)$ reduces to the established (3), and hence we have established $\rho .(X\equiv Y)$ , i.e.

(4) [ X \equiv X \equiv Y \equiv Y ]

or, with the special variable Y introduced for this purpose and the Rule of Instantiation,

(4 ^ {\prime}) [ X \equiv X \equiv \overline {{Y}} \equiv \overline {{Y}} ] .

Variable $\bar{Y}$ is a local gimmick of the current argument. We promise that we shall never sub- stitute anything for it. For that reason we would rather not see it in our formulae, something we can achieve by giving the expression $\bar{Y} \equiv \bar{Y}$ a name, "true" say; we can capture this naming

convention by postulating

(5) [true $\equiv \overline{Y} \equiv \overline{Y}\rbrack$

to be an established formula. From (41) and (5) we establish with the Rule of Leibniz

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

In view of the little we have used, (6) is a fascinating formula: parsing it as $\left\lbrack {X \equiv \left( {X \equiv \text{true}}\right) }\right\rbrack$ , we conclude from it (in combination with the two inference rules) that true acts as identity element of the equivalence.

Remark. It is not difficult to show that an operator with a left identity element and a right identity element has a unique identity element. The equiv- valence being symmetric, we can conclude that true is the identity element of the equivalence. (End of Remark.)

Though (0) and (2) as established formulae capture the notions of associativity and symmetry of the equivalence, we shall rarely refer to them in the sequel. The reader will be supposed to know and remember that the equivalence -like a few other operators to be introduced shortly- is associative and symmetric, and we shall freely reorder and regroup the operands of such operators as the need arises.

In a similar vein we shall often refrain from ex- plicitly spelling out an instantiation such as (1). It is more likely that we shall refer to the formula to which the Rule of Instantiation is to be applied, if necessary with the substitution to be performed: instead of appealing to (1), we might give the hint "on account of (0) with $X,Y,Z\coloneqq A,B,C$ ", the latter being a code for the substitution to be performed.

The above conventions greatly reduce the lengths of our proofs -reducing half a page or so to perhaps a single line - while neither impairing the rigour of the argument, nor posing a puzzle to the reader.

Remark. In all but the simplest applications of the Rule of Instantiation, the author is almost morally obliged to mention the substitution to be performed. In the presence of operators defined on bags of operands, which occur in a hence irrelevant order, the question of whether one given formula is a syntactic descendant of another given formula seems in general not easy to answer at all. (End of Remark.)

Remark. There is little point in stating explicitly that the equivalence is transitive in the sense that for established $\left\lbrack {A \equiv B}\right\rbrack$ and $\left\lbrack {B \equiv C}\right\rbrack ,\left\lbrack {A \equiv C}\right\rbrack$ is es-

tablished as well: the fact follows -in more than one way!- from the Rule of Leibniz. (End of Remark.)

Finally, we derive in detail yet two further consequences of (6).

With $p. z$ of the form $[X \equiv Z]$ , we conclude from (6) and the Rule of Leibniz that $p. x$ is as established as $p. (X \equiv \text{true})$ ; since the latter reduces to the established (6) again! - we have established $p. x$ , i.e.

[\left\lbrack {X \equiv X}\right\rbrack ]

With $\rho .Z$ of the form [2], we conclude from (6) and the Rule of Leibniz that $\rho$ .true is as established as $\rho .(X\equiv X)$ ; since the latter reduces to the established (7), we have established

(8) [true]

So much for the equivalence.

The time has come to introduce our next infix operators: $v$ -called the "disjunction"and $∧$ -called the "conjunction". They, too, are symmetric and associative, and in the sequel the reader is supposed to know and remember this,i.e. we feel again free to omit superfluous

parenthesis pairs and to reorder and regroup their operands as we see fit.

With the introduction of a second infix oper- ator -the disjunction say- we are immediately faced with the question what to do about expressions such as $X \vee Y \equiv Z$ : do we admit it, and, if so, should it be parsed as $(X \vee Y) \equiv Z$ or as $X \vee (Y \equiv Z)$ , or is the distinction irrelevant?

In this case, the distinction is relevant, and we introduce the convention that $X \vee Y \equiv Z$ should be parsed as $(X \vee Y) \equiv Z$ , a convention that is expressed by stating that " $V$ has a greater binding power than $\equiv$ ". (Note that "binding power" is a purely syntactic notion: its introduction allows the omission of some otherwise necessary parenthesis pairs.)

Similarly we introduce the convention that $∧$ has a greater binding power than $\equiv$ , i.e. $X ∧ Y \equiv Z$ should be parsed as $(X ∧ Y) \equiv Z$ .

What about $X ∧ Y \lor Z$ ? Some authors admit it and resolve the syntactic ambiguity by giving $∧$ a greater binding power than v . We shall not do so since such a notational convention would destroy an otherwise pleasing

symmetry.

Remark. Among the formulae that can be established is, for instance,

\begin{array}{l} [ (X \vee Y) \wedge (Y \vee Z) \wedge (Z \vee X) ] \equiv \ (X \wedge Y) \vee (Y \wedge Z) \vee (Z \vee X) ] , \ \end{array}

a formula that would lose much of its "beauty" if we removed the parentheses from its second line. Our objection is, however, more profound. Electronic engineers usually give conjunction a greater binding power than disjunction; we have met many who -in their notation!- would equate $X\wedge (Y\vee Z)$ without hesitation to XYvZ, but were very uncertain whether XYvZ could be equated to $(X\vee Z)\wedge (Y\vee Z)$ . In other words, they did not know that the disjunction distributes as well over the conjunction as the conjunction distributes over the disjunction. For this strange observation, their asymmetric notation is a plausible explanation. (End of Remark.)

As a result of our refusal to give v and ^ different binding powers, we shall not admit X Y V Z (nor its syntactic descendants).

A next syntactic convention is required for unary operators, of which we introduce one,

viz. $¬$ ,called the "negation". We use it as prefix operator with the highest binding power, i.e. $¬ X \vee Y,¬ X ∧ Y$ ,and $¬ X \equiv Y$ should be parsed as $\left( {¬ X}\right) \vee Y,\left( {¬ X}\right) ∧ Y$ ,and $\left( {¬ X}\right) \equiv Y$ respectively.

For the sake of completeness we mention $≠$ , the "nonequivalence". Like the equivalence, it is symmetric and associative, and we give it the same low binding power as the equivalence because $≠$ and $\equiv$ are also mutually associative, i.e.

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

is an established formula. In contrast to the equivalence, which is required for the application of the Rule of Leibniz, the nonequivalence is used rarely.

Remark. The convention that negation has a greater binding power than (non)equivalence is of limited "relevance" in the sense that - as will transpire later-- the unary $¬$ and the binary $\equiv$ (and ≠) are mutually associative, i.e. we can establish

[ ¬ (X \equiv Y) \equiv (¬ X) \equiv Y ] \qquad a n d

[ ¬ (X ≠ Y) \equiv (¬ X) ≠ Y ]

Despite this irrelevance we shall continue to parse ${7x} \equiv y$ as $\left( {7x}\right) \equiv y . (\operatorname{End of Remark.})$

The introduction of a name. False say, for the expression ? true :

(q) [false ≡ ¬true]

concludes for the time being our notational con

Since the pairs of square brackets pose no syntactic problems -indeed: as the reader has probably guessed, opening and closing brackets are to be paired as usual - the reader is almost prepared to read formulae (2.0) through (2.10) from the Appendix of this chapter.

Some preliminary remarks, however, seem appropriate. By now, the reader may have begun to wonder what our predicates "really" are and what our square brackets "really mean". Well, these are philosophical questions, which we therefore prefer to leave unanswered. But just in case some readers definitely prefer to have a "model" in mind, in terms of which they can "interpret" our formulae, we are willing to provide one.

Our willingness to provide that model does not imply that we promote it. On the contrary, we suggest that, once that model has helped those readers over the threshold of unfamiliarity, they "forget" it

as soon as possible and try to appreciate our proofs as manipulations of uninterpreted formulae. We have two compelling reasons for that suggestion.

The one reason is that we shall manipulate formulae that are quite manageable when treated as strings of characters but baffle the imagination when interpreted in terms of the model. The other reason is that the most central concept of that model turned out -somewhat to our surprise!- to play no role at all in the major part of our theory: in fact, we only need it in the chapter that links our theory to operational considerations.

The model consists in viewing our predicates as boolean-valued functions defined on some non-empty domain and by applying the operators point-wise, i.e. -in the usual parlance- :

$X \equiv Y$ is a boolean function that is true wherever $X$ and $Y$ have equal values and false everywhere else;

$X ≠ Y$ is a boolean function that is true everywhere $X$ and $Y$ have different values and false everywhere else;

$X \vee Y$ is a boolean function that is false wherever both $X$ and $Y$ are false and true everywhere else;

$X ∧ Y$ is a boolean function that is true wherever both $X$ and $Y$ are true and false everywhere else;

$?X$ is a boolean function that is true wherever $X$ is false and false everywhere else.

In this model, true and false are used to denote either the boolean constants or the constant functions on the domain. (We could make a notational distinction between the two concepts, but it is much more convenient not to do so.)

Finally, in this model the square brackets should be interpreted as universal quantification over all points of the domain, e.g. $[A \equiv B]$ expresses that $A \equiv B$ is true in all points of the domain, i.e. that in all points of the domain $A$ and $B$ have equal values, i.e. that $A$ and $B$ are the same boolean function on the (same) domain, a circumstance sometimes expressed by $A = B$ . We shall not do so.

Reason. For functions $f$ and $g$ on the same domain "for all $x$ in the domain: $f.x = g.x$ " is usually rendered by " $f = g$ ". In that convention, the universal quantification over $x$ is in " $p = g$ " more or less indicated by omitting at both sides the argument. But we have left the argument unmentioned to start with! Therefore, to justify $A = B$ as shorthand for $[A \equiv B]$ , we would have to stress the difference between $\equiv$ and

$=$ by adjoining the latter with a universal quanti-. fication, the scope of which is not indicated. (What about $A = B \lor \exists u A = B = C$ ?)

Our experience with such implied universal quantifica-tions is so unfortunate in the case of boolean-valued operands that we have decided to continue to write the perfectly clear $[A\equiv B]$ . Who doubts the wisdom of this decision should study the philosophers' hassle about "the material implication" versus "the logical implication". (End of Reason.)

By way of intermezzo, we shall now derive a number of the formulae (2.0) through (2.10). We call this an intermezzo, firstly, because this monograph is not a treatise on logic and, secondly, because this calculus can be founded in so many - perhaps even better - ways that we must have special reasons for presenting the following derivation.

Our main reason is that we regret the traditionally central role that the implication plays in such deriva-tions, a role it plays at the expense of the equivai- valence to the extent that the equivalence, denoted by $\Leftrightarrow$ instead of by $= \equiv$ and pronounced as "if and only if", is viewed as a mere abbreviation of mutual implication. The predominance of that view is truly regrettable because it has given rise to whole generations of mathematicians for whom it has become a second nature to prove each equivalence by showing that the one side implies

the other and the other way round, and whose proofs are as a result often twice as long as necessary. (A subsequent complication is that their proofs of the individual implications are frequently encumbered by perfectly avoidable "Reductiones ad Absurdum.") The consequences of the central role of the implication seem worse than mere clumsiness: the discovery that almost all of these mathematicians are unaware of the associativity of the equivalence forced upon us the conclusion that their vision of that logical operator has truly been obscured.

Another reason for doubting the wisdom of giving the implication such a central role to play is that of all the usual infix operators it is precisely the only one that is neither symmetric nor associative, a circumstance that makes formulae expressed in it less easy to manipulate. As a result it does not seem to provide a basis for a convenient and flexible calculus. This intermezzo is included with the intention of increasing the reader's appreciation of such simple properties as symmetry and associativity; at the same time it may teach him some new useful formulae or shed a new light on formulae he already knows.

The derivation starts with the introduction of $\equiv$ , postulated to be symmetric and associative, and of the expression named true, as

in formulae (0) through (8).

Next we introduce the disjunction $\vee$ , also postulated to be symmetric and associative. Furthermore the disjunction is postulated to be idempotent, i.e.

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

and to distribute over the equivalence, i.e.

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

From (11) we derive,by substituting $X$ for $Y$ , followed by two applications of (6) - once with

(12) [true v Z ≡ true]

i.e. true is also the zero element of the disjunction.

Next we introduce the conjunction $∧$ by defining it by the postulate -unofficially known as "The Golden Rule" -

(13) $[X \wedge Y \equiv X \equiv Y \equiv X \vee Y]$

From the symmetry of the equivalence and (13) we deduce that the conjunction is as symmetric as the disjunction. From (13) with $X := Y$ we deduce

[ X \wedge X \equiv X \equiv X \equiv X \vee X ] ,

i.e. the conjunction is as idempotent as the disjunctio. Hence, in view of (10)

(1 4) [ X \wedge X \equiv X ]

Next, we shall show that the conjunction as defined by (13) is as associative as the disjunctio. We establish in succession: from (7) with $X:= X ∧ (Y ∧ Z)$

[ X \wedge (Y \wedge Z) \equiv X \wedge (Y \wedge Z) ] ;

hence, from (13) with $X,Y \mathrel{\text{:=}} Y,Z$

[ X \wedge (Y \wedge Z) \equiv X \wedge (Y \equiv Z \equiv Y \vee Z) ];

hence, from (13) with $Y \mathrel{\text{:=}} Y \equiv Z \equiv Y \vee Z$

[ X \wedge (Y \wedge Z) \equiv X \equiv Y \equiv Z \equiv Y \vee Z \equiv X \vee (Y \equiv Z \equiv Y \vee Z) ];

hence, from (11) - repeatedly- and rearranging terms

\begin{array}{l} [ X \wedge (Y \wedge Z) \equiv X \vee (Y \vee Z) \equiv \ X \equiv Y \equiv Z \equiv Y \vee Z \equiv X \vee Y \equiv X \vee Z ] \ \end{array}

Since the second line of the above is symmetric in $X, Y$ , and $Z$ , so is the first line. Exploiting this fact and the symmetry of dis- and conjunction, we get

\begin{array}{l} [ X \wedge (Y \wedge Z) \equiv (X \wedge Y) \wedge Z \equiv \ X \vee (Y \vee Z) \equiv (X \vee Y) \vee Z ] , \ \end{array}

which neatly expresses that conjunction is as associative as disjunctio. (Note that in this derivation we needed that v distributes over ≡ .)

We leave to the reader to verify that the Rules of Absorption - see (25) in Appendix follow rather directly from the Golden Rule and the idempotence. More interesting are the distributive rules.

With (7) and (13), we establish

[ (X ∧ Y) \lor Z \equiv (X \equiv Y \equiv X \lor Y) \lor Z ]

hence, with (11) - repeatedly - and (10) with $x \mathrel{\text{:=}} 2$

[ (X \wedge Y) \vee Z \equiv X \vee Z \equiv Y \vee Z \equiv X \vee Z \vee Y \vee Z ] _ {i}

hence, with (13) with $X,Y\coloneqq X\vee Z,Y\vee Z$

(15) $\left[(X \wedge Y) \vee Z \equiv (X \vee Z) \wedge (Y \vee Z)\right]$ ,

i.e. the disjunction distributes over the conjunction as well.

To demonstrate at this stage that, conversely, the conjunction distributes over the disjunction, is possible, but more laborious. Because later - i.e. after the introduction of the negation- a much shorter argument can be given, we now give only a sketch. In

(x \wedge z) \vee (Y \wedge Z)

the conjunctions are eliminated with (13). Next, $v$ is distributed as much as possible over $\equiv$ ; the result is an equivalence of 9 terms, which are disjunctions. After simplification of the terms with

(10) - the idempotence of $v - 6$ of the 9 terms cancel according to (6), and we are left with

X \vee Y \equiv Z \equiv X \vee Y \vee Z

which on account of (13) equivales ${\left( X \vee Y\right) }^{ ∧ }Z$ .

Finally we establish from (13) with ${Y}_{i} =$ true and (16) $\left\lbrack {X ∧ \text{true} \equiv X}\right\rbrack$ .

i.e. true is the identity element of the conjunction as well. So much for the introduction of the conjunction.

Next we introduce - again in terms of $v$ and $\equiv -$ the negation by

(17) $[X \vee Y \equiv X \vee Y \equiv X]$

From (17) with $Y := \text{true}$ , (12) and (6) we derive

[ X \vee ¬ \text {t r u e} \equiv X ]

i.e. we have found the identity element of the disjunction, which deserves a name, false say. With

(18) [false ≡ ¬true]

we have derived

(19) $\left\lbrack {X \vee \text{false} \equiv X}\right\rbrack$

From (13) with $Y \coloneqq$ false, and (19) we establish

(20) $\left\lbrack {X ∧ \text{false} \equiv \text{false}}\right\rbrack$

i.e. false is also the zero element of the conjunction.

From (17) with $Y_{i} = X$ and (10), we get

[XY]

From (17) with $X, Y \coloneqq \text{false}, X$ we get

[ \text {f a l s e} v \cdot X \equiv \text {f a l s e} v X \equiv \text {f a l s e} ] ;

two applications of (19) yield

(22) $\left\lbrack {-X \equiv {X}^{ = }\operatorname{false}}\right\rbrack$

Combining (22) "as is" and (22) with $X \mathrel{\text{:=}} 7X$ ,we get

(23) $\left\lbrack {{77} \times \equiv X}\right\rbrack$

i.e. negation is its own inverse.

From (22) with $X \mathrel{\text{:=}} X \equiv Y$

[ ¬ (X \equiv Y) \equiv X \equiv Y \equiv \mathrm {f a l s e} ]

and (22) once more we get

(24) $[i(X\equiv Y)\equiv iX\equiv Y]$

With $X,Y \mathrel{\text{:=}} 7{Y}_{1}X , $ (17) yields

[ ¬ Y \vee ¬ X \equiv ¬ Y \vee X \equiv ¬ Y ]

this yields in combination with (17)

[ ¬ Y \vee ¬ X \equiv ¬ Y \equiv X \equiv X \vee Y ];

with (24) we get

[ ¬ Y \vee ¬ X \equiv ¬ (Y \equiv X \equiv X \vee Y) ]

and with the Golden Rule

(2 5) [ ¬ X \vee ¬ Y \equiv ¬ (X \wedge Y) ]

ie one of the laws of Augustus de Morgan; his other law immediately follows with the aid of (23).

The Golden Rule is symmetric in $\vee$ and $\wedge$ ; de Morgan's Laws and the fact that negation is its own inverse yield another way of exploiting the symmetry between them. It is, for instance, now a simple matter to derive from (15) that, conversely, conjunction distributes over conjunction.

In order to prepare the reader for another appreciation of The Golden Rule, we make a small excursion about associative operators in general. Denoting - for brevity's sake some operator by juxtaposition , its associativity is expressed by

(a b) c = a (b c).

The purpose of this excursion is to point out that each associative operator gives rise to two transitive relations, which are identical if the associative operator is symmetric. For the

purpose of this excursion we denote such a relation by and define it with having the lowest binding power - by

(2 7) a ≤ b \equiv a b = b

(If the associative operator is such that, seen as equation, ${ab} = b$ does not have interesting solutions,the corresponding relation is not very interesting either.)

Transitivity of means that if $a ≤ b$ and $b ≤ c$ are given,asc holds as well. According to (27)

\begin{array}{l} (2 8) a b = b a n d \ (2 9) b c = c \ \end{array}

have been given. We now observe in succession:

\begin{array}{l} a c = a (b c) {\mathrm {o n} a c c o u n t o f (2 9) } \ a (b c) = (a b) c {(2 6) } \ (a b) c = b c {o n a c c o u m t o p (2 8) } \ b c = c {(2 g) } \ \end{array}

Combining these results, we deduce $a = c$ ,i.e.

Note. Our conclusions "on account of" (2g) and (28) respectively are essentially an appeal to the Rule of leibniz, be it in a different context. (End of Note.)

Exploiting the associativity of the disjunction we can define, analogously to (27), for predicates the operator $⇒$ -called the "implication"

[ (X ⇒ Y) \equiv X \vee Y \equiv Y ] \tag {30}

By an argument completely analogous to the above, we then find that the implication is transitive in the sense that if $\left\lbrack {A ⇒ B}\right\rbrack$ and $\left\lbrack {B ⇒ C}\right\rbrack$ are established, $\left\lbrack {A ⇒ C}\right\rbrack$ can be established as well.

The Golden Rule states that

[ (X ⇒ Y) \equiv X ∧ Y \equiv X ]

with $X,Y\coloneqq Y,X$ and the symmetry of $\wedge$ (31) yields

[ (Y ⇒ X) \equiv X ∧ Y \equiv Y ]

i.e. but for an interchange of the arguments, the disjunction and the conjunction give rise to the same transitive relation.

We mention a further consequence of The Golden Rule. Suppose that we would like to establish, for some $A$ and $B$ , $[A \equiv B]$ . Thanks to The Golden Rule, this amounts to establishing $[A ∧ B \equiv A \lor B]$ , which can be achieved by establishing for some $C$ both

$\left\lbrack {A ∧ B \equiv C}\right\rbrack$ and $\left\lbrack {A \vee B \equiv C}\right\rbrack$ . Choosing for $C$ for instance $A$ ,our proof obligations become $\left\lbrack {A ∧ B \equiv A}\right\rbrack$ and $\left\lbrack {A \vee B \equiv A}\right\rbrack$ ,i.e. $\left\lbrack {A ⇒ B}\right\rbrack$ and $\left\lbrack {B ⇒ A}\right\rbrack$ respectively. In words: equivalence may be proved by proving mutual implication.

Before making more use of the implication we had better decide its relative binding power: we give it a greater binding power than $\equiv$ and ≠, but a smaller binding power than v, ∧ and 7 . In terms of the implication, we can now rewrite the rules of absorption as

[ X ∧ Y ⇒ X ]

and

[ X ⇒ X \vee Y ]

respectively.

We have mentioned earlier that our predicates may be modelled by boolean functions on some non-empty domain and that the square brackets then correspond to universal quantification over that domain. Since in this model [A] does not depend on the anonymous domain variable, a further universal quantification over that domain has no effect, i.e. viewed as unary operator, the square brackets denote a unary operator that is idempotent: we need not distinguish between [A] and [[A]] and any expression of the form [A] is an identity element of the

square brackets. Identity elements of the square brackets are called "domain constants"; barring dependence on other parameters, true and false are the only domain constants.

Furthermore, in this model the operators introduced so far - i.e. $\equiv ,≠ ,⇒ ,∧ ,\lor ,$ and $¬ -$ do not introduce dependence on the anonymous domain variable, i.e. if their operands are do- main constants, so is the result . Consequently, we do not need to express the idempotence of the square brackets by

[ [ [ X ] ] = [ X ] ]

just $\left\lbrack {\left\lbrack X\right\rbrack }\right\rbrack \equiv \left\lbrack X\right\rbrack$ will do.

Formulae (2.11.b) and (2.11.c) of the

Appendix express

b) that universal quantification of a conjunction is the conjunction of the universal quantifications - a generalization of the associativity and symmetry, of the conjunction -

c) that the disjunctio distributes over universal quantificaton - a generalization of the disjunction's distribution over conjunction.

Remark Formula (2.0.b) may be rewritten as

[ t r u e ] \equiv t r u e , \qquad a n d

formula (2.0.c) as

[ \mathrm {f a l s e} ] \equiv \mathrm {f a i s e}

thus expressing that true and false are identity elements of the square brackets. Since universal quantification over an empty domain always yields true and existential quantification over an empty domain always yields false, emptiness of the domain is excluded. They would also hold for existential quantification over a non-empty domain, but this interpretation is ruled out by (2.11.b). (End of Remark.)

We now turn to formulae (2.14) through (2.25) of the appendix, and since they use a number of new notations, we shall explain those first. (And we guarantee the reader that, after these explanations, the formulae are much less formidable and overpowering than they may look at first sight.)

We start with our notation for functions. Because, in the sequel, we wish to do a lot by the manipulation of uninterpreted formulae, we have to be very precise about the notational conventions we have chosen to adopt. (And to choose we had! There seems to be hardly another area of mathematical notation where the established conventions are so unclear, confusing, ambiguous, and conflicting. We write "sin $\left( {x + \pi }\right)$ ",but are the parentheses in "sin(x)" necessary? Does "sin2x" stand for " (sin x) ${}^{2}$ " or for "sin (sin x) ? If you choose the

First one, please remember that "sin-1x" is usually taken to stand for "arcsin x". Is $f$ in $\mathbf{\Phi}^{*}\mathbf{f}(\mathbf{x},\mathbf{y})^{\prime \prime}$ a function with two arguments, or a function with one argument, this time applied to an argument that happens to be the pair $(x,y)$ ? This last question is less far-fetched as it may seem at first sight because, as we shall see later, a pair of predicates can be viewed as a single predicate.)

We have chosen to treat functional application as an asymmetric binary operator, the left-hand operand being the function and the right-hand operand being the argument, and furthermore to denote this operator by an infix period. So we would write "sin.x" and not merely "sin x". Functional application is given the highest binding power, so in "sin.(x+1)" the parentheses are not optional.

Furthermore, functional application is what is called "left-associative", i.e. $f.x.y$ is short for $(f.x).y$ , where $f.x$ stands for a function that can accept another argument -viz. $y$ -, that is, $f$ itself is a function, application of which (to an argument) yields another function.

Remark Viewing function application to a number of arguments as a number of applications to one argu

ments, one at a time, is a well-known device, called "Currying" (after H.B. Curry). Function application is often denoted by juxtaposition, i.e. by a space. The decision to fill that space by a period, however, is ours. The decision was primarily inspired by the desire to distinguish those "application spaces" from other spaces one might introduce in formulae (as a visual aid to parsing); we chose the period because -again as visual aid to parsing- it is wise to represent the operator with the greater binding power by the smaller character. (End of Remark.)

Next we turn to our syntax for quantifier expressions:

(A dummy: range : term)

universal quantification

(EDdUmmy:range:term)

existential quantification

where "dummy" could also be "dummies" - see, for instance, (2.15.b/c) -

Because this notation deviates in three ways from what is usual, we give the reason for these deviations.

Firstly, instead of A and E one often sees V and E . But writing letters upside down is not a wise way of introducing new characters: for a number of letters -for instance O,I,N,S,X,and

Z - it is too hard to observe the rotation, and the convention greatly complicates the production of typewritten documents.

Secondly, the introduction of the range is unusual. We immediately admit that in the context of universal and existential quantification, the freedom of expression the range gives us is not strictly necessary. As we see from (2.17)

\begin{array}{l} [ (A x: c. x: f. x) \equiv (\underline {{A}} x: t r u e: ¬ c. x \vee f. x) \ I (E x: c. x: f. x) \equiv (\underline {{A}} x: t r u e: c. x \wedge f. x). \ \end{array}

i.e. the range can be subsumed in the term; and as soon as the range is always the constant true, it can be abolished, and such is the convention adopted in the standard literature on logic. The possibility to subsume the range in the term is, however, peculiar to A and E, for which the term is a predicate. The terms could be numbers and the quantification could be the analogue of multiplication or taking the maximum, or the terms could be sets with intersection as the analogue. For the latter situations there are all sorts of conventions; it seemed wiser to choose a uniform syntax and to extend it to universal and existential quantification as well.

The new freedom took us some time getting used to, but, as time went by, we began to

appreciate it more and more. It turned out to be convenient from a calculational point of view. We encountered, for instance, calculations in which all ranges were the same, and we took then the liberty of omitting them -but maintaining the two colons, as we have done, for instance, in (2.22), so as to indicate the omission-. Thus we shortened our calculations without loss of clarity. Admittedly, the concept of range increased the number of formulae we should have at our fingertips; at the same time it increased the amount of useful knowledge at our immediate disposal. The more profound gain, however, will transpire in already the next chapter, where a fundamental characterization of universal and existential quantifications is made in terms of characteristics of their ranges. Without the notion of range, the subsequent theory would have been hard to formulate; it is doubtful whether we could have developed the theory at all.

Our third deviation consists in the obligatory parenthesis pair: $(\underline{\mathbf{A}}\mathbf{x}::\mathbf{f}\cdot \mathbf{x})$ instead of $\forall x.\beta (x)$ We are not going to explain what dummies "really are", but one thing is certain: the notion of a dummy only makes sense with respect to part of the formula, and this part of the formula (which is called the "scope" of the dummy) had better be explicitly delineated. The disadvantage

T - delineates

of the convention of prefixing expressions -with $\forall x$ or $\exists x$ in the case of quantification, with $λ x$ . in the case of lambda abstraction or with $\mu x$ . for the minimal fixpoint- is that it fails to indicate explicitly where the scope of the dummy ends, with the consequence that am- biguous formulae are almost unavoidable. Hence our convention that the obligatory pair of parentheses!the scope of the dummies declared at the beginning, i.e. between the quantifier and the first colon following it. The fact that identity and scope of dummies are syntactically determined is an invaluable convenience.

Remark. Most mathematical notations en vogue now are older than the block concept of ALCOL 60. A major part of the traditional difficulties in explaining the dummy variable to the novice is a direct consequence of now identified short-comings of traditional notations. (End of Remark.)

The simplest approach to dummy variables is to regard a dummy by definition as a fresh variable, never used before and never used again, only used his et nunc. The fact that we write the same x and y over and over again is no more than laziness and lack of phantasy on our part. It does not matter, provided we re

member that under all circumstances

(32) $\left\lbrack {\left( {{\underline{A}}{x} : {b}{.}x : {f}{.}x}\right) \equiv \left( {{\underline{A}}{y} : {b}{.}y : {f}{.}y}\right) }\right\rbrack$

and that there is no point in stating the (usual) proviso "provided neither $x$ nor $y$ occurs (free) in b or p". Function $f$ ,being defined outside the scope of the dummy in question, cannot depend on it in any way: where $f$ is defined, the dummy in question simply "does not exist".

Formula (32) is so fundamental that we did not include it in the appendix. As an aid, we shall stick to the discipline of denoting the dependence of range and term on the dummy so explicitly that renaming the dummy is, as in (32), purely a matter of textual substitution.

We draw attention to the fact that (A x: b. x: f. x) does not depend on $x$ . (How could it? We could have written (A y: b. y: f. y) as well.) It is a consequence of the fact that the dummy "does not exist" outside its scope. This independence is the same phenomenon as the fact that, for any A, [A] is a domain constant. Another way of stating this is that a quantifier expression does not depend on the variable quantified over.

In general, (A dummy: range: term) depends on everything the range or the term depends on; in particular, it is a domain constant if both

range and term are domain constants. In this connection we have to know that boolean expressions as we now them -say: $0 ≤ i < n -$ are domain constants. As a result, (Ai: 0 isn: f.i) is a domain constant if the value of $f$ ,applied to an integer, is; it is a predicate if $f$ is a mapping from integers to predicates ; in general it is a function of $n$

In most cases in the rest of this monograph the range is a domain constant and the term is not. In a few cases a formula only holds provided the range is a domain constant. They are essentially (2.15.a) and its derivatives (2.16.c/d) and the one-point rules (2.24). That is why we have written [b.x] for the range in (2.15.a), which may also be applied with a range such as 0.5i_n (which does not need a pair of square brackets to be transformed into a domain constant).

In reading formulae (2.14) through (2.25) it helps to remember that universal and existential quantifications can be viewed as generalized conjunctions and disjunctions respectively. In particular, we can view a range that is a domain constant as an equation in the dummy; if that equation has a finite number of roots, the universally quantified expression can

be viewed as the conjunction of as many terms as the equation has roots, and similarly for the existential quantification and the disjunction.

The above puts formulae (2.14) into perspec- tive as soon as we realize that false is the canonical form for the equation without roots: the proper value to be attached to a con- or disjunction of zero terms is the corresponding identity element. (At first confrontation with these formulae, (2.14.b) is usually accepted without hesitation, whereas (2.14.a) evokes raised eyebrows; it is the same phenomenon as that people usually accept immediately that the empty sum should be defined to be equal to 0 but have more dif- ficulty with accepting 1 as the proper value for the empty product.)

Formulae (2.15) are the analogue of the symmetry and associativity of con- and disjunction : quantifi-cations of the same kind may be interchanged. Note the special interchange of universal quanthisca-tion and the square brackets (2.15.a): it is only applicable provided the range is a domain con-stant.

Formulae (2.16) express primarily the analogue of the mutual distribution over each other of con- and disjunction; (2.16.c/d) are derivatives, included because of Frequent appeal to them.

Formulae (2.17) express how, with a predicate as term, the range can be subsumed in the term.

Formulae (2.18) express a different consequence from the fact that the quantifications can be viewed as "junctions". So do formulae (2.19); formulae (2.19.c/d) have been added since they give a common case.

Note that in formulae (2.20), variable $y$ occurs only once, and that outside the quantifica tion. It is tacitly assumed that $x$ and $y$ are of the same type, i.e. range over the same domain.

Formulae (2.21) express various forms of what is called "monotonicity", a concept we shall discuss in more detail in the next chapter.

Formulae (2.22) express the analogue of de Morgan's Laws; formulae (2.23) are truly "miscellaneous".

The "one-point rules" (2.24) express that a con- or disjunction of a single term can be viewed as that term itself.

Formulae (2.25) for transforming the dummy are usually applied with a function $g$ that has

an inverse $g^1$ . In that case there are no special constraints on the term, as a function of x can then be rewritten as a function of g.x (viz. the functional composition of the original function and $g^{+}$ ). The fact that g need not be invertible is a reflection of the idempotence of the "junctions".

Formulae (2.26) represent a variation of Leibniz's Rule - about which more below - in combination with monotonicity of quantification.

Though the implication induces an only partial order on predicates, it asks for adjectives referring to that order so that we can use their comparatives and superlatives; the adjectives "strong" and "weak" belong in this connection to the established tradition:

$\left\lbrack {X ⇒ Y}\right\rbrack ∧ !\left\lbrack {X \equiv Y}\right\rbrack$ is read as " $X$ is stronger than $Y$ " or as " $Y$ is weaker than $X$ " and

$\left\lbrack {X ⇒ Y}\right\rbrack$ is read as " $X$ is at weakest $Y$ ", " $X$ is at least as strong as $Y$ ", " $Y$ is at strongest $X''$ or " $Y$ is at least as weak as $X''$ (or sometimes, out of old habit, as " $X$ implies $Y$ ".

The terminology allows us to talk about the strongest or the weakest solution of equations with a predicate as unknown.

We are now going to change gears slightly (or drastically, depending on your taste.)

To begin with we observe that all established formulae are domain constants. Furthermore, since true is the identity element of the equivalence, for each established formula [A] we can establish

[ A ] \equiv t r u e

as well - and the other way round - ; in other words, we may identify "being established" with "being (equivalent to) true".

Next we identify our freedom to establish - on account of the Rule of Leibniz - for some $p$ , $A$ ,and $B$ formula $\left\lbrack {p,B}\right\rbrack$ if $\left\lbrack {A \equiv B}\right\rbrack$ and [P.A] are established with the establishedness of

(A $\equiv$ B] A [P.A] [P.B]

and our freedom of establishing $\left\lbrack {P,A}\right\rbrack \equiv \left\lbrack {P,B}\right\rbrack$ -which is our expression of " [P.A] and [P.B] being equally established" - with the established.

$\left\lbrack {A \equiv B}\right\rbrack ⇒ \left\lbrack {\left\lbrack {P.A}\right\rbrack \equiv \left\lbrack {P.B}\right\rbrack }\right)$

The general formulae

$\left\lbrack {X \equiv Y}\right\rbrack ∧ \left\lbrack {f \cdot X}\right\rbrack ⇒ \left\lbrack {f \cdot Y}\right\rbrack$ and

$\left\lbrack {X \equiv Y}\right\rbrack ⇒ \left( {\left\lbrack {f.X}\right\rbrack \equiv \left\lbrack {f.Y}\right\rbrack }\right)$

cannot be established without postulating for instance - see (2.26.a)

(37) $\left\lbrack {X \equiv Y}\right\rbrack ⇒ \left\lbrack {f \cdot X \equiv f \cdot Y}\right\rbrack$

(The substitution $ \phi \cdot 2\because \left\lbrack {\phi \cdot 2}\right\rbrack $ in (37)) yields

[ X \equiv Y ] ⇒ [ [ f. x ] \equiv [ f. y ] ]

but since the equivalence of two domain constants is again a domain constant, the outer square brackets may be removed, yielding (36). The derivation of (35) from (36) will be postponed until we have described the format of such derivations.)

Finally, we would like to identify as well our appeals to the Rule of Instantiation to an established formula. The Rule of Instantiation tells us that if [r.x.z] is an established formula, so is [r.x.A] for any predicate expression A. (Here Z stands for the variable substituted for, X stands for all the others.)

The established formula we are looking for is (2.20.a)

[ (\underline {{A}} x: f. x) ⇒ f. y) ]

which with the substitution $x,y,f,z \mathrel{\text{:=}} Z,A,\left\lbrack {f \cdot X \cdot z}\right\rbrack$ yields - after omission of the superfluous outer square brackets -

(38) $\left( {\underline{A}Z : \left\lbrack {P.X.Z}\right\rbrack }\right) ⇒ \left\lbrack {P.X.A}\right\rbrack$

Formula (38) is of a structure different from (33) and (34), in which the antecedent - i.e. the part to the left of $⇒$ - is the conjunction of established formulae. For formula (38) the analogy is saved by the following trick: the fact that in an established formula $[\beta .X.Z]$ any expression may be substituted for $Z$ is equated to implicit universal quantification over $Z$ - and over $X$ as well in case we would like to substitute something for $X$

It is in this sense that establishing a new result is equated with establishing an implication with the antecedent a conjunction of established formulae and the consequent - the part to the right of $⇒$ - the new result.

*

In any case, establishing a new result boils down to establishing that the new result is equiv- valent to the domain constant true . A beloved way of doing so is to establish by a chain of transformations that the new result is equivalent to an already established one.

We shall now describe the format of the calculation that establishes $[A] \equiv [D]$ by establishing in succession $[A] \equiv [B], [B] \equiv [C]$ and $[C] \equiv [D]$ . We do not want to write down these three "intermediate" equivalences, as it would force us to write down the "intermediate" formulae

[B] and [C] twice, and those stepping stones of the calculation might be lengthy. Hence we propose the format

[A]

\begin{array}{l} = {\mathrm {h i n t} w h y [ A ] \equiv [ B ] } \ = {\mathrm {h i n t} w h y [ B ] \equiv [ C ] } \ = {h i n t w h y [ C ] \equiv [ D ] } [ D ] \ \end{array}

(The obvious generalization to shorter or longer chains of transformations is left to the reader.)

We shall illustrate the procedure by showing that, instead of postulating (37), we could have

(3 9) [ [ X \equiv Y ] \wedge f. X \equiv [ X \equiv Y ] \wedge f. Y ]

and we do so by establishing that (37) and (39) are equivalent thanks to previously established formulae. For the sake of clarity and because it is the first time we display here such an argument we shall do it in small steps.

\begin{array}{l} [ [ X \equiv Y ] \wedge f. X \equiv [ X \equiv Y ] \wedge f. Y ] \ = {\mathrm {N e g a t i o n} (2. 8. c) } \ [ ¬ ([ X \equiv Y) ∧ f. X) \equiv ¬ ([ X \equiv Y ] ∧ f. Y) ] \ = {d e M o r g a n (2. 9. b), t w i c e } \ [ ¬ [ X \equiv Y ] \vee ¬ f. X \equiv ¬ [ X \equiv Y ] \vee ¬ f. Y ] \ = {\text {D o m a i n c o n s t a n t} (2. 1 1. c) } \ \end{array}

distribution is missing

\begin{array}{l} ¬ [ X \equiv Y ] \lor [ ¬ f. X \equiv ¬ f. Y ] \ = {N e g a t i o n (2. 8, c) } \ ¬ [ X \equiv Y ] \lor [ P. X \equiv P. Y ] \ = {I m p l i c a t i o n (2. 1 0. a) } \ [ X \equiv Y ] ⇒ [ f. X = f. Y ] \qquad q. e. d. \ \end{array}

Note With growing familiarity with the calculus, the chains become shorter: the first two steps could be combined into a single one, and so could the last two steps. (End of Note.)

In a similar vein we could establish $[A] ⇒ [D]$ by establishing, for instance, in succession $[A] ⇒ [B]$ , $[B] \equiv [C]$ , and $[C] ⇒ [D]$ . Such an argument would be rendered in the format

\begin{array}{l} [ A ] \ ⇒ {\mathrm {h i n t w h y} [ A ] ⇒ [ B ] } \ = {\mathrm {h i n t w h y} [ B ] \equiv [ C ] } [ C ] \ ⇒ {\mathrm {h i n t} [ D ] ⇒ [ C ] ⇒ [ D ] } \ \end{array}

and by way of illustration we shall demonstrate, as promised, that (36) implies (35), i.e. with

(4 0) (A ⇒ (B \equiv C)) ⇒ (A ∧ B ⇒ C)

and we could proceed as follows

\begin{array}{l} A ⇒ (B \equiv C) \ = {I m p l i c a t i o n (2. 1 0. a) } \ \lnot A \lor (B \equiv C) \ = {\mathrm {E q u i v a l e n c e} (2. 1 3, a) } \ \lnot A \lor ((\lnot B \lor C) ∧ (B \lor \lnot C)) \ = {D i s t r i b u t i o n (2. 7 c) } \ (¬ A \vee ¬ B \vee C) \wedge (¬ A \vee B \vee ¬ C) \ ⇒ {\mathrm {A b s o r p t i o n} (2. 5, c) } \ \therefore A \vee ¬ B \vee C \ = {d e M o r g a n (2. 9, b) } \ \lnot (A ∧ B) \lor C \ = {I m p l i c a t i o n (2. 1 0. a) } \ A ∧ B ⇒ C \ \end{array}

9.e.d.

The implication just derived, as well as the equivalence derived before, are implied by the formulae referred to in the hints. This gives us another format for proving (40): we compute that the consequent equivales true by using the truth of the antecedent in one of the transformations.

To illustrate this with the same example, we proceed as follows. To start with, we transform the antecedent

\begin{array}{l} A ⇒ (B \equiv C) \ = {\text {I m p l i c a t i o n} (2. 1 0, a) } \ \therefore A \vee (B \equiv C) \ = {\mathrm {D i s t r i b u t i o n} (2. 7. a) \ \end{array}

(4 1) ¬ A \vee B \equiv ¬ A \vee C

and then we proceed

\begin{array}{l} A ∧ B ⇒ C \ = {\text {I m p l i c a t i o n} (2. 1 0, a) } \ i (A \wedge B) \vee C \ = {d e M o r g a n (2. 9. b) } \ (G A \vee \tilde {C}) \vee ¬ B \ = {\mathrm {o n a c c o u n t} o f (4 1) \mathrm {a n d L e i b r i z , s e e N o t e b e l o w} } \ (A \vee B) \vee ¬ B \ = {\mathrm {T e r t i u m n o n d a t u r} (2. 4. a) } \ i A \vee t r u e \ = {\mathrm {Z e r o e l e m e n t s} (2. 2 a) } \ t r u e \ \end{array}

9.e.d.

Note Since A,B,and C stand for domain constants we may surround (41) by a pair of square brackets, thus justifying an appeal to the Rule of Leibniz. (End of Note.)

Of the two ways of proving an implication that have been illustrated above, we shall in future take the liberty of choosing the one that seems most convenient. The decision to allow ourselves that liberty was what we referred to when we wrote that we were "going to change gears slightly (or drastically, depending on your taste)".

Sometimes we prove equivalence by showing the mutual implications separately, e.g. when demonstrating (2.13.c). We give the proof as example of working with quantified formulae.

true

\begin{array}{l} = {\mathrm {L e i b n i z} (2. 2 6. a) } \ [ X \equiv Y ] ⇒ ([ Z ⇒ X ] \equiv [ Z ⇒ Y ]) \ ⇒ {(2. 1 4, c) } \ (A Z: [ X \equiv Y ] ⇒ ([ Z ⇒ X ] \equiv [ Z ⇒ Y ]) \ = {\mathrm {D i s t r i b u t i o n} (2. 1 6, c) } \ [ X ⇒ Y ] ⇒ (¬ Z:: [ Z ⇒ X ] \equiv [ Z ⇒ Y ]) \ \end{array}

\begin{array}{l} (¬ A Z:: [ Z ⇒ X ] \equiv [ Z ⇒ Y ]) \ ⇒ {\mathrm {I n s t a n t i a t i o n} (2. 2 0. a) } \mathrm {t w i c e :} Z := X \mathrm {a n d} Z := Y } \ ([ X ⇒ X ] \equiv [ X ⇒ Y ]) \wedge ([ Y ⇒ X ] \equiv [ Y ⇒ Y ]) \ = {\mathrm {T e r t i u m n o n d a t u r} (2. 4. c) } \ [ X ⇒ Y ] ∧ [ Y ⇒ X ] \ = {(2. 1 2. b), (2. 1 1. b), a n d (2. 1 3. a) } \ [ X \equiv Y ] \ \end{array}

q.e.d.

We shall use the same proof format for establishing $[A \equiv D]$ by, say, the chain $[A \equiv B], [B \equiv C]$ , and $[C \equiv D]$ , i.e.:

A

\begin{array}{l} = {h i n t w h y [ A = B ] } \ = {h i n t w h y [ B \equiv C ] } \ = {h i n t w h y [ C \equiv D ] } \ \end{array}

Similarly we might demonstrate $\left\lbrack {A ⇒ D}\right\rbrack$ by

\begin{array}{r l} & {A} \ & {= {\mathrm {h i n t} w h y [ A \equiv B ] }} \ & {B} \ & {⇒ {\mathrm {h i n t} w h y [ B ⇒ C ] }} \ & {C} \ & {= {\mathrm {h i n t} w h y [ C \equiv D ] }} \ & {D} \end{array}

That is, in our proof lines we need not restrict ourselves to domain constants, we can admit general predicate expressions as well provided that we remember that the chain of reasoning still consists of a chain of domain constants, as the relation between any pair of successive lines has to be surrounded by a pair of square brackets. (Since $[A] = [B]$ and $[A] = [B]$ are the same, our initial use of the proof format is a special case of our final use as we just described.)

Warning Our final proof format leaves pairs of square brackets unmentioned:

A = {\mathrm {h i n t} } B = {\mathrm {h i n t} } C = {\mathrm {h i n t} } D

is not short for

[ A = B \equiv C \equiv D ]

but short for the much stronger

[ A \equiv B ] \wedge [ B \equiv C ] \wedge [ C \equiv D ]

Implicit square brackets are such a rich source of potential confusion that for more than two years we have confined ourselves in our work to proofs in which the lines were domain constants. We could do that by using a new predicate variable, $Z$ say, and write:

"We observe for any $z$

\begin{array}{l} [ Z \equiv A ] \ = {\mathrm {h i n t} w h y [ A \equiv B ] } \ [ Z \equiv B ] \ = {\mathrm {h i n t} w h y [ B \equiv C ] } \ [ z \equiv c ] \ = {\mathrm {h i n d} w h y [ C \equiv D ] } \ [ Z \equiv D ] \ \end{array}

Since A, B, C, and D are in general sizeable expressions, the introduction of the $[Z \equiv \dots]$ is only a small notational overhead. But eventually we have allowed ourselves to be convinced that it could also be viewed as a notational mannerism: the $[Z \equiv \dots]$ occurred so frequently that it seemed justified to subsume its role in the rules as how to read our proofs. From now onwards the reader has to remember the unwritten square brackets that are implied by the proof format. (End of Warning.)

Constants

(2.0) a) [false ≡ ¬true] b) [true] c) $\left\lbrack {\text{false}}\right\rbrack$

Identity elements

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

e) $\left\lbrack {X \equiv X}\right\rbrack$

b) $\left\lbrack {X \equiv X ≠ {\rho a1s e}}\right\rbrack$ c) $\left\lbrack {X \equiv X \vee {\text{false}}}\right\rbrack$ d) $\left\lbrack {X \equiv X ∧ \text{true}}\right\rbrack$

Zero elements

(2.2) a) $\left\lbrack {X \vee \text{true} \equiv \text{true}}\right\rbrack$ b) $\left\lbrack {X ∧ \text{false} \equiv \text{false}}\right\rbrack$

Idempotence

(2.3) a) $[X, X \equiv X]$ b) $\left\lbrack {X ∧ X = X}\right\rbrack$

Tertium non dahur

(2.4) a) $\left\lbrack {X \vee ¬ X \equiv ¬ \text{true}}\right\rbrack$

c) $\left\lbrack {X ⇒ X}\right\rbrack$

b) $\left\lbrack {X ∧ ¬ X \equiv \text{ false }}\right\rbrack$

Absorption

(2.5) a) $[X \vee (X \wedge Y) \equiv X]$

c) $\left\lbrack {X ∧ Y ⇒ X}\right\rbrack$

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

d) $\left\lbrack {X ⇒ X \vee Y}\right\rbrack$

Complement

(2.6) a) $\left\lbrack {X \vee \left( {¬ X ∧ Y}\right) \equiv X \vee Y}\right\rbrack$

b) $\left\lbrack {X ∧ \left( {¬ X \vee Y}\right) \equiv X ∧ Y}\right\rbrack$

Distribution

(2.7) a) $\left\lbrack {\left( {X \equiv Y}\right) \vee Z \equiv X \vee Z \equiv Y \vee Z}\right\rbrack$ b) $\left\lbrack {\left( {X ≠ Y}\right) ∧ Z \equiv X ∧ Z ≠ Y ∧ Z}\right\rbrack$ c) $\left\lbrack {\left( {X ∧ Y}\right) \vee Z} \equiv \left( {X \lor Z}\right) ∧ \left( {Y \lor Z}\right) }\right\rbrack$ d) $\left\lbrack {\left( {X \vee Y}\right) ∧ Z \equiv \left( {X ∧ Z}\right) \vee \left( {Y ∧ Z}\right) }\right\rbrack$

Negation

(2.8) a) [77X ≡ X]

b) $\left\lbrack {¬ \left( {X \equiv Y}\right) \equiv X ≠ Y}\right\rbrack$ c) $\left\lbrack {X \equiv Y \equiv ¬ X = ¬ Y}\right\rbrack$

de Morgan

(2.9) a) [7(XvY) = 7x vY] b) $\left\lbrack {7\left( {X ∧ Y}\right) \equiv 7X \vee 7Y}\right\rbrack$

Implication

(2.10) a) $\left\lbrack {X ⇒ Y \equiv {¬ X} \vee Y}\right\rbrack$

b) $\left\lbrack {X ⇒ Y \equiv X ∧ Y \equiv X}\right\rbrack$ c) $\left\lbrack {X ⇒ Y \equiv {X}_{\vee }Y \equiv Y}\right\rbrack$ d) $\left\lbrack {X ⇒ Y \equiv \left( {X \equiv Y}\right) \vee Y}\right\rbrack$ (e) $\left\lbrack {X ⇒ Y ≠ \left( {X ≠ Y}\right) ∧ X}\right\rbrack$

$\left{ {\begin{array}{l} X ∧ Y \equiv X \equiv Y \equiv {XVY}\rbrack \end{array} ⇒ {XV} ⇒ {YV}}\right.$

Domain constants

(2.11) a） $[ [ X ] ] = [ X ]$

b) $\left\lbrack {X ∧ Y}\right\rbrack \equiv \left\lbrack X\right\rbrack ∧ \left\lbrack Y\right\rbrack$ c) $[X \vee [Y]] \equiv [X] \vee [Y]$ d) $[X \equiv Y] ⇒ ([X] \equiv [Y])$ (e) $[X ⇒ Y] ⇒ ([X] ⇒ [Y])$

Expressions for $\left\lbrack {X ⇒ Y}\right\rbrack$

(a) $\left\lbrack {X ⇒ Y}\right\rbrack \equiv \left\lbrack {X ∧ ¬ Y \equiv {¬ a} \mid s}\right\rbrack$

\begin{array}{l} b) [ X ⇒ Y ] \equiv [ ¬ X \lor Y \equiv \mathrm {t r u e} ] \ c) [ X ⇒ Y ] \equiv [ X ∧ Y \equiv X ] \ d) [ X ⇒ Y ] = [ X \vee Y \equiv Y ] \ e) [ X ⇒ Y ] \equiv (\exists Z: [ X \equiv Y ∧ Z ]) \ f) [ X ⇒ Y ] \equiv (\exists z: [ X \vee Z \equiv Y ]) \ g) [ X ⇒ Y ] \equiv [ (\underline {{A}} Z: [ Z ⇒ X ]; Z ⇒ Y) ] \ \end{array}

E x p r e s s i o n s f o r [ X \equiv Y ]

(2.13) a) $[X \equiv Y \equiv (¬ X \vee Y) \wedge (X \vee ¬ Y)]$

\begin{array}{l} b) [ X \equiv Y \equiv (X \wedge Y) \vee (¬ X \wedge ¬ Y) ] \ c) [ X \equiv Y ] \equiv (¬ Z:: [ Z ⇒ X ] \equiv [ Z ⇒ Y ]) \ d) [ X \equiv Y ] \equiv (\underline {{A}} Z: [ X ⇒ Z ] \equiv [ Y ⇒ Z ]) \ e) [ X \equiv Y \equiv X \vee Y \equiv X \wedge Y ] \ \end{array}

Quantification over empty range or of constant term

(2.14) a) [ (A x: false: f.x) ≡ true ] c) [ (A x: b.x: true) ≡ true ] b) $\left\lbrack {\left( {\underline{E}x : \text{false: }f.x}\right) \equiv f\text{false}}\right\rbrack \mathrm{d})\left\lbrack {\left( {\underline{E}x : b.x : \text{false}}\right) \equiv \text{false}}\right\rbrack$

Interchange of quantifications

(a) $\left\lbrack {\left( {\underline{a} \times : \lbrack b.x\rbrack : f \cdot x}\right) }\right\rbrack \equiv \left( {\underline{a} \times : \lbrack b.x\rbrack : \lbrack f \cdot x\rbrack }\right)$

b) [ (A, y: b.x ∧ c.x.y: f.x.y) ]

(\underline {{A}} x: b. x: (\underline {{A}} y: c. x. y: f. x. y)) ]

c) $I\left( {\underline{E}{x,y};b.x ∧ c.x.y;\overline{p}.\left( {x,y}\right) }\right) \equiv$

(E x: b. x: (E y: c. x. y: f. x. y)) ]

d) $\left\lbrack {\left( {\underline{A} \times : {bx} : \left( {\underline{A}y : c.y : f.x.y}\right) }\right) \equiv }\right.$

(\exists y: c. y: (\exists x: b. x: f. x. y)) ]

(e) $\left\lbrack {\left( {{E}{X} : {b}{X} : \left( {{E}{Y} : c{Y} : f_{X,Y}}\right) }\right) \equiv }\right\rbrack$

(\exists y: c. y: (\exists x: b. x: f. x. y)) ]

Distribution of $v, ∧$ and $⇒$

(2.16) a) $\left\lbrack {\left( {\underline{A} \times : b \cdot x : f \cdot x}\right) \vee X}\right) \equiv \left( {\underline{A} \times : b \cdot x : f \cdot x}\right) \vee X\rbrack$

b) $\left\lbrack {\left( {{E}{X} : {b}{X} : {f}{X} ∧ X}\right) \equiv \left( {{E}{X} : {b}{X} : {f}{X}}\right) ∧ X}\right\rbrack$ c) $\left( {\underline{A}x : \left\lbrack {b.x}\right\rbrack : \left\lbrack {X ⇒ {f}_{.}x}\right\rbrack }\right) \equiv \left\lbrack {X ⇒ \left( {\underline{A}x : \left\lbrack {b.x}\right\rbrack : \underline{f}.x}\right) }\right\rbrack$ d) $\left( {\underline{\mathrm{A}}\mathrm{x} : \left\lbrack {\mathrm{b}.\mathrm{x}}\right\rbrack : \left\lbrack {\mathrm{f}.\mathrm{x} ⇒ \mathrm{x}}\right\rbrack }\right) \equiv \left\lbrack {\left( {\underline{\mathrm{E}}\mathrm{x} : \left\lbrack {\mathrm{b}.\mathrm{x}}\right\rbrack : \mathrm{f}.\mathrm{x}}\right) ⇒ \mathrm{X}}\right\rbrack$

Trading

(2.17) a) $\left\lbrack {\left( {\underline{A}x : b.x ∧ c.x : f.x}\right) \equiv \left( {\underline{A}x : b.x : c.x \lor f.x}\right) }\right\rbrack$ b) $\left\lbrack {\left( {{\underline{\mathrm{E}}}{X} : {b}{.}X ∧ c.{.}^{ ∧ }{c}{.}X}\right) \equiv \left( {{\underline{\mathrm{E}}}{X} : {b}{.}X : {c}{.}X ∧ {f}_{.}X}\right) }\right\rbrack$

Distribution of $\underline{A}$ and $E$

(2.18) a) [ (a x : : f.x A g.x ) ≡

(\underline {{A}} x: f. x) \wedge (\underline {{A}} x: f. y) ]

b) $\left\lbrack {\left( {\underline{E} \times \because f. \times v}\right) \vee g. \times }\right\rbrack =$

(E x: f. x) \vee (E x: g. x) ]

Range a disjunction

(2.19) a) $\left\lbrack {\left( {{\underset{\sim }{A}}{X} : {b}{X} \vee c.X : f.X}\right) \equiv }\right.$

(\underline {{A}} x: b. x: f. x) \wedge (\underline {{A}} x: c. x: f. x) ]

b) $\left\lbrack {\left( {\underline{E}x : b.x \vee c.x : f.x}\right) \equiv }\right.$

(E x: b. x: f. x) \vee (E x: c. x: f. x) ]

c) $\left\lbrack {\left( {{A}{i} : 0 ≤ i < n + 1 : {P}{i}}\right) \equiv \left( {{A}{i} : 0 ≤ i < n : {P}{i}}\right) ∧ {P}_{i}n}\right\rbrack$

$d)\left\lbrack {\left( {{E}{i} : 0 ≤ i < n + 1 : {f}{i}}\right) \equiv \left( {{E}{i},0 ≤ i < n : {f}{i}}\right) \vee {f}_{i}n}\right\rbrack$

Instantiation

(2.20) a) $\left\lbrack {\left( {\underline{A}x}\right) : f.x}\right) ⇒ f.y\rbrack$

b) $\left\lbrack {f,y ⇒ \left( {\underline{E}x : f.x}\right) }\right\rbrack$

Monotonicity

(2.21) a) $\left( {\underline{A}x : \left\lbrack {b,x}\right\rbrack : \left\lbrack {P.x ⇒ g.x}\right\rbrack }\right) ⇒$

[ (\underline {{A}} x: [ b. x ]: \underline {{P}}. x) ⇒ (\underline {{A}} x: [ b. x ]: g. x) ]

b) $\left( {\underline{A}x : \left\lbrack {b,x}\right\rbrack : \left\lbrack {f.x ⇒ g.x}\right\rbrack }\right) ⇒$

[ (\underline {{E}} x: [ b. x ]: \beta . x) ⇒ (\underline {{E}} x: [ b. x ]: g. x) ]

c) $\left\lbrack {\left( {{A}{X} : \left\lbrack {{P}{X} ⇒ {g}{X}}\right\rbrack : {P}{X}}\right) ⇒ \left( {{A}{X} : \left\lbrack {{P}{X} ⇒ {g}{X}}\right\rbrack : {g}{X}}\right) }\right\rbrack$

$d)\left\lbrack {\left( {{E}{X} : \left\lbrack {{P}{X} ⇒ {g}{X}}\right\rbrack : P}{X}}\right) ⇒ \left( {{E}{X} : \left\lbrack {{P}{X} ⇒ {g}{X}}\right\rbrack : {g}{X}}\right) }\right\rbrack$

de Morgan

(2.22) a) $\left\lbrack {7\left( {\underline{A}x : : P.x}\right) \equiv \left( {\underline{E}x : : - P.x}\right) }\right\rbrack$

$⇒ \left\lbrack {¬ \left( {{\underline{\mathrm{E}}}{x} : : {\underline{P}}{x}}\right) \equiv \left( {{\underline{\mathrm{A}}}{x} : : {\underline{P}}{x}}\right) }\right\rbrack$

Miscellaneous

(2.23) a) $\left\lbrack {\left( {\underline{A} \times :}\right\rbrack \left\lbrack {{\rho }{1}x}\right\rbrack : \left( {{\rho }{1}x}\right) \equiv \text{true}}\right\rbrack$

b) $\left\lbrack {\left( {E \times :}\right) \left\lbrack {f.x}\right\rbrack : v\left( {f.x}\right) \equiv f\text{false}}\right\rbrack$

c) [ $p,q ∧ \left( {\underline{A}i : 0 ≤ i < n : p\left( {t + 1}\right) }\right) \equiv$

(\underline {{A}} i: 0 ≤ i < n + 1: f _ {i}) ]

$d)$ [ $p,q$ v (E i: $0 ≤ i < n : p\left( {i + 1}\right) ) \equiv$

(E: i: 0 ≤ i < n + 1: p, i) ]

e) $V = \phi \vee \left\lbrack {\left( {{\underline{\mathrm{A}}}{X} : X \in V : {\beta }{X} ∧ X}\right) \equiv \left( {{\underline{\mathrm{A}}}{X} : X \in V : {\beta }{X}}\right) ∧ X}\right\rbrack$ $p) V = \varnothing \vee \left\lbrack {\left( {{E}{X} : X \in V : {p}{X} \vee X}\right) \equiv \left( {{E}{X} : X \in V : {p}{X} \vee X}\right) }\right\rbrack$ $g) v = \phi \vee \left\lbrack {\left( {\underline{A}x : x \in V : X}\right) \equiv X}\right\rbrack$ [h) V = \phi \vee \left\lbrack {\left( {{E}_{X} : X \in V : X}\right) \equiv X}\right\rbrack ]

One-point rules

(2.24) a) $\left\lbrack {\left( {\underline{A}x : x = y : f.x}\right) \equiv {f.y}}\right\rbrack$ b) [ (A X : [ X ≡ Y ] : F X) = F . Y ] c) $\left\lbrack {\left( {\underline{\mathrm{E}}x : x = y : f.x}\right) \equiv f.y}\right\rbrack$ d) [(EX: [X ≡ Y] : f. X) ≡ f. Y]

Transforming the dummy

(2.25) a) [ (A X: b.X : f. (g. X)) ]

(\underline {{A}} Y: (\underline {{E}} X: b. x: [ g. x \equiv Y ]): f. Y) ]

b) $\left\lbrack {\left( {\underline{E} \times : b \cdot x : f.}\right) .\left( {g \cdot x}\right) }\right\rbrack \equiv$

(\underline {{E}} Y: (\underline {{E}} X; b. X: [ g. X \equiv Y ]): f. Y) ]

Leibniz

(2.26) a) $\left\lbrack {X \equiv Y}\right\rbrack ⇒ \left\lbrack {P \cdot X \equiv P \cdot Y}\right\rbrack$

(b) $\left\lbrack {\left( {\underline{A} \times : b. \times : \left\lbrack {X. \times = Y. \times }\right\rbrack }\right) ⇒ }\right\rbrack$

(\underline {{A}} x: b. x: [ f. (X. x) \equiv f. (Y. x) ]) ]

(c) $\left\lbrack {\left( {{E}_{X} : b.x : \left\lbrack {X.X \equiv Y.X}\right\rbrack }}\right) ⇒ }\right\rbrack$

(E x: b. x: [ f. (X. x) \equiv f. (Y. x) ]) ]

Some comments on the preceding draft of Chapter 2

This chapter became much longer than foreseen. It will have to be rewritten, but I shall postpone its rewriting until at least a major part of the draft for the whole book has been finished: then we know in how much detail we want to refer to the formulae in the appendix.

I do like the sections on syntax and notation (symmetry, associativity, binding power, range and term) and am pleased with the term "domain constant." I also think I was right in starting with $\equiv$ At EWD905-13 (Reason) I should have stressed that $\left\lbrack {A \equiv B}\right\rbrack$ expresses equality for predicates in the sense that $x = y$ is written $\left\lbrack {x \equiv y}\right\rbrack$ in the special case that $x$ and $y$ are predicates: I was annoyed that .at (2.24) I had to write my one-point rules in duplo.

I abstained from introducing Q for either A or E ; in the final version I shall do so, I think. The one-point rule becomes

[ (\underline {{Q}} x: x = y: f. x) \equiv f. y ]

In retrospect there are enough formulae to jus

I am less pleased by my rather formal introduc- tion of what looks like the propositional calculus - the intermezzo- and, in contrast, just the postula-tion of the formulae with quantification. The intermezzo is fun, but perhaps out of place. I have

my doubts about my use of "to establish" and wonder whether I could have avoided that meta-phor , thereby avoiding the need "to shift gears".

A symptom for my annoyance is "the trick" on EWD905-3g, top paragraph: from

[ f. X. Z ] (\equiv \mathrm {d r u e})

and (A) $Z\because$ true)

we derive

(\mathrm {且} Z:: [ P, X, Z ])

Somewhere I should have stated that the universal quantification was there all the time.

I have been very implicit about "substitution". It does not bother me, but I am sure it bothers others. I could have solved this problem, by introducing $P.\mathrm{Z}$ first (with $P.\mathrm{A}$ ) and then state that the logical connectives form new functions $\mathrm{f}.\mathrm{Z} ∧ \mathrm{f}.\mathrm{Z}$ yielding $P.\mathrm{A} ∧ P.\mathrm{A}$ , etc.

I found it very hard to decide which formulae to include in the appendix. There seems something wrong with including

[ X \equiv Y \equiv (X \wedge Y) \vee (¬ X \wedge ¬ Y) ]

and its "immediate" consequence

[ X \equiv Y ] \approx [ (X \wedge Y) \vee (¬ X \wedge ¬ Y) ].

I now realize that

[ (X \wedge Z) \vee (Y \wedge ¬ Z) \equiv (X \vee ¬ Z) \wedge (Y \vee Z) ]

has disappeared. (Tomy's X if Z elze Y)

In the name of the intermezzo I may have postponed the introduction of the implication for too long. Had I focussed on the calculus as used later I could have concentrated on

(i) how to derive an equivalent expression (ii) how to derive a weaker expression.

Any comments and helpful suggestions are welcome!

Austin, 3 February 1985

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