Remarks on notation (with A.J.M. van Gasteren)

Remarks on notation

We tried to write a more or less comprehensive essay on notation but failed. We concluded that we were not ready for it and had better first collect more observations, not worrying if they are disconnected.

In the case of explicitly mentioned dummies it should be syntactically explicit that they are dummies. Standard set notation does not satisfy this criterion, cf. the following sequence of "sets": ${x \mid x < y}, {y \mid y > x}, {y \mid x < y}, {x + y \mid x < y}$ .

By the nature of our work we have to deal a lot with named total truth functions defined on the states $σ$ of a state space $Σ$ . A standard mathematical practice is to name the function, $P$ say, and to denote the value of its application by supplying it with an argument, $P(x,y)$ say. The definition of $P$ then requires dummies for the formal parameters, say

def P (\eta , \eta) = (3 \cdot \frac {\eta}{2} ≤ \eta + 1).

If the function is always applied to the same argument, the need for such local terminology in the definition can be circumvented by not naming the function, but by naming the expression, say

def P: 3 \cdot x ≤ y + 1.

What in functional notation would be written as $P\left( {x,y}\right) ⇒ Q\left( {x,y}\right)$ is then rendered by $P ⇒ Q$ . We have used such "express- sional notation" at great advantage. (We know, however, of a

referee of a mathematical journal that objected to it.

A further advantage of the expressiional notation is that no new convention is required for the introduction of expressions such as $¬ P$ or $¬ P ∧ Q$ to denote derived predicates, whereas in functional notation the introduction of derived functions such as $¬ P$ or $¬ P ∧ Q$ would require either a separate convention or an explicit function definition each time.

The advantage of the functional notation is the readiness with which we can express universal quantification, e.g.

(\underset {σ : σ \in Σ : P (σ) ⇒ Q (σ)} {σ : σ \in Σ : P (σ) ⇒ Q (σ)}) o r (\underset {σ : σ \in Σ : P (σ) = Q (σ)} {σ : σ \in Σ : P (σ) = Q (σ)}).

But this is rather lengthy. The first temptation is to omit the range, e.g. $(\underline{\alpha}σ::P(σ) = Q(σ))$ , but this is silly, since $Σ$ carries more relevant information than the dummy $σ$ . The latter's irrelevance is sometimes reflected in its omission with the purpose of expressing universal quantification, e.g. for $(\underline{\alpha}σ::P(σ) = Q(σ))$ either $P = Q$ or, to stress the point, $P \equiv Q$ . Such hidden universal quantification, however, is deadly dangerous, for then $P ≠ Q$ has not the same meaning as $¬ (P = Q)$ .

The expressional notation, however, invites us to omit in the universal quantification not the range but the dummy and to write

(\underline {{\theta}}: Σ : P ⇒ Q) o r (\underline {{\theta}}: Σ : P = Q).

In a treatise involving a single state space , that state spacecan remain anonymous , provided we introduce a special bracket

pair for " $(\underline{\mathbf{A}}:Σ :$ " and the matching ") " respectively. In a recent manuscript the local convention was adopted to use square brackets for this purpose; the resulting formulae were well-geared to systematic manipulation. One quickly learns that $P ⇒ Q$ stands for a predicate defined on state space, whereas $[P ⇒ Q]$ denotes a boolean value, thereby avoiding a common confusion.

A further remark about $\equiv$ , when used as special infix character to denote universal quantification. In an earlier version of aforementioned manuscript only implications were universally quantified. By analogy the new symbol $⇒$ could have been introduced; in fact, the symbol $⇒$ was used with the explicitly stated convention that implications had to be understood to be quantified over all states. This convention was as profound a mistake as the new symbol would have been. Neither of the two techniques admits of extension to all logical connectives: either one has to introduce more new symbols - a notorious blind alley - or more traditional connectives can no longer be used in their (indispensable) standard meaning. (And that extension to universal quantification beyond quantification of implications only was exactly what was needed for the streamlining of the original argument.) Moreover both techniques fail in the absence of a connective.

drs. A.J.M. van Gasteren BP Venture Research Fellow Dept. of Mathematics and Computing Science University of Technology 5600 MB EINDHOVEN The Netherlands

3 March 1982 prof. dr. Edsger W. Dijkstra Burroughs Research Fellow Plataanstraat 5 5671 AL NUENEN The Netherlands