 -->Alonzo Church--> proved the undecidability of classical first-order logic relying on  Gödel’s incompleteness theorem. Dana Scott proved that if \(A\) is a  nonempty proper subset of \(\lambda\)-terms that is closed under equality  then \(A\) is not recursive. The analogous claim for CL, that follows from  the existence of a Gödelian sentence for CL, is that it is  undecidable if two CL-terms are equal.