# Intuitively speaking, why was there a need to “eliminate” quantified variables in mathematical logic?

I'm trying to wrap my head around the understanding of lambda-calculus, from a math/computing/logic standpoint and am reading more about its very genesis. This has taken me to 1924 - Schonfinkel's introduction of combinatory logic that seems to have started it all. On Wikipedia it says:

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry...

I understand the need for quantified variables like $\forall$ and $\exists$ in mathematical logic and it seems useful. But I fail to understand the reason to eliminate them. Why was this important? What does one attain with this elimination? Does it become more expressive? How so?

First, I'm not sure I agree that combinatory logic primarily aims to eliminate variables bound by $\forall$ and $\exists$. The basic formulation of combinatory logic works at the propositional level, where there are no quantifiers to eliminate in the first place. Instead, what it eliminates is $\lambda$-bound variables, but in a terms-as-proofs setting through the Curry-Howard isomorphism. We the have the correspondence

$$\frac{\text{combinatory logic}}{\lambda\text{-calculus}} : \frac{\text{Hilbert-style formal proofs}}{\text{natural deduction}}$$

There's a natural correspondence between terms in the simply-typed $\lambda$-calculus and proofs in natural deduction for intuitionistic propositional logic. Through this correspondend, the combinators in combinatory logic correspond to the basic axioms of a Hilbert-style system.

There are various ways to extend this correspondence to predicate logic (and these may well have come first, historically), but they are not nearly as well-known or commonly encountered as the propositional setting. So you should probably not think of it as primarily having to do with $\forall$ and/or $\exists$ -- at least if you're trying to gain a contemporary understanding of how things fit together.

Now, what is this good for? As a practical way of writing down proofs it is a disaster -- it is well known that terms in the $\lambda$-calculus can increase in size exponentially when one tries to express them in combinatory logic.

However, there are some theoretical benefits -- because there are no variables, there is no need to define a notion of substitution either, and we don't need to worry about capturing variables during substitution and develop a machinery for avoiding this. This can often simplify proofs about the system.

• Given my understanding of $\lambda$ calculus is still rudimentary and I'm struggling with associating it with logic and computing, could you please "dum down" your explanation for the non-mathematically inclined? I'm not sure I understood the answer well enough. – PhD Feb 11 '15 at 22:18
• Comment 1: on the history: Curry undoubtedly was interested in illative combinatory logic encyclopediaofmath.org/index.php/Illative_combinatory_logic which aims to capture the logical quantifiers as primitives. – Rob Arthan Feb 12 '15 at 22:46
• Comment 2: on the practicalities of combinatory logic: combinators are not disastrous (unless you tie your hands behind your back and only allow $S$ and $K$). The theory of combinators is very important for implementors and users of functional programming languages. E.g., see dl.acm.org/citation.cfm?id=802129 for a seminal reference on the use of combinators in compilers. – Rob Arthan Feb 12 '15 at 22:55
• @RobArthan: I must admit I never read the supercombinator stuff back when I had a way through the paywall (and I even did some joint work with the author :p) but isn't that under an assumption where you can design which combinators to use based on the program you want to compile? – Henning Makholm Feb 12 '15 at 23:06
• @Henning Makholm: you can still compile functional programs quite efficiently with a fixed repertoire of combinators. See David Turner's seminal reference on bracket abstraction jstor.org/discover/10.2307/… – Rob Arthan Feb 12 '15 at 23:14