November 10, 2000 November 10, 2000

The source for this problem is Donald Knuth, The Art of Computer Programming, Volume 1 Fundamental Algorithms, Third Edition. His Example 2., page 30 begins with a proof that
n

i = 0 
i

j = 0 
aiaj = n

i = 0 
n

j = i 
aiaj  .

Its proof is in the vein of the fourth problem on the fourth assignment. It is formulated in the notation of the text as
(+i | 0 i n:(+j | 0 j i : a[i]a[j])) = (+i | 0 i n:(+j | i j n : a[i]a[j])) .

(+i | 0 i n:(+j | 0 j i : a[i]a[j]))
=

(8.20), j d.n.o.f. in 0 i n.

(+i,j | (0 i n) (0 j i) : a[i]a[j])
=

Axiom, (*x,y | P:Q ) = (*y,x | P:Q )

(+j,i | (0 i n) (0 j i) : a[i]a[j])
=


Lemma: (0 i n) (0 j i) (0 j n) (j i n),
Leibniz 8.12. Proof of Lemma appears below.


(+j,i | (0 j n) (j i n) : a[i]a[j])
=

(8.20), i d.n.o.f. in 0 j n.

(+j | 0 j n:( +i | j i n : a[i]a[j]))
=

(8.21) applied four times (see below)

(+i | 0 i n:( +j | i j n : a[j]a[i]))
=

Arithmetic, a[j]a[i] = a[i]a[j]

(+i | 0 i n:( +j | i j n : a[i]a[j]))
Now for the proof of the Lemma:
(0 i n) (0 j i)
=

Notation

(0 i) (i n) (0 j) (j i)
=


|- (j i)(i n) (j n) by (15.41)(d).
Apply (3.60) to obtain |- (j i)(i n) (j i)(i n)(j n).


(0 i) (i n) (0 j) (j i)(j n)
=


|- (0 j) (j i) (0 i) by (15.41)(d).
Apply (3.60) to obtain |- (0 i) (0 j) (j i) (0 j) (j i) .


(i n) (0 j) (j i)(j n)
=

(3.36), (3.37)

(0 j) (j n) (j i) (i n)
=

Notation

(0 j n) (j i n)
The proof uses (15.41)(d), the transitivity property for .

For the step which uses (8.21), choose k and l fresh variables. Then apply (8.21) to rename the dummy i to k and afterwards (8.21) to rename the dummy j to l. As there are no free occurrences of i or j now ``reverse'' by renaming k to j and then l to i. To formalize write down (8.21) in each case and apply Transitivity three times.

We have already discussed (8.13) Axiom, Empty Range. For (8.14) Axiom, One-point rule observe that there is a restriction that there are no free occurrences of the object variable x in the expression E. The following examples show what can happen if one ignores this restriction:

Consider

(+x | x = x2-2x+2:x) = x2-2x +2
and
("| x = x2-x +1: x = 1) (x2-x+1 = 1)

Show that neither are theorems by finding an interpretation for which each is false.


File translated from TEX by TTH, version 2.60.
On 9 Nov 2000, 21:04.