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.



Church’s theorem and the decision problem

DOI: 10.4324/9780415249126-Y003-1
Version: v1,  Published online: 1998
Retrieved June 21, 2024, from

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 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.

Citing this article:
Parikh, Rohit. Church’s theorem and the decision problem, 1998, doi:10.4324/9780415249126-Y003-1. Routledge Encyclopedia of Philosophy, Taylor and Francis,
Copyright © 1998-2024 Routledge.

Related Searches


Related Articles