(en.wikipedia.org) Scott–Curry theorem - Wikipedia

ROAM_REFS: https://en.wikipedia.org/wiki/Scott–Curry_theorem

In mathematical logic, the Scott–Curry theorem is a result in lambda calculus stating that if two non-empty sets of lambda terms A and B are closed under beta-convertibility then they are recursively inseparable.

** Explanation

A set A of lambda terms is closed under beta-convertibility if for any lambda terms X and Y, if \(X \in A\) and X is β-equivalent to Y then \(Y \in A\). Two sets A and B of natural numbers are recursively separable if there exists a computable function \(f:\mathbb{N}\rightarrow\{ 0,1\}\) such that \(f(a) = 0\) if \(a \in A\) and \(f(b) = 1\) if \(b \in B\). Two sets of lambda terms are recursively separable if their corresponding sets under a Gödel numbering are recursively separable, and recursively inseparable otherwise.

The Scott–Curry theorem applies equally to sets of terms in combinatory logic with weak equality. It has parallels to Rice's theorem in computability theorem, which states that all non-trivial semantic properties of programs are undecidable.

The theorem has the immediate consequence that it is an undecidable problem to determine if two lambda terms are β-equivalent.