Boolean connectives yield punctual expressions

Boolean connectives yield punctual expressions

Let all through this little note Ig stand for predicate transformers. In that case, we formulate Leibniz's principle as

[\left\lbrack {x \equiv y}\right\rbrack \Rightarrow \left\lbrack {f \cdot x \equiv f \cdot y}\right\rbrack \quad \text{for all}x,y] or -in the style of [GS94] "if $x = y$ is [valid, i.e.] true in all states, then so is $f_{\cdot}x = f_{\cdot}y$ it satisfies the stronger means that (1) $\left\lbrack {\left( {x \equiv y}\right) \Rightarrow \left( {{p}{x} \equiv {p}{y}}\right) }\right\rbrack$ for all ${x}_{2}y$

Remark Property (1) is justly called "stronger". Since $\left( 1\right) \Rightarrow \left( 0\right)$ ,as follows from the mono- tonicity of $\left\lbrack \ldots \right\rbrack$ :

$$ [ x \Rightarrow y ] \Rightarrow ([ x ] \Rightarrow [ y ]) $$

(End of Remark)

An equivalent definition of $f$ 's punc-tuality is $\left( 2\right) \left\lbrack {\left( {x \equiv y}\right) \land f \cdot x \equiv \left( {x \equiv y}\right) \land f \cdot y}\right\rbrack$

Proof. To demonstrate the equivalence of (1) and (2) we observe for any $a, b, c$

