Here's a class related post that comes out of an explanation I got recently. It is also a bit rough, so be gentle. You can simulate lambda-abstraction in combinatory logic. You want to do this to get some of the lambda-abstraction flexibility without leaving a first-order (with types) framework. Lambda calculus is not first-order because terms (lambdas) can bind variables, which you can't do in FOL. How are lambdas different than quantifiers? One's a term and the other isn't, maybe? I'm not completely clear on that. But, the combinators are first order. The simulated abstraction doesn't work in all cases. It can't with the resources of just combinatory logic. One case it fails is (\lambda x.t)[s/z]=\lambda x(t[s/z]) (From Jeremy Avigad). Why might one want to do simulate the abstraction at all? There is a result that shows there is an isomorphism between proofs and programs, and so types (and categories, apparently). This means that one can think of a proof as a program, which is definable via the lambda calculus. This in turn means that one can think of proofs as terms (formulas? I think terms) in the lambda calculus. What sort of proof though? The terms are natural deduction proofs, with the abstracted terms viewed as undischarged hypotheses. Application is discharging a hypothesis. So, one gets that lambda calculus is the type theoretic analog of natural deduction. What are combinators then? Combinators are the type theoretic analog of axiomatic proofs. The route to seeing this is by looking at the types that make up the combinators. K is p->(q->p) and S is (p->q->r)->((p->q)->(p->r)). These types are structurally the same as the first two axoims of propositional logic (as usually presented; they'll be in there somewhere). The punchline: combinators are the type theoretic analog of axiomatic proofs, and they are just as hard to use. Now, the question is: what is the type theoretic analog of the sequent calculus?