An Interesting Puzzle in Propositional Logic

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

The first professor you come across, $\hbox{Prof. Bal}$, knows what $\mathit{bal}$ means, the second professor you come across, $\hbox{Prof. Kat}$, knows what $\mathit{kat}$ means, and the third professor you come across, $\hbox{Prof. Lot}$, knows what $\mathit{lot}$ 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 $\hbox{Prof. }(\mathrm{Bal}\rightarrow\mathrm{Kat})$.  He doesn’t know what $\mathit{bal}$ means or what $\mathit{kat}$ means, but if you told him what $\mathit{bal}$ meant, he would be able to tell you what $\mathit{kat}$ means (for example, maybe he knows that $\mathit{kat}$ is the noun form of $\mathit{bal}$).

The next professor you meet is named $\hbox{Prof. }(\mathrm{Bal}\rightarrow(\mathrm{Kat}\rightarrow\mathrm{Lot}))$.  If you told him what $\mathit{bal}$ meant and what $\mathit{kat}$ meant, he would be able to tell you what $\mathit{lot}$ means.

The next professor you meet is named $\hbox{Prof. }((\mathrm{Bal}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Lot})$.  If you told him a method for finding out the meaning of $\mathit{kat}$ given the meaning of $\mathit{bal}$, he would be able to tell you the meaning of $\mathit{lot}$.

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

Notice that some professors have essentially the same state of knowledge.  For example, $\hbox{Prof. Bal}$ and $\hbox{Prof. }((\mathrm{Kat}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Bal})$ have essentially the same knowledge, since to get the meaning of $\mathit{bal}$ out of $\hbox{Prof. }((\mathrm{Kat}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Bal})$ you only have to tell him a method for finding out the meaning of $\mathit{kat}$ given the meaning of $\mathit{kat}$, which is something that you can do without any particular special knowledge concerning $\mathit{bal}$, $\mathit{kat}$ and $\mathit{lot}$.

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

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 $\mathbb{C}_n$ be the free cartesian closed category over $n$ objects.  Given objects $A$ and $B\in \mathbb{C}_n$, say that $A$ and $B$ are equivalent if there is an arrow from $A$ to $B$ and an arrow from $B$ to $A$.  Then there are only finitely many equivalence classes in $\mathbb{C}_3$.  (The corresponding statements are also true with $3$ replaced by $n$.)

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 $V$ be a finite set of propositional variables, and let $F$ be the smallest set containing $V$ and such that if formulas $\phi$ and $\psi$ are in $F$, then the formula $\phi\rightarrow\psi$ is in $F$.  We define a relation $\vdash$ between sets of formulas in $F$ and formulas in $F$ as follows:  We will let $\vdash$ be the smallest relation such that, for any $\Gamma\subset F$, $\phi,\psi\in F$:

1. $\Gamma\cup\{\phi\}\vdash\phi$.
2. If $\Gamma'\supset \Gamma$ and $\Gamma\vdash \phi$, then $\Gamma'\vdash \phi$.
3. If $\Gamma\vdash \phi\rightarrow\psi$ and $\Gamma\vdash\phi$, then $\Gamma\vdash \psi$.
4. If $\Gamma\cup\{\phi\}\vdash \psi$, then $\Gamma\vdash \phi\rightarrow\psi$.

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

We say that $\phi$ and $\psi$ are equivalent if $\{\phi\}\vdash\psi$ and $\{\psi\}\vdash\phi$, and the proposition is then that there are only finitely many equivalence classes in $F$.

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 $(\cdots(((A_1\rightarrow A_2)\rightarrow A_3)\rightarrow A_4)\cdots\rightarrow A_n)$ where each $A_i$ is a propositional variable.  Since we know how to parenthesize such formulas, we can write them simply in the form $A_1A_2A_3A_4\cdots A_n$.

The crucial insight is the following:

Let $A_i$ be a propositional variable for $1\leq i\leq n$.  Let $i and suppose that $A_i=A_k$.  Then the formulas $A_iA_1A_2\cdots A_n$ and $A_jA_1A_2\cdots A_n$ are equivalent.

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

• If $P=A_i$, it allows you to complete the proof immediately.
• If $P$ is of the form $A_j\rightarrow A_i$, then it allows you to change the goal from $A_i$ to $A_j$.
• If $P$ is of the form $(Q\rightarrow A_j)\rightarrow A_i$, then it allows you to change the goal from $A_i$ to $A_j$ and give yourself $Q$ as a hypothesis.

In the third case above, suppose that $Q$ is of the form $(R\rightarrow A_k)$.  The only way that $Q$ can be of use is if you have some way to change the goal from $A_j$ to $A_k$.  In general, if you have $BA_1\cdots A_n$ as a hypothesis, if you get to use $B$ you must have a method for turning the goal from $A_{i+1}$ to $A_i$ for $1\leq i\leq n-1$.  By assumption in the boxed statement, we therefore have a method for turning the goal from $A_i$ to $A_j$ and vice versa. So $A_iA_1\cdots A_n$ and $A_jA_1\ldots A_n$ 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 $P$ and variable $A_i$, $(((P\rightarrow A_i)\rightarrow A_i)\rightarrow A_i)$ is equivalent to $P\rightarrow A_i$.

From the two boxed facts, it pretty easily follows that every left-associated formula $\phi$ is equivalent to one of length at most $3n^3 +2$ (where $n$ is the number of propositional variables):  Suppose that $\phi$ is equivalent to no shorter formula.  Chopping $\phi$ up into $\lfloor |\phi|/3\rfloor$ 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 $n^3$ distinct triplets, that gives a length of at most $3n^3 + 2$.

Therefore, there are at most $n^{3n^3+2}$ left-associated formulas.

One thought on “An Interesting Puzzle in Propositional Logic”

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