Church’s theorem and the decision problem
Rohit Parikh · 2018
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 P and showed that P was representable in first-order logic. If first-order logic were decidable, P would also be decidable. Since 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.