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

Question

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?

Answer 1

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.