A result of rabbit removal

A result of rabbit removal

In this note, all variables are of the same type.

In "Introduction to Logic and to the Methodology of Deductive Sciences" by Alfred Tarski, I found the following theorem - my formulation

Let $\bullet$ be an associative, symmetric infix operator such that

(0) equation $x$ : $a = b \cdot x$ is solvable for all $a,b\;i$ then $\left( 1\right) \;x \cdot y = x \cdot z \Rightarrow y = z\;\therefore$

In comparison, Tarski calls his calculational proof "considerably more involved"; it was in any case too complicated to be remembered (at least: by me), it also seemed to me to be more complicated than necessary. (This last judgement was, of necessity, very tentative, because without detailed analysis it was impossible to see how much of the complexity belonged to the argument proper, and how much of it was the result of the style of presentation deemed acceptable in the 30s. Of course we cannot

blame Tarski for having done most of his work before Wim Feigen developed his proof format.)

Under the circumstances there was only one acton possible for me, viz. to ignore what I had seen and could not remember, and to try to design a proof myself. (Here, the ambitious reader is invited to stop reading and to try to prove the theorem himself.)

Since the consequent of our demonstrator (1) is the equality $y = z$ ,the suggested structure of our proof could be

"We observe for any $x,y,z$

$$ = \begin{array}{l l} y & \ z & \end{array} \left{ \begin{array}{l l} \mathrm {a n t e c e d e n t} & x \cdot y = x \cdot z \end{array} \right} $$

but this sketch contains little more than a proposal how to let the proof structure reflect that our demonstrum has the shape of an implication.

In the one and only step of the above proof sketch, an equality has to be justified by an equality, hence an application of Leibniz's principle is dictated! Our next

proof sketch is therefore:

"We observe for any $x,y,z$

$$ \begin{array}{l} = \begin{array}{l} y \ f. (x \cdot y) \end{array} \left{ \begin{array}{l} \text {d e f i n i t i o n o f} f \end{array} \right} \ = \left{ \begin{array}{l l} \mathrm {a n t e c e d e n t} & x \cdot y = x \cdot z \ f. (x \cdot z) & \end{array} \right} \ = {d e f i n i t i o n o f f } \ \end{array} $$

Remark As far as the use of the antecedent via Leibniz's principle is concerned, one could consider the alternative

$$ \begin{array}{l} = \begin{array}{l} y \ f. (x \cdot z) \end{array} \quad \left{ \begin{array}{l} \text {d e f i n i t i o n o f} f \end{array} \right} \ = \left{ \begin{array}{l l} \mathrm {a n t e c e d e n t} & x \cdot y = x \cdot z \ f. (x \cdot y) \end{array} \right} \ = \begin{array}{l} \left{\mathrm {d e f i n i t i o n o f} f \right} \ z, \end{array} \ \end{array} $$

but that does not work, and we shall later see why. (End of Remark.)

Our next task is to design a suitable $f$ , i.e. to propose how to rewrite $y$ as an expression that contains $x \cdot y$ as subexpression. Since $•$ is the only operator

defined on our type, we have little freedom:

(0) with $a,b \mathrel{\text{:=}} y,x \cdot y$ allows us to post- tulate that $p$ satisfies

(2) $y = x \cdot y \cdot p\;\therefore$

and now our proof can start as follows:

$$ \begin{array}{l} = y \quad {(2) } \ x \cdot y \cdot p \ = {\mathrm {a n t e c e d e n t} x \cdot y = x \cdot z } \ x \cdot z \cdot p \ \end{array} $$

Our remaining problem is how to transform $x \cdot z \cdot p$ into $z$ , and we have little choice but to use the same (2), which has just been used for $(x, p)$ -introductiOn, a second time, but now for $(x, p)$ -removal. But for this removal to work, we need a temporary reintroduction of $y$ . For rewriting $z$ so that it contains $y$ as subexpression, the simplest solution, allowed by (0) with $a, b := z, y$ , is to postulate that $q$ satisfies

$$ (3) \quad z = y \cdot q $$

And now we can give the complete proof. For any $x, y, z$ , we postulate, as permitted by (0), that $p$ satisfies (2) and $q$ satisfies

fies (3), and subsequently we observe

$$ \begin{array}{l} = \left{ \begin{array}{l l} y & \Delta y \ (2) \end{array} \right}. \ x \cdot y \cdot p \ = {x \cdot y = x \cdot 2 } - 1 + 1 \ x \cdot 2 \cdot p \ = {(3) } + 1 - 1 + 1 \ x \cdot y \cdot q \cdot p \ = {(2) } - 1 \ y \cdot 9 \ = \left{ \begin{array}{l l} (3) \ 2 \end{array} \right} \ \end{array} $$

