Math 2.0

Mathematical logic and foundations First-order logic Theorem

Church's theorem on undecidability of first-order logic

Builds on Predicate logicSentenceComputable setTuring machineUndecidability of the halting problemGödel's completeness theorem

Statement

There is a finite signature LL with the following property. The set of valid first-order sentences of LL, that is, of the LL-sentences true in every LL-structure, is not a computable set. Equivalently, no algorithm decides, for an arbitrary LL-sentence, whether it is valid in first-order logic.

Remarks

Church proved the result in 1936 with the lambda calculus, and Turing proved it independently with Turing machines. In Turing's approach, one builds from each Turing machine MM a sentence φM\varphi_M that is valid exactly when MM halts on the empty input. A decision procedure for validity would then solve the halting problem, which is impossible.

The theorem gives a negative answer to Hilbert's Entscheidungsproblem. It holds for every signature that contains a binary relation symbol. It fails for signatures with only unary relation symbols: monadic first-order logic is decidable.

By Gödel's completeness theorem, the valid sentences are exactly the provable ones, so they form a computably enumerable set. So validity is semi-decidable but not decidable.

Going deeper

For a student

Church's theorem is the first-order counterpart of the undecidability of the halting problem. It is the reason why automated theorem provers can only search for proofs, and may run forever. Decidable fragments, such as monadic logic, and decidable theories, such as Presburger arithmetic, are therefore valuable in computer science.

Reading path

To understand this page from the ground up, read these 19 pages in order. The foundations come first.

Show the path as a graph
Computable set, concept, no evidence levelComputable setconceptGödel numbering, concept, no evidence levelGödel numberingconceptHilbert system, concept, no evidence levelHilbert systemconceptLogical consequence, concept, no evidence levelLogical consequenceconceptModel, concept, no evidence levelModelconceptProposition, concept, no evidence levelPropositionconceptSentence, concept, no evidence levelSentenceconceptTuring machine, concept, no evidence levelTuring machineconceptUndecidability of the halting problem, statement, no evidence levelUndecidability of the…statementGödel's completeness theorem, statement, no evidence levelGödel's completeness …statementConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionPropositional logic, concept, no evidence levelPropositional logicconceptPredicate logic, concept, no evidence levelPredicate logicconceptChurch's theorem on undecidability of first-order logic, statement, no evidence levelChurch's theorem on u…statement
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Computable set concept
  2. Gödel numbering concept
  3. Hilbert system concept
  4. Logical consequence concept
  5. Model concept
  6. Proposition concept
  7. Sentence concept
  8. Turing machine concept
  9. Undecidability of the halting problem statement
  10. Gödel's completeness theorem statement
  11. Conjunction definition
  12. Disjunction definition
  13. Implication definition
  14. Negation definition
  15. Predicate definition
  16. Biconditional definition
  17. Propositional logic concept
  18. Predicate logic concept
  19. Church's theorem on undecidability of first-order logic statement

Further reading

  1. Web https://en.wikipedia.org/wiki/Entscheidungsproblem
About this page
TagVA6BNNY2YC
URIm2://VA6BNNY2YC
Kindstatement, theorem
WritingW0 stub
MSC03B25, 03D35, 03B10
StatusThis copy of the site has no build data. Run m2 status VA6BNNY2YC.
AboutPredicate logic
UsesPredicate logic, Sentence, Computable set, Turing machine, Undecidability of the halting problem, Gödel's completeness theorem
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.