Elementary predicates and elimination (with A.J.M. van Gasteren)

Elementary predicates and elimination

In a recent manuscript "Some theory about predicate transformers and equations in predicates," C.S. Scholten introduced the notion of "elementary predicates" to capture the notion of points in state space. In the following, p and q will be used to denote elementary predicates. Scholten introduced them with the following two Axioms for elementary predicates

Axiom 0: $\left\lbrack {\left( {{E}_{p} : p}\right) }\right\rbrack$

Axiom 1: For all predicates $P$ and all elementary predicates $q \left\lbrack {q ⇒ P}\right\rbrack ≠ \left\lbrack {q ⇒ ¬ P}\right\rbrack$

For $P$ a predicate on a space with $x$ as one of its coordinates, a by now beloved definition of $P_{x^1}^x$ , with $x^1$ a fresh variable, is

(A : X) ≠ X' ∨ P)

Another way of describing the substitution in $P$ of $x^{\prime}$ for $x$ is the elimination of $x$ from the pair of equations $P$ and $Q$ , with for $Q$ the expression $x = x^{\prime}$ . Now (a) is of the form

(Ax: YQ v P)

a form which is not symmetric in $P$ and $Q$ ! That it is a genuine asymmetry is shown by the following ex- ample.

$P : {abs}\left( x\right) = 1$

Q: $x = y$

Elimination of $x$ from $P ∧ Q$ obviously yields $abs\left( y\right) = 1$ .

Indeed $\left( {{A}_{x} : {7Q} \vee P}\right) \equiv abs\left( y\right) = 1$ for all $y$ . However, (Ax:7PvQ)E false for all y. The rest of this short note is devoted to the investigation of this phenomenon.

Let $R$ be a predicate in $x$ and $y$ . Eliminating $x$ from $R$ boils down to constructing the strongest predicate in $y$ that holds for all solutions of $x, y: R$ ; it is

(2) $\left( {{\underline{\mathrm{E}}}_{\mathrm{x} : : }\mathrm{R}}\right)$

With $P$ and $Q$ predicates in $x$ and $y$ ,application

(3) $\left{ {{E}_{X} : P ∧ Q}\right}$ ,

an expression which is nicely symmetric in $P$ and $Q$ . We shall now give a sufficient condition on $Q$ such that (1) and (3) are the same predicate in $y$ . The condition is

$\left\langle {A,y : \left( {\underline{N}x : Q}\right) = 1}\right\rangle$

Relation (4) in a sense expresses that for each $y$ $Q$ is an elementary predicate in $x$ . It allows us to derive for $Q$ the analogue of Scholten's Axiom 1.

For any value $y$ and any predicate $P$ we have

\begin{array}{l} (N \times : Q) = 1 \ = {\left[ Q \equiv (Q ∧ P) \vee (Q ∧ ¬ P) \right] } \ (N \times : (Q ∧ P) \lor (Q ∧ ¬ P)) = 1 \ = {\left[ ¬ ((Q ∧ P) ∧ (Q ∧ ¬ P)) \right] } \ (N x: Q \wedge P) + (N x: Q \wedge ¬ P) = 1 \ ⇒ {\mathrm {a r i t h m e t i c} } \ \end{array}

\begin{array}{l} (\underline {{N}} x: Q \wedge P) ≠ 0 \equiv (\underline {{N}} x: Q \wedge ¬ P) = 0 \ = {\text {p r e d i c a t e c a l c u l u s} } \ (E x: Q \wedge P) \equiv (A x: 7 Q \vee P) \ \end{array}

Note. Since -predicate calculus-

(E x: Q ∧ P) \equiv ¬ (A x: ¬ Q \lor ¬ P),

the last line of the above derivation is the analogue of Scholten's Axiom 1. (End of Note.)

Since the implication derived above holds for any value $y$ ,satisfaction of (4) allows us to conclude that (3) and (1) express the same predicate in $y$ .

From the above follows the following

Corollary. If for predicates $P$ and $Q$ in $x$ and $y$

\underline {{A}} y: (\underline {{N}} x: P) = 1 ∧ (\underline {{N}} x: Q) = 1)

holds, then

(\underline {{A}} y: (\underline {{A}} x: Q ⇒ P) = (\underline {{A}} x: P ⇒ Q))

(End of Corollary.)

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

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