= Solution
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 use
$$
F=\lambda x.D(Gx)UV.
$$
Equivalently, define $E=\lambda u v n.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 \b[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 \b[beta equality is undecidable]. It is nevertheless <semidecidable>, since finite conversion proofs can be effectively enumerated.
Back to article page