To the right of the proof we have rec- corded the changes in the number of occur rences of variables $y,z,p,q$ . Because the net effect of the appeals to (2) and (3) is $\Delta p = 0\wedge \Delta q = 0$ , it yields $\Delta y = 0\wedge \Delta z = 0$ as well. The total effect of the proof (whose steps transform y into z) has to be $\Delta y = -1\wedge$ $\Delta z = +1$ , and this is the change provided by the use of the antecedent via Leibniz's principle. This counting argument explains why the al-. ternative proof sketch in the Remark does not work: it works in the wrong direction, viz. $\Delta y = +1\wedge \Delta z = -1$

*

To put the above proof into perspective, let me render -reduced to its essentials - Tarski's proof.

For any $x, y, z$ , we postulate, as permitted by (0), that $u, v, w$ satisfy

$\left( 4\right) y = y \cdot u$ (5) $z = y \cdot v$ (6) $u = x \cdot w$

and subsequently observe

$$ \begin{array}{l} = \begin{array}{l} y \ {(4) } \end{array} \ = \begin{array}{l} y \cdot u \ {6 } \end{array} \ y \cdot x \cdot w \ = { \begin{array}{l} x \cdot y = x \cdot z \end{array} } \ = \left{ \begin{array}{l} {(6)} \ {2 \cdot u} \end{array} \right} \ = \left{ \begin{array}{l l} (5) \end{array} \right} \ \begin{array}{r l} & {= {(4) }} \ & {y \cdot v} \ & {= {(5) }} \ & {z} \end{array} \ \end{array} $$

Tarski's proof is 2 steps longer than ours because

of the occurrence of

troduced, and removed later. In fact, our

proof can be obtained from Tarski's by eliminating $u$ from (4) & (6).

It is not quite clear

why u was introduced in the first place ; could it have happened because the heuristics

remained completely implicit?

The structure of Tarshi's proof was further obscured by his insistence of fully parenthe

sizing his expressions: symmetry and asso- ciativity thus add another 7 steps to the proof, which I consider a high price for so little.

About 20 pages later, he proves another theorem - again my formulation- Let $\bullet$ be an infix operator that is symmetric and associative wherever defined, and such that

(0) equation $x : a = b \cdot x$ is solvable for all $a,b\;i$ then (7) $x \cdot y$ is defined for all $x,y$

The plan of the proof is to construct, as permitted by (0), for given $x, y$ , a quantity $z$ which, by virtue of its construction, can be transformed into $x \cdot y$ . For reasons of heuristics, we start at the other end and ask ourselves what we have to introduce that will enable us to transform $x \cdot y$ into $z$ .

Starting from

(α)

$x \cdot y$

we have to do 3 things: remove x, remove $y$ ,and introduce

achieve 2 of them by defining -as (0) allows us to do - z for suitably chosen

(8) $z : \;y = w \cdot z\;$

then (x) can be rewritten as

$\left(\beta\right)$ $x \cdot w \cdot z$

The remaining task consists of 2 things, viz. removal of $x$ and removal of $w$ . Remembering (i) that, as yet, $w$ is undefined, and (ii) that $(\beta)$ provides the environment in which to exploit that is associative, we can effectively both removals by defining - as (0) allows us to do- $w$ for suitably chosen $u$ by

(9) $w : \;u = x \cdot w$

then (β) can be rewritten as

$\left( y\right)$ $u \cdot z$

The remaining task is to choose $u$ in such a way that we can remove it. For given $z$ , (0) would allow us to define $u$ by

$$ z = z \cdot u $$

and -thanks to the symmetry of $\bullet -$ such

and (9), our $z$ is functionally dependent on u. Having to define u independently of $z$ , we generalize our last relation and define -as (0) allows us to do- u for suitably chosen c by

$$ (1 0) \quad u: \quad C = C \cdot u, $$

and hope that we can find a c that does the job

Appealing to (10) requires in our re-writing exercise the temporary introduction of $C$ into the intermediate result. Also, for the very last step of the transformation, we need an expression that can be equated to 2 . These two considerations suggest a next - and last- appeal to (o) : we define v by

$$ (1 1) \quad v: \quad z = c \cdot v. $$

Now the transformation continues:

$$ \begin{array}{l} (\gamma) \quad u \cdot z \ = {(1 1) } \ u \cdot c \cdot v \ = {(1 0) } \ C \cdot V \ = {(\mathbf {1}) } \ z \ \end{array} $$

and we are done. For $c$ ,any element will do.

In summary: choose a C, define in order u by (10), w by (9), 2 by (8)

$$ \begin{array}{l} z \ = {(1 1) } \quad c \cdot v \ = {(1 0) } \quad u \cdot c \cdot v \ = {(1 1) } \quad u \cdot z \ = {(9) } \quad x \cdot w \cdot z \ = {(8) } x \cdot y \ \end{array} $$

Tarski's presentation of this proof is obscured by the fact that without any comment he has made the arbitrary choice $c = y$

Ref. Tarski, Alfred, "Introduction to Logic and to the Methodology of Deductive Sciences", Dover Publications Inc., New York, 1995

Austin, 11 June 1995

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