Scott–Curry theorem

Proof

The proof is adapted from Barendregt in The Lambda Calculus.

Let A and B be closed under beta-convertibility and let a and b be lambda term representations of elements from A and B respectively. Suppose for a contradiction that f is a lambda term representing a computable function such that ${\displaystyle fx=0}$ if ${\displaystyle x\in A}$ and ${\displaystyle fx=1}$ if ${\displaystyle x\in B}$ (where equality is β-equality). Then define ${\displaystyle G\equiv \lambda x.\text{if}(\text{zero?}(fx))ab}$. Here, ${\displaystyle \text{zero?}}$ is true if its argument is zero and false otherwise, and ${\displaystyle \text{if}}$ is the identity so that ${\displaystyle \text{if}bxy}$ is equal to x if b is true and y if b is false.

Then ${\displaystyle x\in C⟹Gx=a}$ and similarly, ${\displaystyle x\notin C⟹Gx=b}$. By the Second Recursion Theorem, there is a term X which is equal to f applied to the Church numeral of its Gödel numbering, X'. Then ${\displaystyle X\in C}$ implies that ${\displaystyle X=G(X^{\prime })=b}$ so in fact ${\displaystyle X\notin C}$. The reverse assumption ${\displaystyle X\notin C}$ gives ${\displaystyle X=G(X^{\prime })=a}$ so ${\displaystyle X\in C}$. Either way we arise at a contradiction, and so f cannot be a function which separates A and B. Hence A and B are recursively inseparable.

History

Dana Scott first proved the theorem in 1963. The theorem, in a slightly less general form, was independently proven by Haskell Curry. It was published in Curry's 1969 paper "The undecidability of λK-conversion".