Ping-pong arguments and Leibniz’s principle

$\frac{P\left( {1 + u}\right) }{P\left( {1 - u}\right) } = \frac{u}{\left( {1 + u}\right) \left( {1 - u}\right) }$

Let $\downarrow$ denote an idempotent,symmetric, and associative infix operator; it is given a higher binding power than the relational operators.

In terms of $\downarrow$ we define a relation $\leq$ by postulating for any $x,y$

$x \leq y \Rightarrow x \downarrow y = x$

We would like to prove for any $w,x,y$

$\omega \leq x \downarrow y \equiv w \leq x \land w \leq y$

Applying (0) three times to eliminate the ss, we rewrite demonstrandum (1) as

(2) ${w}^{ \downarrow }{x}^{ \downarrow }y = w \equiv {w}^{ \downarrow }x = w \land {w}^{ \downarrow }y = w$

We use Leibniz's Principle in the form

$$ a = b \land f. a \Rightarrow f. b $$

and proceed to prove (2) by a ping-pong argument. For pong we observe for any $w,x,y$

$$ w \downarrow x = w \wedge w \downarrow y = w $$

$$ \begin{array}{l} \Rightarrow \quad {\mathrm {L e i b n i z} } \ (w \downarrow x) \downarrow y = w \ = {\downarrow a s s o c i a t i v e } \ w \downarrow x \downarrow y = w \ \end{array} $$

$$ \begin{array}{l} \begin{array}{l} {\mathrm {f o r p i n g w e a n l y p r o v e (f o r b r e v i t y s}} \ {\mathrm {s a k e) w \downarrow x \downarrow y = w \Rightarrow w \downarrow x = w b y o b s e r v i n g}} \end{array} \ w \downarrow x \downarrow y = w \ = {p r e d i c a t e c a l c u l u s } \ = {\downarrow^ {i} d e m p o t e n t + } \ w \downarrow x \downarrow y = w ^ {\prime} \wedge w \downarrow (x \downarrow x) \downarrow y = w \ = {\downarrow \mathrm {s y m m e t r i c a n d a s s o c i a t i v e} } \ w \downarrow x \downarrow y = w \wedge (w \downarrow x \downarrow y) \downarrow x = w \ \Rightarrow \quad {L e i b n i z } \ w \downarrow x = w \ \end{array} $$

It was a pleasant surprise to see that (1) had a simpler proof via (2) than via all sorts of other properties of $\leq$ . The reason for recording the proof, however, is that its structure reveals Leibniz's Principle as a generator of ping-pong arguments. (Moreover, for a lecture on Leibniz's Principle, it is a very nice example.)

Austin, 3 September 1994

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