Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 76 / 5 / iv

There is an argument-order defect in the printed flip context: the discriminator constructed above takes its numeral first. Fix $U\in \mathcal{U},V\in \mathcal{V}$ and useEquivalently, define $E=\lambda uvn.Dnuv$ and write the context as $\lambda x.EUV(Gx)$. This is an explicit permutation of the discriminator arguments, not an assumption that $DUV(Gx)$ has the required behavior.

Let $Q{\equiv }_{\beta }Fd(Q)$ be the self-quoting fixed point. There are exactly two cases. If $Gd(Q){\equiv }_{\beta }{c}_0$, then $Q{\equiv }_{\beta }U$, so closure under beta equivalence puts $Q$ in $\mathcal{U}$ and forces $Gd(Q){\equiv }_{\beta }{c}_1$. If $Gd(Q){\equiv }_{\beta }{c}_1$, then $Q{\equiv }_{\beta }V\in \mathcal{V}$, forcing $Gd(Q){\equiv }_{\beta }{c}_0$. Both contradict the distinct beta-normal Church numerals $c_0,c_1$. Hence no such total binary lambda classifier exists.

If beta equivalence were decidable, its decision algorithm would give a total computable function that outputs one exactly on codes of terms beta-equivalent to $I$, and zero on all other codes. Its numeral representation would be such a $G$, taking $\mathcal{U}$ to be the class of $I$ and $\mathcal{V}$ its complement. Both are nonempty: $K$ has a different beta-normal form from $I$. The contradiction proves beta equality is undecidable. It is nevertheless semidecidable, since finite conversion proofs can be effectively enumerated.