Do combinatory logic bases need a function of 3 variables? All the known bases of combinatory logic, such as $\{S,K\}$, or $\{K,W,B,C\}$,
have one or more combinators using 3 variables:
\begin{align*}
S ={} & \lambda x\lambda y\lambda z. x z(y z), \\
B ={} & \lambda x\lambda y\lambda z. x  (y z), \\
C ={} & \lambda x\lambda y\lambda z. x   z y.
\end{align*}
This raises the question whether we can make a basis with functions of only 2 variables. Surely if such a thing were possible, it would be a most interesting result and it would be well-known.
But as far as I can tell, no such thing is known. Thus it seems nobody believes such a thing to be possible.
But has this been proven anywhere?
How do we know that $\{K,W,2,O,T,D\}$ is not a basis, where
\begin{align*}
K ={} & \lambda x\lambda y. x, \\
W ={} & \lambda x\lambda y. x y y, \\
2 ={} & \lambda f\lambda x. f(f x), \\
O ={} & \lambda x\lambda y. y(x y), \\
T ={} & \lambda x\lambda y. y x, \\
D ={} & \lambda x. x x?
\end{align*}
 A: A Basis Result in Combinatory Logic, Remi Legrand, J. Symb. Logic 53.4 (1988), pp. 1224-1226.

The aim of this article is to show that a basis for combinatory logic must contain at least one combinator with rank strictly greater than two.

A: @PeterTaylor’s excellent answer points to exactly the result wanted.  But the proof there can be streamlined a bit, and may be paywalled for some readers, so I’ll write it out here for accessibility.
Theorem. Let $\newcommand{\B}{\mathbf{B}}\B$ be any set of combinators of rank ≤2.  Then there is no $\B$-expression $T$ such that $\newcommand{\reddto}{\twoheadrightarrow}Tabc \reddto cab$.
Proof.  Fix such $\B$ throughout.  The idea is (unsurprisingly) to find an invariant of $Tabc$ that is sufficiently closed under reduction, and not satisfied by $cab$.  Say that an expression is bad if it is of the form $E[F[a,b],c]$, where $E$ and $F$ are each $\B$-expressions of 2 variables.  Then we have:
Lemma. Any bad expression is either normal, or else has a reduction chain to another bad expression, including at least one leftmost reduction.
Proof of lemma. If a bad expression $E[F[a,b],c]$ is not stuck, consider its leftmost redex.  There are three possible cases:

*

*The head combinator of the redex is not in an occurrence of $F$.  Then each occurrence of $F$ is either outside the redex, or inside an argument of the head combinator; so the reduct is of the form $E'[F[a,b],c]$.


*The whole redex is inside an occurrence of $F$.  Then by reducing it in every occurrence of $F$, we have $E[F[a,b],c] \reddto E[F'[a,b],c]$, and this includes the leftmost redex.


*The head combinator $H$ is iside an occurrence of $F$, but not the whole redex.  Then $H$ must be of rank ≥1.  If $H$ is of rank 1, then $F$ is just $H$, so $x,y$ don’t occur, and the whole expression (both before and after reduction) is of the form $E'[c]$, so is still bad.  If the head combinator is of rank 2, then we must have $F[a,b] \equiv HF'[a,b]$, so by re-parsing as $E[F[a,b],c] \equiv E'[F'[a,b],c]$, case 1 applies.
This proves the lemma. It follows that any bad expression either reduces to a bad normal form, or has an infinite quasi-leftmost reduction sequence.  So by the quasi-leftmost-reduction theorem (Hindley–Seldin 2008, Thm 3.22), any normal form of a bad expression is bad; and so the bad expression $Tabc$ cannot reduce to the normal, non-bad expression $cab$. □
References:

*

*Rémi Legrand, A Basis Result in Combinatory Logic, J. Symb. Logic 1988; jstor full text

*J. Roger Hindley, Jonathan P. Seldin, Lambda-Calculus and Combinators, an Introduction, CUP 2008

