How to Banish Variables from Logic Forever

Why Variables Can Be Tricky—Even in a Simple Sentence

Imagine you read a sentence: “Everybody reads him and Russell.” Who is “him”? It could be anyone—the sentence leaves it open. Now tweak it: “Everybody reads himself and Russell.” Suddenly the meaning snaps into place: each person reads themselves and reads Russell. In logic, this tiny change comes from whether a variable like y is free or bound.

Logicians use quantifiers—“for all” (∀) and “there exists” (∃)—together with variables like x and y. A variable inside the scope of a quantifier is bound; outside, it is free. “All birds are animals” becomes ∀x (Bx ⊃ Ax), with x bound. When you substitute a name—say, “Tweety”—for x, you get Bt ⊃ At, and the meaning stays on track.

But substitution can go wrong. Consider the open formula ∀x (Rx y ∧ Rx r), where y is free. If you blindly replace that y with x, you get ∀x (Rx x ∧ Rx r), a closed formula that says something entirely different. The free variable got captured by the quantifier, like a loose thread pulled into a knot.

Moses Schönfinkel (1889–1942), a Russian logician, saw that this problem is just the beginning. In complex formulas, quantifiers nest and variables interweave in messy patterns. He asked a bold question: what if we could get rid of variables completely?

Schönfinkel’s Bold Plan: Squeeze Logic to One Symbol, Then Squeeze Out the Variables

In ordinary propositional logic you can reduce all truth‑functional connectives to just one: the Sheffer stroke “|” (nand). Schönfinkel wanted to do the same for first‑order logic. He invented a binary operator called nextand (written |^x) that combines the work of ∃, ¬, and ∧. Using only this operator, every first‑order formula can be rewritten equivalently—even the universal quantifier ∀x A becomes definable.

But the real magic came next: eliminating the bound variables. Schönfinkel introduced new constants called combinators—S and K—that act like tiny functions to rearrange, duplicate, and delete arguments. He also defined a special constant U for “disjointness” (there is no x that satisfies both predicates). By cleverly applying S, K, and U, any formula turns into a term with no variables at all.

Here is a taste. The sentence “For every natural number there is a greater prime” can be formalized as ∀y∃x(Ny ⊃ (Px ∧ Gx y)). After a series of transformations, Schönfinkel would turn it into an expression built from U, S, K, and the predicates N, P, G—no variables in sight. The variable‑free term might read UN(B(UP)(CG) ) (though the real one is a bit longer). It looks alien, but it captures exactly the same meaning.

The trick works because combinators let you curry functions: instead of a function that takes several arguments at once, you break it into a chain of one‑argument functions. That way you never need to name a variable—the function’s own behavior does the work. Schönfinkel had shown that logic could be done without variables, forever.

Meet the Combinators: Tiny Machines That Do the Work of Variables

Imagine two little robots, S and K. They live in a world where everything is a function, and you combine them by application—writing MN means “apply M to N.” The robots follow simple rules:

• K takes two arguments and returns the first one, ignoring the second. It’s a stubborn creature that always picks the first thing it sees.
• S takes three arguments. It applies the first to the third, and the second to the third, then applies the first result to the second. It copies and combines like a tiny weaving machine.

With just S and K you can build any other combinator. The identity combinator I, which returns its argument unchanged, is SKK. You can make a combinator B that composes functions, a combinator C that swaps arguments, and a combinator W that duplicates (W x y → x y y). Schönfinkel proved that S and K are combinatorially complete: any function that can be described using variables can be built from these two alone.

One especially mind‑bending combinator is Y, the fixed‑point combinator. For any function f, Y f gives a fixed point: f (Y f) = Y f. So Y enables self‑reference and recursion—functions that call themselves. This power makes combinatory logic capable of expressing all computable functions. But it also introduces infinite loops: the term WWW reduces to itself forever, never reaching a simple outcome.

Thus combinators are not just a curiosity; they form a full‑blown programming language with zero variables.

When Combinators Crash: Normal Forms, Loops, and the Church‑Rosser Theorem

Now that we have terms built from S and K, we can compute by applying the reduction rules step by step—this is called reduction. For example, K x y reduces to x, and S f g x reduces to f x ( g x ). A redex is a subterm that matches one of these patterns; you can contract it to simplify.

Sometimes you can reduce a term until no redexes remain—that is a normal form. But not all terms have one. WWW loops endlessly. Yet some terms with infinite reduction sequences still have a normal form: Y (K I) can reduce forever, but it also reduces to I if you choose the right path.

This leads to a crucial result: the Church‑Rosser theorem. It says that no matter what order you reduce, if you keep going you will eventually reach the same result—provided any result exists at all. Think of it like a maze where every path leads to the same treasure chest, even though some paths wander in circles. The theorem guarantees that the logic is consistent: you will never end up with two different normal forms for the same starting term.

The theorem also shows that combinatory logic is not a free‑for‑all; it behaves like a clean computational system. The hunt for normal forms and the study of which terms terminate (strongly normalize) are central to the theory of computation. Combinators give us a playground where we can test what it means for a program to actually finish running.

From Schönfinkel’s Blackboard to Your Favorite App: Why Combinators Still Matter

Schönfinkel’s ideas did not stay in a dusty journal. They sparked a revolution. Alonzo Church (1903–1995) developed the lambda calculus, a close relative that uses a variable‑binding operator λ, but he also explored combinators. Haskell Curry (1900–1982) built on Schönfinkel’s work, giving us “currying” and the Curry‑Howard correspondence that bridges logic and computation.

Today, combinatory logic and the lambda calculus are the theoretical backbone of functional programming languages such as Haskell and ML. When you write a function that calls another function, you are using currying. Recursive definitions often rely on fixed‑point combinators. Even the way compilers simplify expressions draws on reduction and normal forms.

There is also a surprising limit: it is impossible to write a program that can decide, for any two combinatory terms, whether they are equal. This undecidability result, foreshadowed by Gödel’s incompleteness theorems, means there is no all‑powerful debugger that can always tell if two programs do the same thing. So Schönfinkel’s quest did not just tidy up logic—it laid bare deep truths about what computers can and cannot do.

The next time you run an app or write a line of code, remember that hidden inside may be a combinatory descendant, working quietly without a single variable.

Think about it

1. If you could build any function using only two simple robots (S and K), what would that say about the world being made of a tiny set of rules? Could all of nature be built from just a handful of building blocks?
2. Imagine a program that never stops—it loops forever. Would you say it is doing something meaningful, or is it just broken? Does a function that never gives an answer still count as a function?
3. Variables feel natural: we name things. If a computer can work without naming anything, does that change what it means to “know” or “understand”? Can you think of a skill you learned without naming each step?