Leibniz’s Principle (Mathematical Methodology)

The complicated attracts attention, the seemingly simple tends to be ignored, and I am afraid that the latter fate of neglect has befallen the notion of equality.

One symptom of that neglect is that there was no symbol to denote equality before 1557, when Robert Recorde introduced the equal- ity sign $=$ as we know it today. Prior to Recorde's invention, equality was indicated verbally, by an abbreviation thereof, or even implicitly, e.g. by mere juxtaposition.

Another symptom of that neglect is that it took another three centuries before acquired the full status of an infix oper-ator: only after the introduction of the boolean domain in 1854 could $x = y$ be considered an expression, capable of taking on a value.

A final striking fact is that the formula- tion of equality's most characteristic property had to wait for Leibniz, who lived more than a century later than Recorde. Leibniz

had the insight to formulate -among many other things- equality's property of being preserved under function application.

Equality is really a notion we grew up with. I think we knew subconsciously that equality is a symmetric function of its arguments:

(0) $x = y \equiv y = x,$

before we could doubt. I am now per- fectly willing to accept (o) as a postulate: equality is defined on an unordered pair.

To appreciate Recordie's invention, we should switch back from (0) to a sentence like "The farmer has twice as many cows as his son has sheep", which all but hides that equality is a symmetric notion: if the above sentence expresses $C = 2 \cdot S$ , try to express ${2.5} = c$ similarly,and you will notice that it cannot be done!

Another familiar property of equality -and a property we have subconsciously used before we could formulate it- is that equality is transitive, i.e.

$x = y \land y = z \Rightarrow x = 2$

Mathematical Methodology

Emotionally, equality's transitivity strikes me as "basic", as "fundamental" as its symmetry, but emotions can be misleading: equality's transitivity need not be postulated since -as we shall show below - it follows from Leibniz's Principle (2).

With $f$ a function, and $x$ and $y$ variables of $f$ s argument type, Leibniz's Principle states

$$ (2) \quad x = y \Rightarrow f \cdot x = f \cdot y $$

In its application it is understood that we may view an expression as a function applied to one of its subexpressions; we are, for instance, allowed to conclude

$$ a = b \Rightarrow (a + 3) ^ {2} = (b + 3) ^ {2} $$

because it is an instantiation of (2). (For those readers that have seen the $\lambda$ -calculus, I can give the instantiation of (2):

$$ x, y, f := a, b, (\lambda y: (y + 3) ^ {2}) \quad .) $$

To show that (1) follows from (2), we first observe for any $x,y,z,g$ of the appropriate types

Mathematical Methodology

true

$$ \begin{array}{l} = {(2) \mathrm {w i t h} f := (\lambda u: g. u = z) } \ x = y \Rightarrow (g \cdot x = z \equiv g \cdot y = z) \ \Rightarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ x = y \Rightarrow (g \cdot y = 2 \Rightarrow g \cdot x = 2) \ = {\text {p r e d i c a t e c a l c u l u s} } \ x = y \land g \cdot y = 2 \Rightarrow g \cdot x = 2 \ \end{array} $$

Substituting in the last conclusion for $g$ the identity function yields (1), and thus we have shown that (1) follows from (2).

Leibniz's Principle (2) states that function application preserves equality, but the link between equality and function application is, in fact, stronger: besides the constant relations $T$ and $F$ , equality is the only relation that is preserved under function application. (The constant relations $T$ and $F$ are given by: for all $x, y$

$$ (x T y) \equiv \mathrm {t r u e} \qquad \mathrm {a n d} \qquad (x F y) \equiv \mathrm {f a l s e}. $$

Since predicate calculus tells us

true $\Rightarrow$ true and false $\Rightarrow$ false

we can conclude for all $x,y,p$ of matching

$$ (x T y) \Rightarrow (p _ {x} T p _ {y}) a n d (x F y) \Rightarrow (p _ {x} F p _ {y}), $$

Mathematical Methodology

i.e. function application preserves T and F . For any relation other than $T,F$ ,or $=$ , one can construct an $f$ that does not preserve it.)

