Combinatory logic interactive proof system

✒️ DescriptionAn interactive system for manipulating logical expressions and making deductions in combinatory logic. Features direct manipulation of expressions through drag-and-drop interactions.
▶️ Try It OutLive Demo
⚡ TechnologiesTypeScript, HTML, CSS
🗂️ Source CodeGitHub Repository

Background & motivation

Cover of the book 'To Mock a Mockingbird', by Raymond Smullyan. The cover reads 'to mock a Mockingbird and other logic puzzles' and has, among other things, a picture of a bird
Book cover of "To Mock a Mockingbird"

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: A sheet of paper with some annotations, that illustrates a step-by-step process of iteratively modifying equations. Each line builds on the previous with small changes, reflecting the incremental reasoning. For example: C x = A(B x); C x = A(M x); C x = A(x x); C C = A(C C)

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 xx:

(x)  Mx=xx(\forall x)\; M\,x = x\,x

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

(x)  Mx=xxx(AB)M(AB)=(AB)(AB)\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: (x)  P(x)P(x)(\forall x)\;\textsf{\textbf{P}}(x) \longrightarrow \textsf{\textbf{P}}(\textsf{\textbf{x}}).
  • For-all introduction: arbitrary AA, P(A)(x)  P(x)\textsf{\textbf{P}}(A) \longrightarrow (\forall x)\;\textsf{\textbf{P}}(x).
  • Exists elimination: (x)  P(x)(\exists x)\;\textsf{\textbf{P}}(x) \longrightarrow let AA such that P(A)\textsf{\textbf{P}}(A).
  • Exists introduction: P(x)(x)  P(x)P(\textsf{\textbf{x}}) \longrightarrow (\exists x)\;\textsf{\textbf{P}}(x).
  • Rewriting: given x=y\textsf{\textbf{x}} = \textsf{\textbf{y}}, then xy\textsf{\textbf{x}} \rightarrow \textsf{\textbf{y}} and yx\textsf{\textbf{y}} \rightarrow \textsf{\textbf{x}}.
  • Bound variable renaming: (x)  P(x)(y)  P(y)(\forall x)\;\textsf{\textbf{P}}(x) \longrightarrow (\forall y)\;\textsf{\textbf{P}}(y); (x)  P(x)(y)  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: Animation showing a line labeled A1: "(∀x) M x = x x". The user drags "M" onto "(∀x)", all "x"s are highlighted. When the "M" is dropped, a new line appears below, labeled T1: "M M = M M ... A1".

If the expression we wish to use as an argument is not already present, it can be manually built using an expression editor: Animation starting with the same line as before: "A1. (∀x) M x = x x". The user opens a "Create new expression" pane, drags a template "(hole hole)" to the canvas, fills both holes with "M", then drags the resulting "(M M)" onto the "(∀x)" in A1 and a new line appears below: "T1. M (M M) = (M M) (M M)".

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): Animation starting with A1: "I x = x" and A2: "(∀x) M x = x x". Applying A2 to I yields T1: "M I = I I". Next, the user drags the "I x" side of the equality from A1 onto "I I" in T1, so the system rewrites it using A1’s rule (I x = x) to produce T2: "M I = I". Finally, dragging the "x" side of the equation from A1 onto "M I" in T2 generates T3: "I (M I) = I".

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: Animation starting with the expression "(∀x) M x = x x". Grabbing "M" makes a "(∃M)" indicator appear next to "(∀x)". When dropping "M" over the indicator, the system generates a new theorem T1: "(∃M) (∀x) M x = x x".

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: Animation starting with axioms A1 and A2. The user clicks "New variable", inputs "A", and a header appears: "Let A be an arbitrary bird". Applying A2 to A generates an indented sub-theorem T1.1: "M A = A A". The user continues by making other previously described steps, generating more intermediate steps until the last line is "M A = M (I A)". Finally, after clicking "Finish proof", the system collapses the intermediate steps and adds a new theorem T1: "(∀A) M A = M (I A)".

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 AA to xx: Animation showing double-clicking the "(∀A)" in theorem T1 "(∀A) M A = M (I A)", prompting a variable rename. The user inputs "x", updating T1 in place to "(∀x) M x = M (I x)".

If the new variable name would cause an unwanted variable capture, the inner conflicting variable is also automatically renamed by changing its subscript: Animation showing double-clicking the "(∀A)" in theorem T1 "(∀A) M A = M (I A)", prompting a variable rename. The user inputs "x", updating T1 in place to "(∀x) M x = M (I x)".

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: Animation showing the theorem "(∃C) (∀x) C x = A (M x)". Dragging "C", an unused variable in the context, onto "(∃C)" adds a new line: "Let C such that (∀x) C x = A (M x)"

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.

Animation showing selecting "C C" in the equation "C C = A (C C)", then clicking on "Name expression" and inputting "X". The system creates the equation "X = C C", which is then used by the user to rewrite the original equation as "X = A (C C)".

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]:

Screenshot of the proof system showing axioms A1: (∀A)(∀B)(∃C)(∀x) C x = A (B x) (composition rule) and A2: (M x = x x), with derived theorem T1: (∀A)(∃X) X = A X. Sub-steps demonstrate for-all and exists eliminations, rewriting, and expression naming.

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!


  1. Combinatory logic is a formal system that lets us express any computable function in terms of combinators — special higher-order functions that contain no free variables.

    For example, a function MM defined as M(x)=x(x)M(x)=x(x) is a combinator, since xx is both its parameter and the only variable in its definition.

    In combinatory logic, putting one combinator after another denotes function application, so F(x)F(x) would be written as F  xF\;x. Similarly, the function MM described above would be written as M  x=x  xM\;x = x\;x. ↩︎

  2. Following the metaphor presented in the book, where every value is a combinator, and combinators are called birds. Also in this example, MM would be the mockingbird. ↩︎

  3. The different typefaces have different meanings: xx denotes a variable named “x”, while x\textsf{\textbf{x}} represents a meta-variable that could stand for any variable or expression, such as xx, yy, or more complex terms. The variable AA is used as a placeholder for any variable (excluding other expression types).

    For the structure of the rules (the pairs introduction/elimination), I was inspired by the paper “An intuitionistic theory of types”, by Per Martin-Löf (p. 12, pdf). He was, in turn, based on Gerhard Gentzen. Just as a reference, here are the symbolic rules introduced by Gentzen in 1934, taken from here:

    -Intro.-Elim.FaxFxxFxFa-Intro.-Elim.FaxFx[Fa]xFxCC\boxed{ \begin{array}{c c} \forall\text{-Intro.} & \forall\text{-Elim.} \\[.5em] \displaystyle\frac{\mathfrak{F}a}{\forall x\,\mathfrak{F}x} & \displaystyle\frac{\forall x\,\mathfrak{F}x}{\mathfrak{F}a} \\[3em] \exists\text{-Intro.} & \exists\text{-Elim.} \\[.5em] \displaystyle\frac{\mathfrak{F}a}{\exists x\,\mathfrak{F}x} & \displaystyle\frac{\begin{array}{cc} &[\mathfrak{F}a] \\ \exists x\,\mathfrak{F}x &\mathfrak{C} \end{array}}{\mathfrak{C}} \end{array} }

    ↩︎
  4. The puzzle is called “The Significance of the Mockingbird”. It asks us to prove (or deny) that every bird of the forest is fond of at least one bird; i.e. (A)(B)A  B=B(\forall A)(\exists B)\,A\;B = B. ↩︎