When you hear “Craig’s Theorem”, you probably think of the Craig Interpolation Theorem, and rightly so. This is the most famous theorem (I suppose) of philosopher and logician William Craig. So I was surprised to find out there is another “Craig’s Theorem” that is even cooler for those of us interested in lambda calculus. It is well known that every lambda term can be simulated using a combinator term written using combinators S and K. Have you ever wondered if there is a way to simulate all lambda terms using just a single proper combinator Q (proper here means that the combinator is defined by a reduction rule showing how to reduce to some term built from applications of the variables )? Craig’s (other) Theorem says no. There is a very short (2 pages) proof given here (sorry, this is behind a paywall, I think). I can give a simple variation of this proof here.
Suppose there were such a combinator Q. Since it is, by assumption, combinatorily complete, there must be some way to write the identity combinator I using just Q. Consider the reduction sequence , where is the last step in this reduction sequence (which must be of length at least one since is not the same as ). Since reduces, it must be of the form for some combinators . But this tells us that must be projecting one of the inputs to the final result (and one of those must be ). So is a projection combinator. This part is from the linked paper by Bellot. Here is now an alternative conclusion. If a sequence of reductions consists solely of projections of inputs, then that sequence must be terminating, because at each step, the size of the term is decreased by doing a projection. But the lambda calculus includes nonterminating terms, so a projection function cannot be a sufficient basis for the lambda calculus. Hence there is no one-combinator basis for the lambda calculus (and we need at least two, such as S and K).