Church’s theorem and the decision problem

Church’s theorem, published in 1936, states that the set of valid formulas of first-order logic is not effectively decidable: there is no method or algorithm for deciding which formulas of first-order logic are valid. Church’s paper exhibited an undecidable combinatorial problem $\mathcal{P}$ and showed that $\mathcal{P}$ was representable in first-order logic. If first-order logic were decidable, $\mathcal{P}$ would also be decidable. Since $\mathcal{P}$ is undecidable, first-order logic must also be undecidable.

Church’s theorem is a negative solution to the decision problem (Entscheidungsproblem), the problem of finding a method for deciding whether a given formula of first-order logic is valid, or satisfiable, or neither. The great contribution of Church (and, independently, Turing) was not merely to prove that there is no method but also to propose a mathematical definition of the notion of ‘effectively solvable problem’, that is, a problem solvable by means of a method or algorithm.