Access to the full content is only available to members of institutions that have purchased access. If you belong to such an institution, please log in or find out more about how to order.

### Contents

• content locked

# Church’s theorem and the decision problem

DOI
10.4324/9780415249126-Y003-1
DOI: 10.4324/9780415249126-Y003-1
Version: v1,  Published online: 1998
Retrieved July 16, 2019, from https://www.rep.routledge.com/articles/thematic/churchs-theorem-and-the-decision-problem/v-1

## Article Summary

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.