Written by mkoconnor

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<j<k 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.

2 thoughts on “An Interesting Puzzle in Propositional Logic”

  2. I thought that two formulas are equivalent when they have the same values in the truth table? Why isn’t this true?

    Reply

Leave a comment