A Problem on Easy Terms in λ -Calculus

Abstract

We say that a closed term M is easy in the $\mathit{\lambda }\mathit{\beta }\mathit{\eta }$ -calculus if for every term N the theory $\mathit{\lambda }\mathit{\beta }\mathit{\eta }+\{\mathit{M}=\mathit{N}\}$ is consistent. The main result of the paper is to show that, for a certain term P, the term P( $\mathit{\omega }\mathit{\omega }$ ) is easy, while $\mathit{P}\mathit{\omega }$ is not. It follows that the easiness of a given M does not imply either easiness or non-easiness of PM, contradicting an earlier conjecture.