The λ-calculus is ω-incomplete
Gordon D. Plotkin · Journal of Symbolic Logic · 1974
The ω-rule in the λ-calculus (or, more exactly, the λK-β, η calculus) is In [1] it was shown that this rule is consistent with the other rules of the λ-calculus. We will show the rule cannot be derived from the other rules; that is, we will give closed terms M and N such that MZ = NZ can be proved without using the ω-rule, for each closed term Z, but M = N cannot be so proved. This strengthens a result in [4] and answers a question of Barendregt. The language of the λ-calculus has an alphabet containing denumerably many variables a, b, c, … (which have a standard listing e1, e2, …), improper symbolsλ, ( , ) and a single predicate symbol = for equality. Terms are defined inductively by the following: (1) A variable is a term. (2) If M and N are terms, so is (MN); it is called a combination. (3) If M is a term and x is a variable, (λx M) is a term; it is called an abstraction. We use ≡ for syntactic identity of terms. If M and N are terms, M = N is a formula. BV(M), the set of bound variables in M, and FV(M), its free variables, are defined inductively by A term M is closed iff FV(M) = ∅.