Undecidability of beta equivalence
= Undecidability of beta equivalence
<Beta equivalence> is <semidecidable>: enumerate finite conversion proofs. It is not decidable. A proposed total numeral-valued classifier of two nonempty disjoint <beta equivalence> classes can be reversed by a <Church Boolean> selector; a <self-quoting fixed point> of this reversal then belongs to the opposite class from the classifier output.