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