EWD1216

The equation x:[x]

For equality between "predicates' x and y we introduce the notation [x ≡ y]. For f a function of type predicate→predicate Leibniz's Principle is accordingly expressed as

      [x ≡ y]  ⇒  [f.x ≡ f.y]   .

We now dissect this notation into

(i) the square brackets [ ], which denote a function of type predicate→{true, false}

(ii) the infix operator ≡ which is of type predicate²→predicate and is postulated to be associative and symmetric.

Parsing the relation [(x ≡ y) ≡ (y ≡ x)] that expresses the symmetry as [x ≡ ((y ≡ y) ≡ x)] and [(x ≡ (y ≡ y)) ≡ x], we see that y ≡ y is both left and right identity element of ≡ . Since for an infix operator that has a left identity element and a right identity element, these are equal and unique, we can name the unique identity element of ≡, say by TRUE:

      [x ≡ TRUE ≡ x]

This immediately leads to

   [x] ⇒ [x ≡ TRUE]

i.e. equation x:[x] has a unique solution which equals the identity element of ≡ (and hence, [x] is false for all other values of x).

Remark. It is usual to write TRUE in lower case. (End of Remark.)

The above has been written for David Gries.

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

---

Transcribed by Guy Haworth.

Last revised Sun, 30 Dec 2007.