Church proved that there is no computable function which decides for two given λ-calculus expressions whether they are equivalent or not.
Church a demonstrat că nu există nicio funcție calculabilă⁠(d) care decide, pentru două λ-expresii date, dacă acestea sunt echivalente sau nu.