Hostname: page-component-7c8c6479df-fqc5m Total loading time: 0 Render date: 2024-03-28T08:15:10.221Z Has data issue: false hasContentIssue false

A new proof for Craig's theorem

Published online by Cambridge University Press:  12 March 2014

P. Bellot*
Affiliation:
Institut De Programmation, Université P. Et M. Curie, 75005 Paris, France

Extract

Craig's theorem is a result about the cardinality of a proper basis for the theory of combinators. Its proof given in [3] was shown to be incomplete by André Chauvin [2]. By using a different approach, we give a very short proof of this theorem. We use the notation of [1].

Definition 1. A combinator Q is proper if there exists a natural number n such that for arbitrary variables x1,…,xn we have the following contraction rule:

where C is a pure combination of the variables x1,…,xn. Q is to be understood as an abstract symbol, not as a combination of S and K's. Therefore Q comes with a contraction rule.

Definition 2. A set (Q1,…, Qm} of combinators is a basis for combinatory logic if for every finite set {x1,…, xk} of variables and every pure combination C of these variables, there exists a pure combination Q of Q1,…, Qm such that Qx1xkC.

Craig's Theorem. Every basis for combinatory logic containing only proper combinators contains at least two elements.

Proof. Let {Q} be a singleton basis for combinatory logic, and let us show that we cannot have combinatory completeness. This is an easy consequence of the next two lemmas.

Lemma 1. Q is a projection. That is, Qx1xnxj, for some j.

Proof. Let I be a proper combination of Q such that Ixx for a variable x, and let M be a term such that IxMx and Mx is a nontrivial contraction.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1985

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Barendregt, H., The lambda calculus: Its syntax and semantics, North-Holland, Amsterdam, 1981.Google Scholar
[2]Chauvin, A., Handwritten notes, Université de Metz, Île de Saulcy, 57000 Metz, France.Google Scholar
[3]Curry, H. B. and Feys, R. (with two sections by W. Craig), Combinatory Logic. Vol. I, North-Holland, Amsterdam, 1958.Google Scholar