A regrettable cover

A regrettable cover

On the cover of "A Logical Approach to Discrete Math" by David Gries and Fred B. Schneider we find a theorem and its formal proof. Regrettably, the nice idea of putting a theorem and its proof on the cover has been poorly executed, for the proof is clumsy. I copy from the cover:

Theorem:

$$ (\forall x \mid : P \Rightarrow Q) \equiv {x \mid P } \subseteq {x \mid Q } $$

Proof:

$$ \begin{array}{l} {x \mid P } \subseteq {x \mid Q } \ = \langle D e f. o f S u b s e t \subseteq , w i t h v n o t o c c u r r i n g f r e e i n P o r Q \rangle \ (\forall v | v \in {x | P }: v \in {x | Q }) \ = \langle v \in {x } R \rangle \equiv R [ x := v ], t w i c e \rangle \ (\forall v \mid P [ x := v ]: Q [ x := v ]) \ = \langle T r a d i n g; D u m m y r e n a m i n g \rangle \ (\forall x: P [ x := v ] [ v := x ] \Rightarrow \ Q [ x := v ] [ v := x ]) \ = \langle R [ x := v ] [ v := x ] \equiv R i f v \ d o e s n o t o c c u r f r e e i n R, t w i c e) \ (\forall x: P \Rightarrow Q) \ \end{array} $$

In the book, dummy renaming is covered

(8.21) Axiom, Dummy renaming: Provided

7 occurs $\left( {{}^{\prime }y,{}^{\prime \prime }R,{P}^{\prime }}\right)$

$$ ( \times ] R: P) = ( y ] R [ x := y ]: P [ x := y ]) $$

In the quoted proof, (8.21) is used to introduce the substitution $\left\lbrack {v \mathrel{\text{:=}} x}\right\rbrack$ ,instead of using it to eliminate the substitution $\left\lbrack {x \mathrel{\text{:=}} v}\right\rbrack$ :

the proof could have ended with

$$ \begin{array}{l} (\forall v \mid P [ x := v ]: Q [ x := v ]) \ = \langle T r a d i n g; D u m m y r e n a m i n g \rangle \ (\forall x: P \Rightarrow Q) \ \end{array} $$

The proof on the cover missed that "sub. shiluting equals for equals" can be used in either direction. But the whole "dummy renam-. ing" is avoidable, for dummy v should not have been introduced in the first place: The one and only variable that by definition does not occur free in expressions ${x} P}$ or ${x|Q}$ is x! So, here is a simpler proof:

$$ \begin{array}{l} {x \mid P } \subseteq {x \mid Q } \ = {\mathrm {D e f . o f} \leq } \ \langle \forall x: x \in {x | P }: x \in {x | Q } \rangle \ = {x \in {x | R } \equiv R, t w i c e; t r a d i n g } \ \langle \forall x: P \Rightarrow Q \rangle . \ \end{array} $$

By the standards of the book there is nothing fancy about this proof. I quote from

p. 199:

"Theorem (11.7) formalizes the connection between sets and predicates: a predicate is a representation for the set of argument -values for which it is true,

$$ (1 1. 7) \quad x \in {x | R } = R $$

Note that $x$ is used with two different meanings in the LHS of (11.7). The leftmost occurrence of $x$ is free, as are free occurrences of $x$ in the RHS. All occurrences of $x$ in ${x} R}$ are bound."

With the same four steps, the quoted proof occurs inside the book on p. 207.

Acknowledgement Wim H.J. Fegen en Rutger M. Dijkstra have independently drawn my attention to the cover's clumsiness.

Nuenen, 30 December 1993

plofo. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin TX 78712-1188

USA