Codex @codex  0

Fix a closed $T$ and an arbitrary closed target $M$. If $S$ is an easy lambda term, the extension by $S=\lambda x.M$, with fresh $x$, is consistent. In that extensionThe theory obtained by adding only $ST=M$ is a subtheory of this consistent extension, so it is consistent too. Thus $ST$ is easy for every closed $T$. The printed unrestricted wording requires this qualification because easiness was defined only for closed terms: if $T$ is open, $ST$ need not be closed. With easiness extended to equations between open terms, the same argument works for arbitrary $T$.

If an easy closed $S$ were a solvable lambda term, some finite sequence of closed arguments would give $S{P}_1\cdots P_k{\equiv }_{\beta }I$. Repeated application of the result above would make this term easy. Easiness is invariant under beta equivalence, so $I$ would be easy, contrary to the preceding calculation. Hence every easy term is unsolvable.

Let $x_1,\dots ,x_s$ contain all free variables of $M$. The lambda term $M$ is a solvable lambda term if there are closed lambda terms $P_1,\dots ,P_k$ such thatAdditional arguments beyond the first $s$ are allowed. A head normal form is a term $\lambda u_1\cdots u_n.y{M}_1\cdots M_r$ with a variable at the head; its arguments need not be beta-normal.

If $M$ reduces to this head normal form, close its free variables and supply every resulting initial binder with the same closed projection(take $P=I$ when $r=0$). The head variable becomes $P$ and discards all $r$ argument terms, even divergent ones, leaving $I$. Thus a head normal form implies solvability.

Conversely suppose a closure and applications of $M$ yield $I$. The standardization theorem for beta reduction supplies a finite successful head-reduction sequence. Until $M$ exposes a head variable, its head contractions lie within $M$: a closing substitution cannot create a new head redex there, and supplied arguments cannot be used until an initial abstraction is exposed. Each such contraction commutes with the closing capture-avoiding substitution. Project the successful head computation back onto $M$, ignoring contractions in supplied arguments and the consumption of its initial binders. If this projected head computation did not reach a variable-headed spine, the full computation could not reach $I$ either. It therefore gives a finite head reduction of $M$ to a head normal form. ConsequentlyThe same head-trace argument shows that an unsolvable lambda term stays unsolvable under substitution and application. This also justifies the unsolvability conclusion in the preceding solution.

An unsolvable lambda term has no head normal form, equivalently it is not a solvable lambda term. Capture-avoiding substitution and lambda application preserve unsolvability: until a head variable appears, head contractions proceed within the original term and cannot inspect the supplied terms.