What is the precise statement of Craig's theorem?

Question

I'm interested writing a proof of Craig's theorem. After several attempts I realized that there are several possible ways to state the theorem, each with subtle but important differences.

Here's one statement I came up with:

"If a system of combinatory logic has only one type of combinator x and x is proper, there exists some proper combinator y that cannot be defined in the system."

This version of the theorem has the most restrictive premises, and is correspondingly easy to prove.

Here's another:

"There is no proper combinator x such that, for any proper combinator y, there exists some C that is a combination of x and is functionally equivalent to y."

The main difference from above is that this formalization allows combinators other than the universal combinator in the system, as long as they are given as parameters or obtained through substitutions. In this form the proof becomes surprisingly difficult.

And then there's the issue of valid terms in the system. In both of above examples I have tacitly assumed that the only terms of the system are combinators, but I've seen cases where combinators are treated as polymorphic functions that take parameters of arbitrary types. When generalized to this level, I'm not sure how to state the theorem to begin with.

Which of the above (if any) is the generally accepted statement of Craig's theorem? Is there a better way to state it that makes the theorem easier to work with?

Answer 1

In Bellot's A New Proof for Craig's Theorem, he presents the theorem as:

Every basis for combinatory logic containing only proper combinators contains at least two elements.

He defines a basis as:

A set ${Q_1,\dots,Q_m}$ of combinators is a $basis$ for combinatory logic if for every finite set ${x_1,\dots,x_k}$ of variables and every pure combination C of these variables, there exists a pure combination $Q$ of $Q_1,\ldots,Q_m$ such that $Qx_1\cdots x_k\twoheadrightarrow C$.

This seems to be equivalent to your first contruction, though I confess I'm not totally sure I understand the difference between the two. (If $x$ and $y$ are proper combinators, and C is strictly composed of applications of $x$, I don't see where the other combinators could be relevant).