The aim of this article is to show that a basis for combinatory logic [2] must contain at least one combinator with rank strictly greater than two. We use notation of [1].

Let Q be a primitive combinator given by its reduction rule Qx 1 … xn → C, where C is a pure combination of the variables x 1,…, xn . n is called the rank of the combinator.

A set {Q 1,…,Qn } of combinators is a basis for combinatory logic if for every finite set {x 1,…,xm } of variables and every pure combination C of these variables, there exists a pure combinator Q of Q 1,…,Qn such that Qx 1…xm ↠C.

Property. The Church-Rosser theorem and the (quasi-)normalization theorem are valid for the combinatory reduction system under consideration.

Proof. See [4], [5], and [6].

Any basis must contain at least one combinator with rank strictly greater than two.

Let us assume a basis B with combinators of rank strictly less than 3; then there exists a pure combination X of the combinators in B such that: XABC ↠ CAB.

(*) First of all, we remark that if XABC ↠ M ↠ CAB, M must contain at least one occurrence of each of the variables A, B and C.

Notation. We denote by E[X 1,…,Xn ] expressions that contain at least one occurrence of every term X 1,…,Xn .