The ω-rule in the λ-calculus (or, more exactly, the λK-β, η calculus) isIn [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 byA term M is closed iff FV(M) = ∅.
Syntactic identity, Parallelism and accommodated antecedents
