Version: v1, Published online: 1998
Retrieved May 20, 2019, from https://www.rep.routledge.com/articles/thematic/churchs-theorem-and-the-decision-problem/v-1
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 and showed that was representable in first-order logic. If first-order logic were decidable, would also be decidable. Since 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.
Parikh, Rohit. Church’s theorem and the decision problem, 1998, doi:10.4324/9780415249126-Y003-1. Routledge Encyclopedia of Philosophy, Taylor and Francis, https://www.rep.routledge.com/articles/thematic/churchs-theorem-and-the-decision-problem/v-1.
Copyright © 1998-2019 Routledge.