Combinatory logic interactive proof system ​

Background & motivation ​

Recently, I’ve been diving into To Mock a Mockingbird by Raymond Smullyan, a playful yet rigorous puzzle book that introduces combinatory logic^[1] through different scenarios involving birds in a forest. The book challenges readers to solve increasingly complex logical problems, blending humor with abstract mathematical concepts.

While working through the puzzles, I found myself repeatedly writing out similar lines of equations on paper, making small changes by substituting terms and expanding definitions as I progressed. This manual process of iterative steps is characteristic of math exercises done in high school and college coursework, such as solving equations or factorizing polynomials.
This is an example from my notebook:

Although this step-by-step process helps us recognize patterns and is necessary to solve the problem, I wondered if there might be a less tedious way to work through such deductions.

An “automated” system? ​

Many theorems of combinatory logic can be proven automatically using existing theorem provers. Similarly, automated tools can solve any system of linear equations through linear algebra and instantly factorize polynomials.

The thing is, I didn’t want to fully automate the process, as I still wanted to solve the puzzles myself. Instead, I wanted a tool that would help me go through my process, only handling the tedious aspects —such as variable substitution— rather than solving the problem for me.

So, I went through and decomposed the proofs I had made into atomic steps which can be combined to form the proof. While choosing these steps requires thought, executing them is a mechanical process.

For the following sections, some basic knowledge of first-order logic is required, particularly understanding the meaning of universal ($\forall$) and existential ($\exists$) quantifiers.

Steps & transformations ​

For example, consider this axiom that states that something holds for every $x$:

$$(\forall x)\; M\,x = x\,x$$

Then, this must hold for any arbitrary value —or bird^[2]— we substitute for $x$, let’s say $(A\,B)$. So, we can perform the following transformation:

$$\begin{align*} (\forall x&)\; M\,x = x\,x \\ \big\darr&\scriptsize\; x \coloneqq (A\,B) \\ M\,(&A\,B) = (A\,B)\,(A\,B) \end{align*}$$

This step is tedious and mechanical, making it ideal for automation. We can generalize it and call it a “for-all elimination”.

Here are the basic types of steps/transformations I first identified^[3]:

• For-all elimination: $(\forall x)\;\textsf{\textbf{P}}(x) \longrightarrow \textsf{\textbf{P}}(\textsf{\textbf{x}})$.
• For-all introduction: arbitrary $A$, $\textsf{\textbf{P}}(A) \longrightarrow (\forall x)\;\textsf{\textbf{P}}(x)$.
• Exists elimination: $(\exists x)\;\textsf{\textbf{P}}(x) \longrightarrow$ let $A$ such that $\textsf{\textbf{P}}(A)$.
• Exists introduction: $P(\textsf{\textbf{x}}) \longrightarrow (\exists x)\;\textsf{\textbf{P}}(x)$.
• Rewriting: given $\textsf{\textbf{x}} = \textsf{\textbf{y}}$, then $\textsf{\textbf{x}} \rightarrow \textsf{\textbf{y}}$ and $\textsf{\textbf{y}} \rightarrow \textsf{\textbf{x}}$.
• Bound variable renaming: $(\forall x)\;\textsf{\textbf{P}}(x) \longrightarrow (\forall y)\;\textsf{\textbf{P}}(y)$; $(\exists x)\;\textsf{\textbf{P}}(x) \longrightarrow (\exists y)\;\textsf{\textbf{P}}(y)$.

The system ​

I then implemented an interactive system that can be used to carry out proofs. Here are some examples of the possible interactions.

For-all elimination ​

To eliminate a universal quantifier (that is, to apply it to a particular expression), you have to drop the expression over the binder. While you make this interaction, all occurrences of the variable are highlighted. When the quantifier is applied, a new theorem is created, referencing the proposition it depends upon:

If the expression we wish to use as an argument is not already present, it can be manually built using an expression editor:

Rewriting ​

To rewrite a term using an equation, you can drag and drop the equation member over the expression it matches with. The target expression is unified with the dropped equality member and then replaced by the other side of the equality.

Here’s an example combining a “for-all elimination” with two rewritings (one left-to-right, and the other right-to-left):

Exists introduction ​

If a condition holds for a value, then there exists a value for which that condition holds. So, to introduce an existential quantifier, you have to drop a free variable at the start of the expression:

For-all introduction ​

Both for-all introduction and exists elimination require the concept of a “context” in which new variables are considered. In the case of the former, we first consider a new arbitrary combinator —ahem, bird—, and prove things about it. The resulting theorem will be valid for any bird, since we proved it for an arbitrary one without making any assumptions about it.

We begin by considering a new arbitrary bird, which becomes available in our context. We can use it to prove “sub-theorems”, until we reach a final expression. Then, we finish the proof, and a new universal quantifier will be added to the proven expression if it references the arbitrary bird:

Bound variable renaming ​

The bound variable of any quantifier can be renamed by double-clicking on its binding occurrence, and all its occurrences will be automatically updated. For instance, following the last example, we can rename $A$ to $x$:

If the new variable name would cause an unwanted variable capture, the inner conflicting variable is also automatically renamed by changing its subscript:

Exists elimination ​

When eliminating an existential quantifier, we introduce a new variable in the context such that the body of the existential holds. This is done by dropping an unused variable onto the binder:

Expression naming ​

Sometimes we need to introduce a new variable to name an expression. This is especially useful when preparing to introduce an existential quantifier for a complex expression.

To name an expression, we have to select it and click on “Name expression”. The resulting equality can then be used for rewriting other expressions.

Conclusions & future work ​

We’ve developed an interactive system for dynamically manipulating logical expressions to make deductions. The system can already be used to solve some puzzles from the book; for example, this is a proof of the first one^[4]:

The system was developed in TypeScript using Test-Driven Development for the prover model. You can find the code on GitHub and try the system here.

For me, one of the most interesting aspects of this project was creating a tool that helps users in their own journey exploring combinatory logic puzzles, instead of solving the problem for them by automatically generating solutions. I think this exemplifies a broader philosophy in tool design: creating systems that augment —rather than attempting to replace— human capabilities, where the right balance of challenge and support can provide meaningful assistance while respecting the autonomy of the user.

Future work includes implementing additional domain features:

• Conditionals ($\implies$).
• Conjunction ($\land$).
• Disjunction ($\lor$).
• Negation ($\neg$).

But also (and maybe more importantly) “interaction” features to allow for a better iterative use of the tool:

• Undo/redo functionality.
• Removing proof steps or theorems.
• Support for building parallel theorems/proofs.

If you’re interested in exploring combinatory logic or contributing to the project, visit the GitHub repository or try out the interactive system, feedback is welcomed!