Some results on extensionality in lambda calculus (Q1765154)

A counterexample of Plotkin showed that the \(\lambda\)-theory with the \((\omega)\) rule: \[ \text{If }MQ=NQ\text{ for all closed terms }Q\text{ then }M=N, \] is not recursively enumerable. It is also well known that \(\lambda \beta \eta\), which is recursively enumerable, does not satisfy \((\omega)\). This paper answers a question of Cantini by showing that there is a recursively enumerable \(\lambda\)-theory which satisfies \((\omega)\). The work leads to a better understanding of Plotkin's counterexample.