Dear Peter and John, Peter correctly pointed out the error in my message: the problem was in the use of the "if then .. else .." syntax, not in any form of combinatorial completeness. Answering John: I was using a construction of \lambda x.t where \lambda x.M is KM whenever M is any term not containing x free (this works just as well); so in my construction, \lambda vz. if v then xkzk(ykz) else false DOES contain subterms xk and yk. Anyway, I do now believe that John's latest version is correct. This is really very nice, and a surprise (for me, at least). I stand corrected and must apologize for my first posting in this discussion, casting doubt on PTJ's message. One little point, regarding Combinatorial Completeness. I believe the following form is valid (in the situation with the weak S-axiom): suppose t is a term, x a variable. There is a term \lambda x.t such that for all a,a_1,...,a_n in A: ((\lambda x.t)[a_1,...,a_n])a ~ t[a,a_1,...,a_n] So this is just like the ordinary form, except for the assertion that (\lambda x.t)[a_1,...,a_n] is always defined. We have that (\lambda x.t)[a_1,...,a_n] is defined whenever for some a in A, t[a,a_1,...,a_n] is defined. Best, Jaap