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 .)