A kind of converse of Leibniz’s Principle

A kind of converse of Leibniz's Principle

by

Edsger W. Dijkstra

We owe to Gottfried W. Leibniz the principle that is informally known as "substituting equals for equals" and is formally expressed by

$$ x = y \Rightarrow f \cdot x = f \cdot y $$

which we can also read as "function

Theorem Besides the two constant relations, equality is the only relation preserved by function application.

In this note, function application is denoted by an infix dot (period); for the sake of simplicity we restrict ourselves to "endofunctions", i.e. functions for which argument and function value are of the same type, which is also the type of the variables $\left( {a,b,c,d,x,y}\right)$ and the type on which the binary relations are defined.

Boolean negation will be denoted by $\neg$ , boolean equality by $\equiv$ ,which is given the lowest syntactic binding power ; the dot of function application has the highest binding power.

For the rest of this note, $\mathcal{R}$ denotes - in the usual infix notation - a binary relation

• that differs from the constant relation $T,\;g i v e n\;b\;y\;\left( {\forall x,y : x{T}_{y}}\right) \;$ ,and
• that differs from the constant relation $F,given\;{by}\;{\left\langle \forall x,y\; : \neg \left( x + y\right) \right\rangle }_{,}$ and that differs from equality

To prove our theorem we have to show that, in general, $\mathcal{R}$ is not preserved by function application, i.e. that there exist an $a, b$ and $f$ such that

$a{Rb}$ and

We take care of the existential quantification over $f$ by using the lemma - not proved here

$\left\langle {\exists f : f.a = c \land f.b = d}\right\rangle \equiv \;a = b \Rightarrow c = d\;\therefore$

which allows us to rewrite our proof obligation as follows:

Show the existence of a quadruple $\left{ {a,b,c,d}\right}$ such that

(i) $a{Rb}$ (i) $\neg \left( {c\mathbf{R}d}\right)$ (iii) $a = b \Rightarrow c = d$

We now show this existence by construct- ing a witness.

That R differs from equality enables us to postulate (for the rest of this note) for some $x,y$

$$ x \Re y \neq x = y $$

and now we distinguish two cases.

$$ \mathrm {C a s e 0 :} \quad x R y \land x \neq y. $$

Choosing $a, b \mathrel{\text{:=}} x,y$ ensures that (i) and (iii) are satisfied; because $R$ differs from $T$ , $c,d$ can be chosen so as to satisfy (ii). (End of Case 0)

$$ \mathrm {C a s e 1 :} \quad \neg (x R y) \land x = y $$

Choosing $c,d \mathrel{\text{:=}} x,y$ ensures that (ii) and (iii) are satisfied; because $R$ differs from $F$ , $a,b$ can be chosen so as to satisfy (i) (End of Case 1)

Since the case analysis was exhaustive,

our proof obligation has been discharged.

Remark The unproved lemma can be demonstrated by mutual implication. The one direction left $\Rightarrow$ right follows directly from Leibniz's Principle; the other direction -the one needed in this note - requires a case analysis, say $a = b$ versus $a \neq b$ . (End of Remark.)

Austin, 17 September 1996

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