Loading [MathJax]/jax/output/HTML-CSS/jax.js
Skip to main content
Library homepage
 

Text Color

Text Size

 

Margin Size

 

Font Type

Enable Dyslexic Font
Humanities LibreTexts

3.2: Undecidability

( \newcommand{\kernel}{\mathrm{null}\,}\)

  • 3.2.1: Introduction
    It is one thing to not be able to imagine how one would compute complicated functions, and quite another to actually prove that they are uncomputable.
  • 3.2.2: Enumerating Turing Machines
    We can show that the set of all Turing machines is countable. This follows from the fact that each Turing machine can be finitely described.
  • 3.2.3: The Halting Problem
    The halting problem is one example of a larger class of problems of the form “can X be accomplished using Turing machines.” (The answer is no: the halting problem is unsolvable.)
  • 3.2.4: The Decision Problem
    We say that first-order logic is decidable iff there is an effective method for determining whether or not a given sentence is valid. As it turns out, there is no such method: the problem of deciding validity of first-order sentences is unsolvable.
  • 3.2.5: Representing Turing Machines
    In order to represent Turing machines and their behavior by a sentence of first-order logic, we have to define a suitable language. The language consists of two parts: predicate symbols for describing configurations of the machine, and expressions for numbering execution steps (“moments”) and positions on the tape.
  • 3.2.6: Verifying the Representation
    In order to verify that our representation works, we have to prove two things. First, we have to show that if M halts on input w, then T(M,w)E(M,w) is valid. Then, we have to show the converse, i.e., that if T(M,w)E(M,w) is valid, then M does in fact eventually halt when run on input w.
  • 3.2.7: The Decision Problem is Unsolvable
    If the decision problem were solvable, we could use it to solve the halting problem.
  • 3.2.8: Summary


This page titled 3.2: Undecidability is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .

  • Was this article helpful?

Support Center

How can we help?