Another ping-pong argument from Leibniz’s principle

Another ping-pong argument from Leibniz's

Here is -see EWD 1186- another very simple proof in which our obligation to use Leibniz's principle leads to a ping-pong argument. The proof comes from the beginning of lattice theory.

of infx opera: r (up") and $\downarrow$ ("down") and x and y,we are given

(0) $x \uparrow \left( {y \downarrow x}\right) = x$ $\left( 1\right) y \downarrow \left( {x \uparrow y}\right) = y$

The reader is more or less supposed to recognize the Absorption Laws. Please note that (0) and (1) are transformed into each other by the interchange $x, \uparrow \leftrightarrow y, \downarrow$ .

We are asked to prove

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

Please note that the two sides of this equivalence are transformed into each other by that same interchange $x, \uparrow \leftrightarrow y, \downarrow$ .

${P}_{\text{ing }}$ - i.e. ${x}^{ \uparrow }y = x \Rightarrow {y}^{ \downarrow }x = y -$ is proved

$$ \begin{array}{l} y \downarrow x \ = {L H S, i. e. X \uparrow y = x } \ y \downarrow (x \uparrow y) \ = {1 } \ y \quad , \ \end{array} $$

and pong now follows from the symmetries

The ping-pong argument is forced upon us since (0) and (1) do not provide the tools for a (boolean!) value-preserving transformation of $x \uparrow y = x$ into $y \downarrow x = y$ . We have to use the semantics of these two equality signs, i.e. we have to apply Leibniz's principle.

Austin, 15 October 1994

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