up arrow proof

(back to 3.1.2)

In this page I will prove that in Bowers' array notation, {a,b,c} is equal to a^cb for all a, b, and c. I will prove it like so:

- Prove that {a,b,1} = a^b

- Prove with induction on b that {a,b,2} = a^^b

- Prove inductively that {a,b,c} = a^cb with induction on b and c

First off, it's easy to see why {a,b,1} = a^b. For this array, we follow rule 2 of array notation (remove the 1 at the end), giving us the array {a,b}, which evaluates to a^b.

Now let's try to see if {a,b,2} = a^^b. We'll prove it inductively, first showing that {a,1,2} = a^^1, then that if {a,b,2} = a^^b, then {a,b+1,2} = a^^(b+1).

To evaluate {a,1,2}, we follow the 3rd rule (2nd entry is 1), which states that if the second entry of an array is 1, then the array evaluates to the first entry. Then, {a,1,2} evaluates to a, which is the same as a^^1.

Now, let's assume that {a,b,2} = a^^b. Does a similar equality hold for {a,b+1,2}? To find out, we calculate:


= {a,{a,b,2},1} [rule 5]

= {a,{a,b,2}} [rule 2]

= {a,a^^b} [given]

= a^(a^^b) [rule 1]

= a^^(b+1) [definition of up-arrow notation]

Now let's try a more general case. Let's assume that {a,b,c} = a^cb, and that {a,b,c-1} = a^c-1b as well. Then, we will need to show that {a,b+1,c} = a^c(b+1), and that {a,b,c+1} = a^c+1b.

If {a,b,c} = a^cb, then:


= {a,{a,b,c},c-1}

= a^c-1({a,b,c})

= a^c-1(a^cb)

= a^c(b+1)

And also, if {a,b,c} = a^cb, then we need to first show that {a,1,c+1} = a (same thing as a^c+11), and then that if {a,b,c+1} = a^c+1b then {a,b+1,c+1} = a^c+1(b+1). This will complete the proof.


= a (rule 3 tells us to remove the 1)



= {a,{a,b,c+1},c}

= a^c(a^c+1b)

= a^c+1(b+1)

So we have now completed the proof of translating Bowers' array notation to Knuth's up-arrows.