Church's theorem

Theorem due to the American mathematician and philosopher Alonzo Church (1903-95) stating that the theorems of the predicate calculus do not form a general recursive set. Given Church's thesis, this means that there is no decision procedure or algorithm for deciding whether an arbitrary formula of the first-order predicate calculus is a theorem of the calculus.