Suppose that you’re translating an ancient text, and in this text you come across three words whose meaning you are unsure of: , , and . So, you head down to the ancient language department of your local university.

The first professor you come across, , knows what means, the second professor you come across, , knows what means, and the third professor you come across, , knows what means. So you have fortunately solved your problem.

But you’re now curious and decide to meet some other professors in the department. The next professor you come across is named . He doesn’t know what means or what means, but if you told him what meant, he would be able to tell you what means (for example, maybe he knows that is the noun form of ).

The next professor you meet is named . If you told him what meant and what meant, he would be able to tell you what means.

The next professor you meet is named . If you told him a *method* for finding out the meaning of given the meaning of , he would be able to tell you the meaning of .

In general, for any two professors and , there is a professor with the property that if you told him what knew, he would be able to tell you what knows (but doesn’t know any more than that).

Notice that some professors have essentially the same state of knowledge. For example, and have essentially the same knowledge, since to get the meaning of out of you only have to tell him a method for finding out the meaning of given the meaning of , which is something that you can do without any particular special knowledge concerning , and .

A more nontrivial example is that has the same state of knowledge as . This is because each can “simulate” the other. In one direction, suppose somebody told the meaning of . He therefore knows a trivial “method” for getting the meaning of given any inputs, and so he knows the meaning of . In the other direction, suppose we told a method for turning (methods for turning the meaning of into the meaning of ) into the meaning of . Well, knows a method for turning the meaning of into the meaning of , so he can use that find the meaning of . He can then use his method a second time to turn that into the meaning of .

The puzzle is then to prove that there are only finitely many professors with different states of knowledge.

This puzzle is equivalent to showing that intuitionistic implicational propositional logic over three variables has only finitely many logically inequivalent formulas. Another formulation is: Let be the free cartesian closed category over objects. Given objects and , say that and are equivalent if there is an arrow from to and an arrow from to . Then there are only finitely many equivalence classes in . (The corresponding statements are also true with replaced by .)

This fact was first proved using algebraic methods by Arturo Diego in his Ph.D. thesis in the 1940’s. It was subsequently reproved using semantic methods by various people including Nicolaas de Bruijn and Alasdair Urquhart. A good overview of those results is in Lex Hendriks’s thesis. I proved it in a combinatorial way as part of my thesis.

To rigorously state the problem: Let be a finite set of propositional variables, and let be the smallest set containing and such that if formulas and are in , then the formula is in . We define a relation between sets of formulas in and formulas in as follows: We will let be the smallest relation such that, for any , :

- .
- If and , then .
- If and , then .
- If , then .

The relation formalizes the notion of a formula being provable given a set of hypotheses.

We say that and are equivalent if and , and the proposition is then that there are only finitely many equivalence classes in .

Unfortunately, a full solution using no other machinery (at least the one that I came up with) is a bit too notationally cumbersome for a blog entry, but the puzzle is by no means inaccessible to someone with no other knowledge of logic.

In any case, I will sketch the solution in an important special case: that of formulas which are *left-associated*, i.e., of the form where each is a propositional variable. Since we know how to parenthesize such formulas, we can write them simply in the form .

The crucial insight is the following:

Let be a propositional variable for . Let and suppose that . Then the formulas and are equivalent.

To see why this is so, imagine that you are trying to prove some and you have some hypothesis . What does allow you to do?

- If , it allows you to complete the proof immediately.
- If is of the form , then it allows you to change the goal from to .
- If is of the form , then it allows you to change the goal from to and give yourself as a hypothesis.

In the third case above, suppose that is of the form . The only way that can be of use is if you have some way to change the goal from to . In general, if you have as a hypothesis, if you get to use you must have a method for turning the goal from to for . By assumption in the boxed statement, we therefore have a method for turning the goal from to and vice versa. So and are equivalent. (Actually, what this argument shows is that they can be used in equivalent ways as hypotheses in a proof, which turns out to be enough.)

Now also observe that

For any formula and variable , is equivalent to .

From the two boxed facts, it pretty easily follows that every left-associated formula is equivalent to one of length at most (where is the number of propositional variables): Suppose that is equivalent to no shorter formula. Chopping up into triplets, I claim that no two triplets are the same: If so, and a triplet consisted of all the same variable, we could apply the second boxed fact to get a shorter formula. Otherwise, we can apply the first. Since there are only distinct triplets, that gives a length of at most .

Therefore, there are at most left-associated formulas.

The relevant section of his thesis is Chapter 3 which is also Page 14 (or 23 of the pdf file).