The strength of the link between function application and equality manifested itself in yet another way. Over the years, my proofs became more and more calculational, and, to the best of my knowledge, the many proofs I designed all share the following characteristic: the only use made of equality is that it is preserved under function application, the only use made of the notion of a function is that function application preserves equality.

By way of illustration, consider the following theorem; here, an infix $\uparrow$ is used to denote the maximum of two real operands.

Theorem Let $f$ be a function from real to real that distributes over the maximum, i.e. for all $x, y$

$f\left( {x \uparrow y}\right) = f \cdot x \uparrow f \cdot y$ then $f$ is monotonic, i.e. for all $x, y$ $x \leq y \Rightarrow f \cdot x \leq f \cdot y$

Now the following observations can be made.

• Not all functions from real to real are monotonic; hence, the proof of (4) requires the use of (3). We can only use (3) in a context in which $\uparrow$ occurs. Leibniz's Principle is our only tool for the introduction of $p$ applications in the consequent, so Leibniz's Principle has to be used.
• We can only use Leibniz's Principle in a context in which $=$ occurs.

So, the question is now, how to introduce

Here I assume the availability of the

Lemma For all real $x,y$

$x \leq y \equiv {x}^{ \uparrow }y = y$

(We do not prove that lemma here. The proof depends on how $\leq$ and I have been defined.)

For the proof of our theorem we observe for any real $x,y$

Mathematical Methodology

$$ \begin{array}{l} f _ {x} \le f _ {y} \ = {(5) \mathrm {w i t h} x, y := f ^ {\prime} x, f ^ {\prime} y } \ f \cdot x \uparrow f \cdot y = f \cdot y \ = {(3) } \ f. (x \uparrow y) = f. y \ \Leftrightarrow {L e i b n i z } \ x \uparrow y = y \ = {\langle 5 \rangle } \ x \leq y \ \end{array} $$

which concludes the proof, of which each step seems unavoidable.

In this chapter we introduced the equality by means of two postulates, viz. symmetry and Leibniz's Principle. They can be combined into a single postulate, viz. that

$$ (6) \qquad x = y \Rightarrow f \cdot y = f \cdot x $$

(Instalntiating (6) with for $f$ the identity

$$ x = y \Rightarrow y = x $$

instantiating the latter with $x,y \mathrel{\text{:=}} y,x$

$$ y = x \Rightarrow x = y $$

and (0) now follows by mutual implication.)

Minimizing the number of postulates seems a defensible goal, but I think their disentanglement more important. Symmetry is a notion that is totally independent of Leibniz's Principle or preservation in general - e.g. $a + b = b + a -$ ; preserva- tion under function application makes perfect sense for nonsymmetric relations - e.g. $x < y \Rightarrow f.x < f.y$ for monotonic $f - .$

Let me end this chapter with a plea not to misuse the equality sign. In a standard work on graph theory, vertices are labelled by letters, and arcs by integers. Arc 2 going from vertex $\mathbf{a}$ to vertex $\mathbf{b}$ is written as

$$ 2 = (a, b) $$

arc 3 also goes from vertex a to ver-

which is written as

$$ 3 = (a, b) $$

Since one now must make an effort not to conclude $2 = 3$ ,we deplore the above mis-

Mathematical Methodology

use of the equality sign. The bad habit is not confined to graph theory; shortly after I had encountered it there, I discovered in a lecture a "formula" of the form

$$ e x p r e s s i o n = P _ {h} (\omega_ {1}, \dots , \omega_ {n}) $$

used to state that the expression in question was a homogeneous polynomial in the variables ${\omega }{1},\ldots ,{\omega }{n}$ .

Remark Natural language is here as confusing as usual. From "Susy is my mother" and "John's wife is my mother", you may conclude "Susy is John's wife", but this conclusion can not be drawn from "Susy is my sister" and "John's wife is my sister". It is unwise to import such confusing subtleties into one's for malisms. (End of Remark.)

Austin, 25 April 1990

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