Our book’s omission on quantification over scalar subtypes

Our book's omission on quantification over scalar subtypes

In our book [DS90], we failed to introduce scalars of type T as a subtype of structures of type T, and consequently, our use of the expression "of the same type" is sometimes ambiguous. In the rest of this text, x,y stand for dummies of type structure of typeT, and c for a scalar dummy of type T.

In [AB36], Lex BgIsma righlly points out that our text can be interpreted as suggesting the truth of the generally false

$$ [ \langle \forall c: [ c = x ]: f. c \rangle \equiv f. x ] $$

and that our text fails to deal explicitly with the theorem that for punctual $f^{\alpha}$

(0) $\left\lbrack {\langle \forall c : c = x : f.c}\right\rangle \equiv { .x}$

(a theorem which is used!). The purpose of this note is to remedy this situation.

We shall use for the subtype relation between $x$ and $c$ the postulate

(1) $\left\langle {\forall c : \left\langle {\exists x : \left\lbrack {x = c}\right\rbrack }\right\rangle }\right\rangle$ ,

from which -since $\left\lbrack {\left\lbrack X\right\rbrack \Rightarrow X}\right\rbrack -$

(2) $\left\langle {\forall c : \left\lbrack {\langle \exists x\because x = c}\right\rbrack }\right\rangle$

follows. Furthermore, the fact that $c$ is not just a subtype of the structure $x$ but is the corresponding scalar type leads to the postulate

(3) $\left\langle {\forall x\therefore \left\lbrack {\langle \exists c\therefore c = x}\right\rbrack }\right\rangle$

Finally we recall the definition of $f$ ’s punctuality:

(4) $\left\lbrack {\langle \forall x,y : x = y \Rightarrow f \cdot x = f \cdot y}\right\rbrack$

for boolean $f$ , predicate calculus allows us to rewrite (4) as

$\left\lbrack {\langle \forall x,y : x = y \Rightarrow f \cdot x \equiv x = y \Rightarrow f \cdot y\rangle }\right\rbrack$

Just to be on the -very- safe side, we check that a formula universally quantified over $x$ may be instantiated with $x := c$ , i.e. we shall prove for non necessarily punctual $g$

(6) $\left\lbrack {\langle \forall x : g \cdot x\rangle \Rightarrow \langle \forall c : g \cdot c\rangle }\right\rbrack$

To this end we observe

$$ \begin{array}{r l} & {\langle \forall c:: g. c \rangle} \ {=} & {{(1) }} \ & {\langle \forall c:: \langle \exists x:: [ x = c ] \rangle \Rightarrow g. c \rangle} \ {=} & {{\mathrm {p r e d i c a t e c a l c u l u s} }} \ & {\langle \forall c:: \langle \forall x:: [ x = c ] \Rightarrow g. c \rangle \rangle} \end{array} $$

$$ \begin{array}{l} = {\text {i n t e r c h a n g e}; \text {L e i b n i z} } \ \langle \forall x: \langle \forall c: [ x = c ] \Rightarrow g _ {2} x \rangle \rangle \ = {\text {p r e d i c a t e c a l c u l u s} } \ \langle \forall x: \langle \exists c: [ x = c ] \rangle \Rightarrow q. x \rangle \ \Leftarrow \quad {p r e d i c a t e c a l c u l u s } \ \langle \forall x: g. x \rangle \ \end{array} $$

Note The first step is not such a rabbit

when we realize (i) that we have to use

(i)

have to introduce a quantification over $x$ ,

and (iii) Leibniz is needed to relate $g.c$

to $g.x\;$ (End of Note.)

The proof of (0) is by a ping-pong

the proof of (b) is by a ping-pong argument; pong being the easiest, we do

that we can first.

$$ \mathrm {P r o o f} \varphi (0), [ L H S \Leftarrow R H S ] $$

$$ [ \langle \forall c: c = x: f. c \rangle \Leftarrow f. x ] $$

$$ \Leftrightarrow \quad {(6) } $$

$$ [ \langle \forall y: y = x: f. y \rangle \Leftarrow f. x ] $$

$$ = {\mathrm {p r e d . c a l c .} } $$

$$ [ \langle \forall y: y = x: f \cdot y, \Leftarrow f \cdot x \rangle ] $$

$$ \Leftrightarrow \quad {\mathrm {p r e d . c a l c .} } $$

$$ [ \langle \forall y: y = x \Rightarrow (f. y \equiv f. x) \rangle ] $$

$$ \begin{array}{l} = {4, f i s p u n c t u a l } \ t r u e. \ \end{array} $$

$$ (E n d o f P r o o f o (0), [ L H S \Leftarrow R H S ].) $$

We have not made use yet of (3). We are going to do that by showing, in pre- paration of the proof of pinging, that for punctual

$$ (7) \quad [ \langle \forall x: f. x \rangle \equiv \langle \forall c: f. c \rangle ] $$

The proof is remarkably similar to the earlier proof of (6). We observe for. punctual $f$ :

$$ \begin{array}{l} \langle \forall x: f _ {n} x \rangle \ = {3 } \ \langle \forall x:: \langle \exists c:: c = x \rangle \Rightarrow f. x \rangle \ = {\mathrm {p r e d . c a l c .} } \ \langle \forall x: \langle \forall c: c = x \Rightarrow f. x \rangle \rangle \ = {\text {i n t e r c h a n g e} _ {j} (5) \& (6), P \text {i s p u n c h i a l} } \ \langle \forall c: \langle \forall x: x = c \Rightarrow f. c \rangle \rangle \ = {\text {p r e d . c a l c .} } \ \langle \forall c: \langle \exists x: x = c \rangle \Rightarrow f. c \rangle \ = {2 } \ \langle \forall c: f. c \rangle , \ \end{array} $$

and after this demonstration of (7),

the proof of ping is a walk-over.

$$ \mathrm {P r o o f} (0), [ \mathrm {L H S} \Rightarrow \mathrm {R H S} ] $$

we observe for punctual $f$

$$ \begin{array}{l} \langle \forall c: c = x: p, c \rangle \ = \begin{array}{l} {{(7), ? = x a n d f b o t h p u n c t u a l }} \ {\langle \forall y: y = x: f. y \rangle} \end{array} \ \end{array} $$

$$ \begin{array}{l} \Rightarrow \quad {\mathrm {i n s t a n t i a t i o n} y := x } \ x = x \Rightarrow f. x \ = \left{ \begin{array}{l} \text {p r e d i c a t e c a l c u l u s} \ p. x \end{array} \right} \ \end{array} $$

and this concludes the proof of (0).

This proof became longer than I had ex- pected. I don't feel guilty about postulating (1) and (3) here, but it is bad that they don't occur in our book.

[AB36] A. Bgilsma, “A case of context dependence in predicate calculus”, September 14, 1993, Technical University Eindhoven

[DS90] Edsger W. Dijkstra & Carel S. Scholten, "Predicate Calculus and Program Semantics", Springer-Verlag, 1990 Austin, 22 August 1994

profi. dr. Edsger W. Dgksta Departmen of Compu ter Sciences The University of Texas at Austin Austin, TX 78712-1188 USA