$$ \begin{array}{l} [ a \Rightarrow (b \equiv c) ] \ = \quad {\land \Rightarrow = } \ [ a \wedge (b \equiv c) \equiv a \ = {\wedge o v e r \equiv \equiv } \ [ a \wedge b \equiv a \wedge c ] \ \end{array} $$

(By omitting in the above the square brackets, we could have proved a stronger theorem.)

$$ (E n d o f P r o o f) $$

In the remainder of this note, the assumption of $g$ 's punctuality is ex-pressed analogously

$\left( 3\right) \;\left\lbrack {\left( {x \equiv y}\right) \land g \cdot x \equiv \left( {x \equiv y}\right) \land g \cdot y}\right\rbrack .$

The simple theorem to which this note is devoted is

Theorem An expression built from variables and the boolean connectives -quantifica-tion included- is a punctional function of its global - sometimes called "free"-variables.

Such a theorem has to be proved by "mathematical induction over the syntax", i.e. for the base one proves the property for any expression without subexpressions -i.e. without connectives -, and for the step

one proves for each connective the punctuality of the expression it forms, under the assumption that the connective's operands are punctual.

For the base we have to consider:

(i) the constant function, i.e. $\left\lbrack {f \cdot x = z}\right\rbrack$ , for which,according to,say,(1)we have to show

$$ [ (x \equiv y) \Rightarrow (z \equiv z) ] \quad , a n d $$

(ii) the identity function, i.e. $\left\lbrack {f \cdot x = x}\right\rbrack$ , for which,according to,say,(1) we have show $\left\lbrack {\left( {x \equiv y}\right) \Rightarrow \left( {x \equiv y}\right) }\right\rbrack$

Both proofs are trivial.

For the step we have to consider the connectives in turn.

For the equivalence it suffices to derive

$$ [ (x \equiv y) \wedge (f _ {x} \equiv g _ {x}) \equiv (x \equiv y) \wedge (f _ {y} \equiv g _ {y}) ] $$

from (2) and (3). We observe

$$ \begin{array}{l} (x \equiv y) \land (f. x \equiv g. x) \ = {\wedge o v e r \equiv } \ \end{array} $$

$$ \begin{array}{l} (x \equiv y) \land f \cdot x \equiv (x \equiv y) \land g \cdot x \equiv (x \equiv y) \ = {2 a n d (3) } \ (x \equiv y) \wedge f \cdot y \equiv (x \equiv y) \wedge g \cdot y \equiv (x \equiv y) \ \end{array} $$

$$ \begin{array}{r l} & {{\wedge \mathrm {o v e r} \equiv \equiv }} \ & {= (x \equiv y) \wedge (f. y = g. y)} \end{array} $$

For the disjunctio we have to derive $[ (x \equiv y) \land (f \times v g. x) \equiv (x \equiv y) \land (f \cdot y \lor g \cdot y)]$ from (2) & (3); the exercise is left to the reader. Since $\land, \Rightarrow$ , and $\lnot$ can be expressed in terms of $\equiv, \lor$ and the constant false, only quantification is left to be dealt with; because of de Morgan's Law, it suffices to deal with existential quantification only. That is, to be precise, we have to show

$$ [ (x \equiv y) \land \langle \exists i: f _ {i. x} \rangle \equiv (x \equiv y) \land \langle \exists i: f _ {i. y} \rangle ] \mathrm {u n d e r t h e g e n e r a l i z e d a s s u m p t i o n t h a t} $$

(2') $\left\lbrack {\left( {x \equiv y}\right) \land f.1.x \equiv \left( {x \equiv y}\right) \land f.1.y}\right\rbrack$ for all ${x}{2}{y}{1}i$ i.e. we assume the function f.i in the term to be punctual, independently of the value of the dummy i .

The proof is very similar to the previous ones. We observe for any $f$ satisfying (2') and any $x, y$ $\left( {x \equiv y}\right) \land \left\langle {\exists i : f \cdot i \cdot x}\right\rangle$ $= { \land \text{over}\exists }$

$$ \langle \exists i: (x \equiv y) \land f. i. x \rangle $$

$$ \begin{array}{l} = {(\mathbf {2} ^ {\prime}) } \ \langle \exists i: (x \equiv y) \land f _ {i.} y \rangle \ = {\wedge \overline {{o v e r}} \exists } \ (x \equiv y) \land \langle \exists i: f. c. g \rangle \ \end{array} $$

Note that there is no constraint at all on the domain of the dummy; as far as we are concerned it could be uncountably infinite, and as "ill founded" as the reals. We are carrying out "induction on the grammar" and $\langle \exists i : f\left( {i \cdot x}\right) \rangle$ is definitely a finite formula.

The above has been written down in such detail because [GS94] is here rather confusing. I quote from p.60

"LEIBNIZ'S RULE AS AN AXIOM

On p. 12, we introduced Leibniz (1,5):

$$ \frac {X = Y}{E [ z : = X ] = E [ z : = Y ]} \quad \mathrm {o r} \quad \frac {X = Y}{E _ {X} ^ {2} = E _ {Y} ^ {2}} $$

[On p.14, they "reformulate (1.5) as

$$ \frac {X = Y}{g \cdot X = g \cdot Y} \quad E w D ] $$

Now that we have introduced operator $\Rightarrow$ , we can give a version of Leibniz

as an axiom scheme:

$$ \begin{array}{l} (3. 8 3) \quad A x i o m, \quad L e i b n i z: (e = f) \Rightarrow (E _ {e} ^ {2} = E _ {f} ^ {2}) \ (E a n y e x p r e s s i o n) \ \end{array} $$

Inference rule Leibniz says, " $\mathrm{i}f\mathrm{X} = \mathrm{Y}$ is valid,i.e. true in all states,then so is $E\left\lbrack {2 : = X}\right\rbrack = E\left\lbrack {2 : = Y}\right\rbrack$ . " Axiom (3.83),on the other hand,says "if $e = f$ is true in a state,then $E\left\lbrack {2 : = e}\right\rbrack = E\left\lbrack {2 : = f}\right\rbrack$ is true in that state." Thus,the inference rule and the axiom are not quite the same."

The above quotation is so confusing that all by itself it justifies the writing of this note. The verbal explanation suggests that their (1,5) "inference rule Leibniz" corresponds to our (0), whereas (3.83) "axiom Leibniz" corresponds to our (1). But .... here is my problem.

If in "E any expression" E may really be "any expression". I suggest $\left\lbrack {E \equiv g \cdot z}\right\rbrack$ for a non-punctual $g$ . In that case, $E\left\lbrack {z : = e}\right\rbrack = E\left\lbrack {z : = f}\right\rbrack$ becomes $g \cdot e = g \cdot f$ ,which can be false in a state where $e = f$ is true. So then the Axiom is wrong.

We can try to save the Axiom by explicitly restricting expressions to what can be built from boolean variables, constants and the (punctua) connectives.

But then my problem is that under those constraints, their (3.83) is not an axiom but a theorem.

Comparison of their (1,5) & (3.83) with our (0) & (1) respectively suggests that [GS94] suffers from the implicit scopes of the universal quantificaitons over all states. Has the 2-line format of the inference rules been chosen with the understanding that the scope of the universal quantifica tion does not extend over both lines?

[GS94] David Gries and Fred B. Schneider "A Logical Approach to Discrete Math" Springer-Verlag, 1994

Pedernales Falls State Park & Austin, 19 September 1994

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