WLOG, or the misery of the unordered pair

wlog, or the misery of the unordered pair

Let $p, q$ be predicates on unordered pairs of some type, i.e. (for all $x, y$ )

(0) $p \cdot \left( {x,y}\right) \equiv p \cdot \left( {y,x}\right) \;$ and $q \cdot \left( {x,y}\right) \equiv q \cdot \left( {y,x}\right)$ , and suppose we have to prove (for all $x,y$ $p \cdot \left( {x,y}\right) \Rightarrow q \cdot \left( {x,y}\right)$ Suppose we can prove the weaker theorem $\Rightarrow q.\left( {x,y}\right) \Leftrightarrow q\left( {x,y}\right) \Leftrightarrow q\left( {x,y}\right) \Leftrightarrow q\left( {x,y}\right) \Leftrightarrow q\left( {x,y}\right) \Leftrightarrow q\left( {x,y}\right) \Leftrightarrow q\left( {x,y}\right) \Leftrightarrow$ By renaming in (2) with $x,y \mathrel{\text{:=}} y,x$ and appealing to (0), we immediately get (3) $p \cdot \left( {x,y}\right) \land r \cdot y \Rightarrow q \cdot \left( {x,y}\right)$ and thus the proof of (2) also establishes the conjunction of (2) and (3): (4) $p \cdot \left( {x,y}\right) \land \left( {r \cdot x \vee r \cdot y}\right) \Rightarrow q \cdot \left( {x,y}\right)$ which is equivalent to our demonstrandum (1) provided (5) $p \cdot \left( {x,y}\right) \Rightarrow r \cdot x \vee r \cdot y$

The above describes what WLOG (= Without

Loss of generality) is usually about. In principle -as shown above- the technique is perfectly sound, but the problem is that in practice it is only too often appealed to by the mere "wlog we can assume rx" without formulating, let alone proving (5). Often, the underlying symmetry is not mentioned either, and such omissions make most "wlog proofs" rather unsatisfactory.

When I was introduced to the technique, (2) would be proved, and the proof of (3) would be omitted on the ground that mutatis mutandis that proof would be the same. At the time we were sufficiently vague about quantification and the role of dummies not to be able to see that (2) and (3) are the same theorem, the textual difference being introduced by our use of $\left( {x,y}\right)$ to denote an unordered pair.

Austin, 12 November 1995

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