Turing machines

Undecidability

content/turing-machines/undecidability/undecidability.tex

% Part: turing-machines% Chapter: undecidability\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{tur}{und}{Undecidability}\olimport{introduction}\olimport{enumerating-tms}\olimport{universal-tm}\olimport{halting-problem}\olimport{decision-problem}\olimport{representing-tms}\olimport{verification}\olimport{unsolvability-decision-problem}\olimport{trakhtenbrot}\OLEndChapterHook\end{document}

content/turing-machines/undecidability/introduction.tex

% Part: turing-machines % Chapter: undecidability% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{int} \olsection{Introduction}It might seem obvious that not every function, even every arithmeticalfunction, can be computable. There are just too many, whose behavioris too complicated.  Functions defined from the decay of radioactiveparticles, for instance, or other chaotic or random behavior. Supposewe start counting 1-second intervals from a given time, and define thefunction $f(n)$ as the number of particles in the universe that decayin the $n$-th 1-second interval after that initial moment.  This seemslike a candidate for a function we cannot ever hope to compute.But it is one thing to not be able to imagine how one would computesuch functions, and quite another to actually prove that they areuncomputable.  In fact, even functions that seem hopelesslycomplicated may, in an abstract sense, be computable.  For instance,suppose the universe is finite in time---some day, in the very distantfuture the universe will contract into a single point, as somecosmological theories predict. Then there is only a finite (butincredibly large) number of seconds from that initial moment for which$f(n)$ is defined.  And any function which is defined for only finitelymany inputs is computable: we could list the outputs in one big table,or code it in one very big Turing machine state transition diagram.We are often interested in special cases of functions whose values givethe answers to yes/no questions.  For instance, the question ``is $n$a prime number?'' is associated with the function\[\fn{isprime}(n) = \begin{cases}  1 & \text{if $n$ is prime}\\  0 & \text{otherwise.}  \end{cases}\]We say that a yes/no question can be \emph{effectively decided}, ifthe associated $1/0$-valued function is effectively computable.To prove mathematically that there are functions which cannot beeffectively computed, or problems that cannot effectively decided, itis essential to fix a specific model of computation, and showthat there are functions it cannot compute or problems it cannotdecide.  We can show, for instance, that not every function can becomputed by Turing machines, and not every problem can be decided byTuring machines.  We can then appeal to the Church--Turing thesis toconclude that not only are Turing machines not powerful enough tocompute every function, but no effective procedure can.The key to proving such negative results is the fact that we canassign numbers to Turing machines themselves.  The easiest way to dothis is to enumerate them, perhaps by fixing a specific way to writedown Turing machines and their programs, and then listing them in asystematic fashion.  Once we see that this can be done, then theexistence of Turing-uncomputable functions follows by simplecardinality considerations: the set of functions from $\Nat$ to~$\Nat$ (infact, even just from $\Nat$ to $\{0, 1\}$) are !!{nonenumerable}, butsince we can enumerate all the Turing machines, the set of Turing-computablefunctions is only !!{denumerable}.We can also define \emph{specific} functions and problems which we canprove to be uncomputable and undecidable, respectively.  One suchproblem is the so-called \emph{Halting Problem.} Turing machines canbe finitely described by listing their instructions.  Such adescription of a Turing machine, i.e., a Turing machine program, canof course be used as input to another Turing machine.  So we canconsider Turing machines that decide questions about other Turingmachines.  One particularly interesting question is this: ``Does thegiven Turing machine eventually halt when started on input~$n$?''  Itwould be nice if there were a Turing machine that could decide thisquestion: think of it as a quality-control Turing machine whichensures that Turing machines don't get caught in infinite loops andsuch.  The interesting fact, which Turing proved, is that there cannotbe such a Turing machine. There cannot be a single Turing machinewhich, when started on input consisting of a description of a Turingmachine $M$ and some number~$n$, will always halt with either output$1$ or $0$ according to whether $M$ machine would have halted whenstarted on input $n$ or not.Once we have examples of specific undecidable problems we can use themto show that other problems are undecidable, too.  For instance, onecelebrated undecidable problem is the question, ``Is the first-order!!{formula}~$!A$ valid?''.  There is no Turing machine which, given asinput a first-order !!{formula}~$!A$, is guaranteed to halt withoutput $1$ or $0$ according to whether $!A$ is valid or not.Historically, the question of finding a procedure to effectively solvethis problem was called simply ``the'' decision problem; and so we saythat the decision problem is unsolvable.  Turing and Church proved thisresult independently at around the same time, so it is also called theChurch--Turing Theorem.\end{document}

content/turing-machines/undecidability/enumerating-tms.tex

% Part: turing-machines% Chapter: undecidability% Section: enumerating-tms\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{enu}\olsection{Enumerating Turing Machines}\begin{explain}We can show that the set of all Turing machines is !!{enumerable}.This follows from the fact that each Turing machine can be finitelydescribed.  The set of states and the tape vocabulary are finite sets.The transition function is a partial function from $Q \times \Sigma$to $Q \times \Sigma \times \{\TMleft, \TMright, \TMstay\}$, and solikewise can be specified by listing its values for the finitely manyargument pairs for which it is defined.This is true as far as it goes, but there is a subtle difference. Thedefinition of Turing machines made no restriction on what !!{element}sthe set of states and tape alphabet can have. So, e.g., for every realnumber, there technically is a Turing machine that uses that number asa state. However, the \emph{behavior} of the Turing machine isindependent of which objects serve as states and vocabulary. Considerthe two Turing machines in \olref{fig:variants}.\begin{figure}\begin{center}\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,                    semithick]  \tikzstyle{every state}=[fill=none,draw=black,text=black]  \node[initial,state]         (A)              {$q_0$};  \node[state]         (B) [right of=A] {$q_1$};  \path (A) edge [bend left] node {\TMtrans{\TMstroke}{\TMstroke}{\TMright}} (B)        (B) edge [loop above] node {\TMtrans{\TMblank}{\TMblank}{\TMright}} (B)            edge [bend left] node {\TMtrans{\TMstroke}{\TMstroke}{\TMright}} (A);\end{tikzpicture}\\\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,  semithick]\tikzstyle{every state}=[fill=none,draw=black,text=black]\node[initial,state]         (A)              {$s$};\node[state]         (B) [right of=A] {$h$};\path (A) edge [bend left] node {\TMtrans{A}{A}{\TMright}} (B)(B) edge [loop above] node {\TMtrans{\TMblank}{\TMblank}{\TMright}} (B)edge [bend left] node {\TMtrans{A}{A}{\TMright}} (A);\end{tikzpicture}\end{center}\caption{Variants of the \emph{Even} machine}\ollabel{fig:variants}\end{figure}These two diagrams correspond to two machines, $M$ with the tapealphabet $\Sigma = \{\TMendtape,\TMblank,\TMstroke\}$ and set ofstates $\{q_0,q_1\}$, and $M'$ with alphabet $\Sigma' =\{\TMendtape,\TMblank,A\}$ and states $\{s,h\}$. But theirinstructions are otherwise the same: $M$ will halt on a sequence of$n$ $\TMstroke$'s iff $n$ is even, and $M'$ will halt on a sequence of$n$ $A$'s iff $n$ is even. All we've done is rename $\TMstroke$to~$A$, $q_0$ to~$s$, and $q_1$ to~$h$. This example generalizes: wecan think of Turing machines as the same as long as one results fromthe other by such a renaming of symbols and states.  In fact, we cansimply think of the symbols and states of a Turing machine as positiveintegers: instead of $\sigma_0$ think~$1$, instead of $\sigma_1$think~$2$, etc.; $\TMendtape$ is~$1$, $\TMblank$ is~$2$, etc. In thisway, the \emph{Even} machine becomes the machine depicted in\olref{fig:standard-even}.\begin{figure}\[\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,  semithick]\tikzstyle{every state}=[fill=none,draw=black,text=black]\node[initial,state]         (A)              {$1$};\node[state]         (B) [right of=A] {$2$};\path (A) edge [bend left] node {\TMtrans{3}{3}{\TMright}} (B)(B) edge [loop above] node {\TMtrans{2}{2}{\TMright}} (B)edge [bend left] node {\TMtrans{3}{3}{\TMright}} (A);\end{tikzpicture}\]\caption{A standard \emph{Even} machine}\ollabel{fig:standard-even}\end{figure}We might call a Turing machine with states and symbols that arepositive integers a \emph{standard} machine, and only considerstandard machines from now on.\footnote{The terminology ``standardmachine'' is not standard.}We wanted to show that the set of Turing machines is !!{enumerable},and with the above considerations in mind, it is enough to show thatthe set of standard Turing machines is !!{enumerable}. Suppose we aregiven a standard Turing machine $M = \tuple{Q, \Sigma, q_0, \delta}$.How could we describe it using a finite string of positive integers?We'll first list the number of states, the states themselves, thenumber of symbols, the symbols themselves, and the starting state.(Remember, all of these are positive integers, since $M$ is a standardmachine.)  What about~$\delta$? The set of possible arguments, i.e.,pairs $\tuple{q,\sigma}$, is finite, since $Q$ and~$\Sigma$ arefinite. So the information in~$\delta$ is simply the finite list ofall $5$-tuples $\tuple{q, \sigma, q', \sigma', d}$ where$\delta(q,\sigma) = \tuple{q', \sigma', D}$, and $d$ is a number thatcodes the direction~$D$ (say, $1$ for~$\TMleft$, $2$ for~$\TMright$,and $3$ for~$\TMstay$).In this way, every standard Turing machine can be described by afinite list of positive integers, i.e., as a sequence $s_M \in(\PosInt)^*$. For instance, the standard \emph{Even} machine is codedby the sequence\[2, \underbrace{1, 2}_Q, 3, \overbrace{1, 2, 3}^\Sigma, 1, \underbrace{1, 3, 2, 3, 2}_{\delta(1,3) = \tuple{2,3,R}}, \overbrace{2, 2, 2, 2, 2}^{\delta(2,2) = \tuple{2,2,R}},\underbrace{2, 3, 1, 3, 2}_{\delta(2,3) = \tuple{1,3,R}}.\]\end{explain}\begin{thm}There are functions from $\Nat$ to~$\Nat$ which are not Turingcomputable.\end{thm}\begin{proof}We know that the set of finite sequences of positiveintegers~$(\PosInt)^*$ is !!{enumerable}(\cref{sfr:siz:zigzag:prob:posint-star}). This gives us that the setof descriptions of standard Turing machines, as a subsetof~$(\PosInt)^*$, is itself enumerable.  Every Turing computablefunction $\Nat$ to~$\Nat$ is computed by some (in fact, many) Turingmachines. By renaming its states and symbols to positive integers (inparticular, $\TMendtape$ as~$1$, $\TMblank$ as~$2$, and $\TMstroke$as~$3$) we can see that every Turing computable function is computedby a standard Turing machine. This means that the set of all Turingcomputable functions from $\Nat$ to~$\Nat$ is also enumerable.On the other hand, the set of all functions from $\Nat$ to~$\Nat$ isnot !!{enumerable} (\cref{sfr:siz:red:prob:nat-nat}). If all functionswere computable by some Turing machine, we could enumerate the set ofall functions by listing all the descriptions of Turing machines thatcompute them. So there are some functions that are not Turingcomputable. \end{proof}\begin{prob}  Can you think of a way to describe Turing machines that does not  require that the states and alphabet symbols are explicitly listed?  You may define your own notion of ``standard'' machine, but say  something about why every Turing machine can be computed by a  ``standard'' machine in your new sense.\end{prob}\end{document}

content/turing-machines/undecidability/universal-tm.tex

% Part: turing-machines% Chapter: undecidability% Section: universal-tm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{uni}\olsection{Universal Turing Machines}In \olref[enu]{sec} we discussed how every Turing machine can bedescribed by a finite sequence of integers. This sequence encodes thestates, alphabet, start state, and instructions of the Turing machine.We also pointed out that the set of all of these descriptions is!!{enumerable}. Since the set of such descriptions is !!{denumerable},this means that there is !!a{surjective} function from~$\Nat$ tothese descriptions. Such !!a{surjective} function can be obtained, forinstance, using Cantor's zig-zag method.  It gives us a way ofenumerating all (descriptions) of Turing machines. If we fix one suchenumeration, it now makes sense to talk of the $1$st, $2$nd, \dots,$e$th Turing machine.  These numbers are called \emph{indices}.\begin{defn}If $M$~is the $e$th Turing machine (in our fixed enumeration), wesay that $e$~is an \emph{index} of~$M$. We write $M_e$ for the $e$thTuring machine.\end{defn}A machine may have more than one index, e.g., two descriptions of~$M$may differ in the order in which we list its instructions, and thesedifferent descriptions will have different indices.Importantly, it is possible to give the enumeration of Turing machinedescriptions in such a way that we can effectively compute thedescription of~$M$ from its index, and to effectively compute an indexof a machine~$M$ from its description.  By the Church--Turing thesis,it is then possible to find a Turing machine which recovers thedescription of the Turing machine with index~$e$ and writes thecorresponding description on its tape as output. The description wouldbe a sequence of blocks of~$\TMstroke$'s (representing the positiveintegers in the sequence describing~$M_e$).Given this, it now becomes natural to ask: what functions of Turingmachine indices are themselves computable by Turing machines? Whatproperties of Turing machine indices can be decided by Turingmachines?  An example: the function that maps an index~$e$ to thenumber of states the Turing machine with index~$e$ has, is computableby a Turing machine. Here's what such a Turing machine would do:started on a tape containing a single block of $e$~$\TMstroke$'s, itwould first decode $e$ into its description. The description is nowrepresented by a sequence of blocks of~$\TMstroke$'s on the tape.Since the first !!{element} in this sequence is the number of states.So all that has to be done now is to erase everything but the firstblock of $\TMstroke$'s and then halt.A remarkable result is the following:\begin{thm}\ollabel{thm:universal-tm} There is a \emph{universal  Turing machine}~$U$ which, when started on input $\tuple{e,n}$   \begin{enumerate}    \item halts iff $M_e$ halts on input~$n$, and    \item if $M_e$ halts with output $m$, so does~$U$.  \end{enumerate}  $U$ thus computes the function $f\colon \Nat \times \Nat \pto \Nat$  given by $f(e,n) = m$ if $M_e$ started on input~$n$ halts with  output~$m$, and undefined otherwise.\end{thm}\begin{proof}  To actually produce~$U$ is basically impossible, since it is an  extremely complicated machine. But we can describe in outline how it  works, and then invoke the Church--Turing thesis.  When it starts,  $U$'s tape contains a block of $e$ $\TMstroke$'s followed by a block  of $n$~$\TMstroke$'s. It first ``decodes'' the index~$e$ to the  right of the input~$n$. This produces a list of numbers (i.e.,  blocks of $\TMstroke$'s separated by~$\TMblank$'s) that describes  the instructions of machine~$M_e$. $U$ then writes the number of the  start state of~$M_e$ and the number~$1$ on the tape to the right of  the description of~$M_e$. (Again, these are represented in unary, as  blocks of $\TMstroke$'s.) Next, it copies the input (block of  $n$~$\TMstroke$'s) to the right---but it replaces each $\TMstroke$  by a block of three $\TMstroke$'s (remember, the number of the $\TMstroke$  symbol is~$3$, $1$ being the number of~$\TMendtape$ and $2$ being  the number of~$\TMblank$). At the left end of this sequence of blocks  (separated by $\TMblank$ symbols on the tape of~$U$), it writes a  single~$\TMstroke$, the code for~$\TMendtape$.  $U$ now has on its tape: the index~$e$, the number~$n$, the code  number of the start state (the ``current state''), the number of the  initial head position~$1$ (the ``current head position''), and the  initial contents of the ``tape'' (a sequence of blocks  of~$\TMstroke$'s representing the code numbers of the symbols  of~$M_e$---the ``symbols''---separated by~$\TMblank$'s).  It now simulates what $M_e$ would do if started on input~$n$, by  doing the following:  \begin{enumerate}    \item Find the number~$k$ of the ``current head position'' (at the    beginning, that's~$1$),    \item Move to the $k$th block in the ``tape'' to see what the    ``symbol'' there is,    \item\ollabel{find-inst}%    Find the instruction matching the current ``state'' and    ``symbol,''    \item Move back to the $k$th block on the ``tape'' and replace the    ``symbol'' there with the code number of the symbol $M_e$ would    write,    \item Move the head to where it records the current ``state'' and    replace the number there with the number of the new state,    \item Move to the place where it records the ``tape position'' and    erase a~$\TMstroke$ or add a~$\TMstroke$ (if the instruction says    to move left or right, respectively).    \item Repeat.\footnote{We're glossing over some subtle    difficulties here. E.g., $U$~may need some extra space when it    increases the counter where it keeps track of the ``current head    position''---in that case it will have to move the entire ``tape''    to the right.}  \end{enumerate}  If $M_e$ started on input~$n$ never halts, then $U$ also never  halts, so its output is undefined.  If in step~\olref{find-inst} it turns out that the description  of~$M_e$ contains no instruction for the current  ``state''/``symbol'' pair, then $M_e$ would halt. If this happens,  $U$ erases the part of its tape to the left of the ``tape.'' For  each block of three~$\TMstroke$'s (representing a~$\TMstroke$ on  $M_e$'s tape), it writes a $\TMstroke$ on the left end of its own  tape, and successively erases the ``tape.'' When this is done,  $U$'s~tape contains a single block of~$\TMstroke$'s of length~$m$.    If $U$ encounters something other than a block of  three~$\TMstroke$'s on the ``tape,'' it immediately halts. Since  $U$'s~tape in this case does not contain a single block  of~$\TMstroke$'s, its output is not a natural number, i.e., $f(e,n)$  is undefined in this case.\end{proof}\end{document}

content/turing-machines/undecidability/halting-problem.tex

% Part: computability% Chapter: machines-computations% Section: halting-problem\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{hal}\olsection{The Halting Problem}\begin{explain}Assume we have fixed some enumeration of Turing machinedescriptions.  Each Turing machine thus receives an \emph{index}: itsplace in the enumeration $M_1$, $M_2$, $M_3$, \dots{} of Turing machinedescriptions.We know that there must be non-Turing-computable functions: the set ofTuring machine descriptions---and hence the set of Turing machines---is!!{enumerable}, but the set of all functions from $\Nat$ to $\Nat$ isnot. But we can find specific examples of non-computable functions aswell. One such function is the halting function.\end{explain}\begin{defn}[Halting function] The \emph{halting function}~$h$ is defined as\[h(e,n) =\begin{cases}  \text{0} & \text{if machine~$M_e$ does not halt for input $n$} \\  \text{1} & \text{if machine~$M_e$ halts for input $n$}\end{cases}\]\end{defn}\begin{defn}[Halting problem]The \emph{Halting Problem} is the problem of determining (for any $e$, $n$)whether the Turing machine~$M_e$ halts for an input of~$n$ strokes.\end{defn}\begin{explain}We show that~$h$ is not Turing-computable by showing that a relatedfunction,~$s$, is not Turing-computable. This proof relies on the factthat anything that can be computed by a Turing machine can be computedby a disciplined Turing machine (\olref[mac][dis]{sec}), and the factthat two Turing machines can be hooked together to create a singlemachine (\olref[mac][cmb]{sec}).\end{explain}\begin{defn} The function~$s$ is defined as\[s(e) =\begin{cases}  \text{0} & \text{if machine~$M_e$ does not halt for input $e$} \\  \text{1} & \text{if machine~$M_e$ halts for input $e$}\end{cases}\]\end{defn}\begin{lem}The function~$s$ is not Turing computable.\end{lem}\begin{proof}We suppose, for contradiction, that the function~$s$ is Turingcomputable.  Then there would be a Turing machine~$S$ thatcomputes~$s$. We may assume, without loss of generality, that when $S$halts, it does so while scanning the first square (i.e., that it isdisciplined).  This machine can be ``hooked up'' to anothermachine~$J$, which halts if it is started on input~$0$ (i.e., if itreads $\TMblank$ in the initial state while scanning the square to theright of the end-of-tape symbol), and otherwise wanders off to theright, never halting. $S \concat J$, the machine created by hooking$S$ to~$J$, is a Turing machine, so it is $M_e$ for some~$e$ (i.e., itappears somewhere in the enumeration). Start $M_e$ on an input of~$e$$\TMstroke$s. There are two possibilities: either $M_e$ halts or itdoes not halt.\begin{enumerate}\item Suppose $M_e$ halts for an input of $e$ $\TMstroke$s. Then $s(e)  = 1$. So $S$, when started on~$e$, halts with a single $\TMstroke$  as output on the tape.  Then $J$ starts with a $\TMstroke$ on the  tape. In that case $J$ does not halt. But $M_e$ is the machine $S  \concat J$, so it should do exactly what $S$ followed by $J$ would  do (i.e., in this case, wander off to the right and never halt).  So  $M_e$ cannot halt for an input of $e$ $\TMstroke$'s.\item Now suppose $M_e$ does not halt for an input of $e$  $\TMstroke$s.  Then $s(e) = 0$, and $S$, when started on input~$e$,  halts with a blank tape.  $J$,~when started on a blank tape,  immediately halts.  Again, $M_e$ does what $S$ followed by~$J$ would  do, so $M_e$ must halt for an input of $e$ $\TMstroke$'s.\end{enumerate}In each case we arrive at a contradiction with our assumption. Thisshows there cannot be a Turing machine~$S$: $s$~is not Turingcomputable.\end{proof}\begin{thm}[Unsolvability of the Halting Problem]\ollabel{thm:halting-problem} The halting problem is unsolvable, i.e.,the function~$h$ is not Turing computable.\end{thm}\begin{proof}Suppose $h$ were Turing computable, say, by a Turing machine~$H$. Wecould use $H$ to build a Turing machine that computes~$s$: First, makea copy of the input (separated by a~$\TMblank$ symbol). Then move backto the beginning, and run~$H$.  We can clearly make a machine thatdoes the former (see \cref{tur:mac:dis:prob:copier}), and if $H$existed, we would be able to ``hook it up'' to such a copier machineto get a new machine which would determine if $M_e$ halts oninput~$e$, i.e., computes~$s$. But we've already shown that no suchmachine can exist. Hence, $h$~is also not Turing computable.\end{proof}\begin{prob}The Three Halting (3-Halt) problem is the problem of giving a decisionprocedure to determine whether or not an arbitrarily chosen TuringMachine halts for an input of three $\TMstroke$'s on an otherwiseblank tape. Prove that the 3-Halt problem is unsolvable.\end{prob}\begin{prob}Show that if the halting problem is solvable for Turing machine andinput pairs $M_e$ and~$n$ where $e \neq n$, then it is also solvablefor the cases where $e = n$.\end{prob}\begin{prob}We proved that the halting problem is unsolvable if the input is anumber~$e$, which identifies a Turing machine~$M_e$ via an enumerationof all Turing machines.  What if we allow the description of Turingmachines from \olref[tur][und][enu]{sec} directly as input?  Can therebe a Turing machine which decides the halting problem but takes asinput descriptions of Turing machines rather than indices?  Explainwhy or why not.\end{prob}\begin{prob} Show that the \emph{partial} function~$s'$ is defined as  \[  s'(e) =  \begin{cases}    \text{1} & \text{if machine~$M_e$ halts for input $e$}\\    \text{undefined} & \text{if machine~$M_e$ does not halt for input $e$}  \end{cases}  \]  \emph{is} Turing computable.\end{prob}\end{document}

content/turing-machines/undecidability/decision-problem.tex

% Part: turing-machines% Chapter: undecidability% Section: unsolvability-decision-problem\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{dec}\olsection{The Decision Problem}We say that first-order logic is \emph{decidable} iff there is aneffective method for determining whether or not a given !!{sentence}is valid. As it turns out, there is no such method: the problem ofdeciding validity of first-order sentences is unsolvable.In order to establish this important negative result, we prove thatthe decision problem cannot be solved by a Turing machine.  That is,we show that there is no Turing machine which, whenever it is startedon a tape that contains a first-order !!{sentence}, eventually haltsand outputs either $1$ or~$0$ depending on whether the!!{sentence} is valid or not. By the Church--Turing thesis, everyfunction which is computable is Turing computable. So if this``validity function'' were effectively computable at all, it would beTuring computable. If it isn't Turing computable, then, it also cannotbe effectively computable.Our strategy for proving that the decision problem is unsolvable is toreduce the halting problem to it.  This means the following: We haveproved that the function~$h(e,w)$ that halts with output~$1$ if theTuring machine described by~$e$ halts on input~$w$ and outputs~$0$otherwise, is not Turing computable.  We will show that if there werea Turing machine that decides validity of first-order sentences, thenthere is also Turing machine that computes~$h$.  Since $h$ cannot becomputed by a Turing machine, there cannot be a Turing machine thatdecides validity either.The first step in this strategy is to show that for every input~$w$and a Turing machine~$M$, we can effectively describe !!a{sentence}$!T(M, w)$ representing the instruction set of~$M$ and the input~$w$and !!a{sentence}~$!E(M, w)$ expressing ``$M$ eventually halts'' suchthat:\begin{quote}  $\Entails !T(M, w) \lif !E(M,w)$ iff $M$ halts for input~$w$.\end{quote}The bulk of our proof will consist in describing these sentences$!T(M, w)$ and~$!E(M, w)$ and in verifying that $!T(M, w) \lif !E(M, w)$is valid iff $M$~halts on input~$w$.\end{document}

content/turing-machines/undecidability/representing-tms.tex

% Part: turing-machines% Chapter: undecidability% Section: representing-tms\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{rep}\olsection{Representing Turing Machines}\begin{explain}In order to represent Turing machines and their behavior by !!a{sentence}of first-order logic, we have to define a suitable language. Thelanguage consists of two parts: !!{predicate}s for describingconfigurations of the machine, and expressions for numbering executionsteps (``moments'') and positions on the tape.We introduce two kinds of !!{predicate}s, both of them 2-place: Foreach state~$q$, !!a{predicate}~$\Obj Q_q$, and for each tapesymbol~$\sigma$, !!a{predicate}~$\Obj S_\sigma$. The former allow usto describe the state of~$M$ and the position of its tape head, thelatter allow us to describe the contents of the tape.  In order to express the positions of the tape head and the number ofsteps executed, we need a way to express numbers. This is done using!!a{constant}~$\Obj 0$, and a $1$-place function~$\prime$, thesuccessor function. By convention it is written \emph{after} itsargument (and we leave out the parentheses).For each number $n$ there is a canonical term~$\num{n}$, the\emph{numeral} for~$n$, which represents it in~$\Lang L_M$. $\num{0}$is $\Obj 0$, $\num{1}$ is $\Obj 0'$, $\num{2}$ is $\Obj 0''$, and soon. More formally:\begin{align*}\num{0} & = \Obj 0 \\\num{n+1} &= \num{n}'\end{align*}The term $\num{0}$, i.e., $\Obj 0$ names the leftmost position on thetape as well as the time before the first execution step (the initialconfiguration). The term $\num{1}$, i.e., $\Obj 0'$ names the squareto the right of the leftmost square, and the time after the firstexecution step, and so on.We also introduce !!a{predicate}~$<$ to express both the ordering oftape positions (when it means ``to the left of'') and execution steps(then it means ``before'').Once we have the language in place, we list the ``axioms'' of $!T(M,w)$, i.e., the !!{sentence}s which, taken together, describe thebehavior of~$M$ when run on input~$w$.  There will be !!{sentence}swhich lay down conditions on $\Obj 0$, $\prime$, and $<$,!!{sentence}s that describes the input configuration, and!!{sentence}s that describe what the configuration of $M$ is after itexecutes a particular instruction.\end{explain}\begin{defn}  \ollabel{defn:tm-descr}Given a Turing machine $M = \tuple{Q, \Sigma, q_0, \delta}$, thelanguage~$\Lang L_M$ consists of:\begin{enumerate}\item A two-place !!{predicate} $\Obj Q_q(x, y)$ for every state~$q \in  Q$.  Intuitively, $\Obj Q_q(\num{m}, \num{n})$ expresses ``after $n$  steps, $M$ is in state~$q$ scanning the $m$th square.''\item A two-place !!{predicate} $\Obj S_\sigma(x, y)$ for every  symbol~$\sigma\in \Sigma$.  Intuitively, $\Obj S_\sigma(\num{m},  \num{n})$ expresses ``after $n$ steps, the $m$th square contains  symbol~$\sigma$.''\item A !!{constant} $\Obj 0$\item A one-place !!{function} $\prime$\item A two-place !!{predicate} $<$\end{enumerate}\end{defn}The !!{sentence}s describing the operation of the Turing machine~$M$ oninput $w = \sigma_{i_1}\dots\sigma_{i_k}$ are the following:\begin{enumerate}\item Axioms describing numbers and~$<$:\begin{enumerate}\item !!^a{sentence} that says that every number is less than its successor:\[\lforall[x][x < x']\]\item !!^a{sentence} that ensures that $<$ is transitive:\[\lforall[x][\lforall[y][\lforall[z][      ((x < y \land y < z) \lif x < z)]]]\]\end{enumerate}\item Axioms describing the input configuration:\begin{enumerate}\item After $0$~steps---before the machine starts---$M$ is in  the initial state~$q_0$, scanning square~$1$:\[\Obj Q_{q_0}(\num{1}, \num{0})\]\item The first $k+1$ squares contain the symbols $\TMendtape$,  $\sigma_{i_1}$, \dots, $\sigma_{i_k}$:\[\Obj S_\TMendtape(\num{0}, \num{0}) \land\Obj S_{\sigma_{i_1}}(\num{1}, \num{0}) \land\dots \land\Obj S_{\sigma_{i_k}}(\num{k}, \num{0})\]\item Otherwise, the tape is empty:\[\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{0}))]\]\end{enumerate}\item Axioms describing the transition from one configuration to  the next:For the following, let $!A(x, y)$ be the conjunction of all !!{sentence}sof the form\[\lforall[z][  (((z < x \lor x < z) \land \Obj S_\sigma(z, y))  \lif \Obj S_\sigma(z, y'))]\]where $\sigma \in \Sigma$.  We use $!A(\num{m},\num{n})$ to express``other than at square~$m$, the tape after $n+1$ steps is the same asafter $n$ steps.''\begin{enumerate}\item \ollabel{rep-right} For every instruction $\delta(q_i, \sigma) =  \tuple{q_j, \sigma', \TMright}$, the !!{sentence}:\begin{align*}& \lforall[x][\lforall[y][(   (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\&\qquad   (\Obj Q_{q_j}(x', y') \land \Obj S_{\sigma'}(x, y') \land!A(x, y)))\end{align*}This says that if, after~$y$ steps, the machine is in state~$q_i$scanning square~$x$ which contains symbol~$\sigma$, then after $y+1$steps it is scanning square~$x+1$, is in state~$q_j$, square~$x$ nowcontains~$\sigma'$, and every square other than~$x$ contains thesame symbol as it did after~$y$ steps.\item \ollabel{rep-left} For every instruction $\delta(q_i, \sigma) =  \tuple{q_j, \sigma', \TMleft}$, the !!{sentence}:\begin{align*}& \lforall[x][\lforall[y][    ((\Obj Q_{q_i}(x', y) \land \Obj S_{\sigma}(x', y)) \lif {}]]\\& \qquad   (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x', y') \land!A(x, y))) \land {}\\& \lforall[y][((\Obj Q_{q_i}(\num{0}, y) \land \Obj S_{\sigma}(\num{0},    y)) \lif {}]\\& \qquad (\Obj Q_{q_j}(\num{0}, y') \land \Obj S_{\sigma'}(\num{0},  y') \land !A(\num{0}, y)))\end{align*}Take a moment to think about how this works: now we don't start with``if scanning square~$x$ \dots'' but: ``if scanning square $x+1$\dots'' A move to the left means that in the next step the machine isscanning square~$x$.  But the square that is written on is~$x+1$.  Wedo it this way since we don't have subtraction or a predecessorfunction.Note that numbers of the form $x+1$ are $1$, $2$, \dots, i.e., thisdoesn't cover the case where the machine is scanning square~$0$ and issupposed to move left (which of course it can't---it just staysput). That special case is covered by the second conjunction: it saysthat if, after $y$ steps, the machine is scanning square~$0$ in state$q_i$ and square~$0$ contains symbol~$\sigma$, then after $y+1$ stepsit's still scanning square~$0$, is now in state~$q_j$, the symbol onsquare~$0$ is $\sigma'$, and the squares other than square~$0$ containthe same symbols they contained ofter $y$~steps.\item \ollabel{rep-stay} For every instruction $\delta(q_i, \sigma) =  \tuple{q_j, \sigma', \TMstay}$, the !!{sentence}:\begin{align*}& \lforall[x][\lforall[y][(   (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\&\qquad   (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x, y') \land!A(x, y)))\end{align*}\end{enumerate}\end{enumerate}Let $!T(M, w)$ be the conjunction of all the above !!{sentence}s for Turingmachine~$M$ and input~$w$.In order to express that~$M$ eventually halts, we have to find a!!{sentence} that says ``after some number of steps, the transitionfunction will be undefined.''  Let $X$~be the set of all pairs$\tuple{q, \sigma}$ such that~$\delta(q, \sigma)$ is undefined.  Let$!E(M, w)$ then be the !!{sentence}\[\lexists[x][\lexists[y][(\bigvee_{\tuple{q, \sigma} \in      X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))]]\]If we use a Turing machine with a designated halting state~$h$, itis even easier: then the !!{sentence}~$!E(M, w)$\[\lexists[x][\lexists[y][\Obj Q_h(x, y)]]\]expresses that the machine eventually halts.\begin{prop}\ollabel{prop:mlessk}If $m < k$, then $!T(M, w) \Entails \num{m} < \num{k}$\end{prop}\begin{proof}Exercise.\end{proof}\begin{prob}Prove \olref[tur][und][rep]{prop:mlessk}.(Hint: use induction on $k-m$).\end{prob}\end{document}

content/turing-machines/undecidability/verification.tex

% Part: turing-machines % Chapter: undecidability % Section: verification\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{ver} \olsection{Verifying the Representation}\begin{explain}In order to verify that our representation works, we have to prove twothings. First, we have to show that if $M$ halts on input~$w$, then$!T(M, w) \lif !E(M, w)$ is valid. Then, we have to show the converse,i.e., that if $!T(M, w) \lif !E(M, w)$ is valid, then $M$ does in facteventually halt when run on input~$w$.The strategy for proving these is very different. For the firstresult, we have to show that !!a{sentence} of first-order logic(namely, $!T(M, w) \lif !E(M, w)$) is valid. The easiest way to dothis is to give !!a{derivation}. Our proof is supposed to work for all$M$ and $w$, though, so there isn't really a single !!{sentence} forwhich we have to give !!a{derivation}, but infinitely many.  So the bestwe can do is to prove by induction that, whatever $M$ and~$w$ looklike, and however many steps it takes $M$ to halt on input~$w$, therewill be !!a{derivation} of $!T(M, w) \lif !E(M, w)$.Naturally, our induction will proceed on the number of steps $M$ takesbefore it reaches a halting configuration. In our inductive proof,we'll establish that for each step~$n$ of the run of $M$ on input~$w$,$!T(M, w) \Entails !C(M, w, n)$, where $!C(M, w, n)$ correctlydescribes the configuration of $M$ run on~$w$ after~$n$ steps. Now if$M$ halts on input~$w$ after, say, $n$ steps, $!C(M, w, n)$ willdescribe a halting configuration. We'll also show that $!C(M, w, n)\Entails !E(M, w)$, whenever $!C(M, w, n)$ describes a haltingconfiguration.  So, if $M$ halts on input~$w$, then for some~$n$, $M$will be in a halting configuration after $n$~steps. Hence, $!T(M, w)\Entails !C(M, w, n)$ where $!C(M, w, n)$ describes a haltingconfiguration, and since in that case $!C(M, w, n) \Entails !E(M, w)$,we get that $T(M, w) \Entails !E(M, w)$, i.e., that $\Entails !T(M, w)\lif !E(M, w)$.The strategy for the converse is very different. Here we assume that$\Entails !T(M, w) \lif !E(M, w)$ and have to prove that $M$ halts oninput~$w$.  From the hypothesis we get that $!T(M, w) \Entails !E(M,w)$, i.e., $!E(M, w)$ is true in every !!{structure} in which $!T(M,w)$ is true. So we'll describe !!a{structure}~$\Struct{M}$ in which$!T(M, w)$ is true: its domain will be $\Nat$, and the interpretationof all the $\Obj Q_q$ and $\Obj S_\sigma$ will be given by theconfigurations of~$M$ during a run on input~$w$.  So, e.g.,$\Sat{M}{\Obj Q_q(\num{m}, \num{n})}$ iff $T$, when run on input~$w$for $n$ steps, is in state~$q$ and scanning square~$m$.  Now since$!T(M, w) \Entails !E(M, w)$ by hypothesis, and since $\Sat{M}{!T(M,  w)}$ by construction, $\Sat{M}{!E(M, w)}$.  But $\Sat{M}{!E(M, w)}$iff there is some $n \in \Domain{M} = \Nat$ so that $M$, run oninput~$w$, is in a halting configuration after~$n$ steps.\end{explain}\begin{defn} Let $!C(M, w, n)$ be the !!{sentence}\[ \Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma_0}(\num{0}, \num{n})\land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}) \land\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))]\] where $q$ is the state of $M$ at time~$n$, $M$ is scanning square~$m$at time~$n$, square~$i$ contains symbol~$\sigma_i$ at time~$n$ for $0\le i \le k$ and $k$ is the right-most non-blank square of the tape attime~$0$, or the right-most square the tape head has visited after $n$steps, whichever is greater.\end{defn}\begin{lem}\ollabel{lem:halt-config-implies-halt}If $M$ run on input~$w$ is in a halting configuration after $n$ steps,then $!C(M, w, n) \Entails !E(M, w)$.\end{lem}\begin{proof}Suppose that $M$ halts for input~$w$ after $n$ steps.There is some state~$q$, square~$m$, and symbol~$\sigma$ such that:\begin{enumerate} \item After $n$ steps, $M$ is in state~$q$ scanning square~$m$ on  which~$\sigma$ appears.\item The transition function $\delta(q, \sigma)$ is undefined.\end{enumerate}$!C(M, w, n)$ is the description of this configuration and willinclude the clauses $\Obj Q_{q}(\num{m}, \num{n})$ and $\ObjS_{\sigma}(\num{m}, \num{n})$. These clauses together imply $!E(M,w)$:\[\lexists[x][\lexists[y][(\bigvee_{\tuple{q, \sigma} \in      X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))]]\]since $\Obj Q_{q'}(\num{m}, \num{n}) \land S_{\sigma'}(\num{m},\num{n}) \Entails \bigvee_{\tuple{q, \sigma} \in X} (\Obj Q_q(\num{m},\num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n}))$, as$\tuple{q',\sigma'} \in X$. \end{proof}\begin{explain}So if $M$ halts for input $w$, then there is some~$n$ such that $!C(M,w, n) \Entails !E(M,w)$.  We will now show that for any time~$n$,$!T(M, w) \Entails !C(M, w, n)$.\end{explain}\begin{lem}\ollabel{lem:config}For each $n$, if $M$ has not halted after $n$ steps, $!T(M, w)\Entails !C(M, w, n)$.\end{lem}\begin{proof}Induction basis: If $n = 0$, then the conjuncts of $!C(M, w, 0)$ arealso conjuncts of $!T(M, w)$, so entailed by it.Inductive hypothesis: If $M$ has not halted before the $n$th step,then $!T(M,w) \Entails !C(M, w, n)$. We have to show that (unless$!C(M, w, n)$ describes a halting configuration), $!T(M, w) \Entails!C(M, w, n+1)$.Suppose $n > 0$ and after $n$ steps, $M$ started on $w$ is instate~$q$ scanning square~$m$. Since $M$ does not halt after~$n$steps, there must be an instruction of one of the following threeforms in the program of~$M$:\begin{enumerate} \item \ollabel{right} $\delta(q, \sigma) = \tuple{q', \sigma', \TMright}$\item \ollabel{left} $\delta(q, \sigma) = \tuple{q', \sigma', \TMleft}$\item \ollabel{stay} $\delta(q, \sigma) = \tuple{q', \sigma', \TMstay}$\end{enumerate}We will consider each of these three cases in turn. \begin{enumerate} \item Suppose there is an instruction of the form~\olref{right}.  By \olref[rep]{defn:tm-descr}\olref[rep]{rep-right}, this means that\begin{align*} & \lforall[x][\lforall[y][((\Obj Q_{q}(x,  y) \land \Obj S_\sigma(x, y)) \lif {}]]\\& \qquad (\Obj Q_{q'}(x',  y') \land \Obj S_{\sigma'}(x, y') \land !A(x, y)))  \intertext{is a conjunct of $!T(M,w)$. This entails the following  !!{sentence} (universal instantiation, $\num{m}$ for~$x$ and  $\num{n}$ for~$y$):}& (\Obj Q_{q}(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m},\num{n})) \lif {}\\& \qquad (\Obj Q_{q'}(\num{m}', \num{n}') \land\Obj S_{\sigma'}(\num{m}, \num{n}') \land !A(\num{m}, \num{n})).\intertext{By induction hypothesis, $!T(M, w) \Entails !C(M, w, n)$,  i.e.,}& \Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma_0}(\num{0}, \num{n})\land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}) \land \\& \qquad\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))]\\\intertext{Since after $n$ steps, tape square~$m$ contains~$\sigma$,  the corresponding conjunct is~$\Obj S_\sigma(\num{m}, \num{n})$,  so this entails:}& \Obj Q_{q}(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m},   \num{n})\intertext{We now get}& \Obj Q_{q'}(\num{m}', \num{n}') \land \Obj S_{\sigma'}(\num{m},  \num{n}') \land {}\\& \qquad\Obj S_{\sigma_0}(\num{0}, \num{n}') \land \dots \land  \Obj S_{\sigma_k}(\num{k}, \num{n}') \land {}\\& \qquad \lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))]\end{align*}as follows: The first line comes directly from the consequent of thepreceding conditional, by modus ponens. Each conjunct in the middleline---which excludes $S_{\sigma_m}(\num{m},\num{n}')$---follows fromthe corresponding conjunct in~$!C(M, w, n)$ together with $!A(\num{m},\num{n})$.If $m < k$, $!T(M,w) \Proves \num{m} < \num {k}$(\olref[rep]{prop:mlessk}) and by transitivity of~$<$, we have$\lforall[x][(\num{k} < x \lif \num{m} < x)]$.  If $m = k$, then$\lforall[x][(\num{k} < x \lif \num{m} < x)]$ by logic alone.  Thelast line then follows from the corresponding conjunct in $!C(M, w,n)$, $\lforall[x][(\num{k} < x \lif \num{m} < x)]$, and $!A(\num{m},\num{n})$.  If $m<k$, this already is $!C(M, w, n+1)$.Now suppose $m=k$. In that case, after $n+1$ steps, the tape head hasalso visited square~$k+1$, which now is the right-most squarevisited.  So $!C(M, w, n+1)$ has a new conjunct, $\ObjS_\TMblank(\num{k}',\num{n}')$, and the last conjunct is$\lforall[x][(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))]$. Wehave to verify that these two !!{sentence}s are also implied.We already have $\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x,  \num{n}'))]$. In particular, this gives us $\num{k} < \num{k}' \lif\Obj S_\TMblank(\num{k}', \num{n}')$. From the axiom $\lforall[x][x <  x']$ we get $\num{k} < \num{k}'$. By modus ponens, $\ObjS_\TMblank(\num{k}',\num{n}')$ follows.Also, since $!T(M,w) \Proves \num{k} < \num{k}'$, the axiom fortransitivity of~$<$ gives us $\lforall[x][(\num{k}' < x \lif \Obj  S_\TMblank(x, \num{n}'))]$. (We leave the verification of this as anexercise.)\item Suppose there is an instruction of the form~\olref{left}.  Then, by \olref[rep]{defn:tm-descr}\olref[rep]{rep-left},\begin{align*} & \lforall[x][\lforall[y][((\Obj Q_{q}(x', y) \land \Obj    S_{\sigma}(x', y)) \lif {}]]\\& \qquad (\Obj Q_{q'}(x, y') \land \Obj  S_{\sigma'}(x', y') \land !A(x, y))) \land {}\\& \lforall[y][((\Obj Q_{q_i}(\num{0}, y) \land \Obj S_{\sigma}(\num{0},    y)) \lif {}]\\& \qquad (\Obj Q_{q_j}(\num{0}, y') \land \Obj S_{\sigma'}(\num{0}, y')  \land !A(\num{0}, y)))\intertext{is a conjunct of $!T(M,w)$. If $m>0$, then let $l = m - 1$  (i.e., $m = l+1$). The first conjunct of the above !!{sentence}  entails the following:}& (\Obj Q_{q}(\num{l}', \num{n}) \land \Obj S_{\sigma}(\num{l}', \num{n}))\lif {} \\& \qquad (\Obj Q_{q'}(\num{l}, \num{n}') \land \Obj S_{\sigma'}(\num{l}',\num{n}') \land !A(\num{l}, \num{n}))\intertext{Otherwise, let $l = m = 0$ and consider the following !!{sentence}  entailed by the second conjunct:}& ((\Obj Q_{q_i}(\num{0}, \num{n}) \land \Obj S_{\sigma}(\num{0}, \num{n})) \lif {}\\& \qquad   (\Obj Q_{q_j}(\num{0}, \num{n}') \land \Obj S_{\sigma'}(\num{0}, \num{n}') \land!A(\num{0}, \num{n}))) \intertext{Either sentence implies}&  \Obj Q_{q'}(\num{l}, \num{n}') \land \Obj S_{\sigma'}(\num{m},  \num{n}') \land {}\\&\qquad  \Obj S_{\sigma_0}(\num{0}, \num{n}')\land \dots \land  \Obj S_{\sigma_k}(\num{k}, \num{n}')  \land {} \\& \qquad  \lforall[x][(\num{k} < x  \lif \Obj S_\TMblank(x, \num{n}'))]\end{align*}as before. (Note that in the first case, $\num{l}' \ident \num{l+1}\ident \num{m}$ and in the second case $\num{l} \ident \num{0}$.) Butthis just is $!C(M, w, n+1)$.\item Case \olref{stay} is left as an exercise.\end{enumerate}We have shown that for any~$n$, $!T(M, w) \Entails !C(M, w, n)$.\end{proof}\begin{prob}Complete case~\olref[tur][und][ver]{stay} of the proof of\olref[tur][und][ver]{lem:config}.\end{prob}\begin{prob}Give !!a{derivation} of $\Obj S_{\sigma_i}(\num{i}, \num{n}')$ from$\Obj S_{\sigma_i}(\num{i}, \num{n})$ and $!A(m, n)$ (assuming $i \neqm$, i.e., either $i < m$ or $m < i$).\end{prob}\begin{prob}Give !!a{derivation} of $\lforall[x][(\num{k}' < x \lif \Obj  S_\TMblank(x, \num{n}'))]$ from $\lforall[x][(\num{k} < x \lif \Obj  S_\TMblank(x, \num{n}'))]$, $\lforall[x][x < x']$, and$\lforall[x][\lforall[y][\lforall[z][ ((x < y \land y < z) \lif x <      z)]]]$.)\end{prob}\begin{lem}\ollabel{lem:valid-if-halt}If $M$ halts on input~$w$, then $!T(M, w) \lif!E(M, w)$ is valid.\end{lem}\begin{proof}By \olref{lem:config}, we know that, for any time~$n$, thedescription~$!C(M, w, n)$ of the configuration of $M$ at time~$n$ isentailed by~$!T(M, w)$.  Suppose $M$ halts after $k$ steps. At thatpoint, it will be scanning square~$m$, for some~$m \in \Nat$. Then$!C(M, w, k)$ describes a halting configuration of~$M$, i.e., itcontains as conjuncts both $\Obj Q_q(\num{m}, \num{k})$ and $\ObjS_\sigma(\num{m}, \num{k})$ with $\delta(q,\sigma)$ undefined.  Thus,by \olref{lem:halt-config-implies-halt}, $!C(M, w, k) \Entails !E(M,w)$. But since $!T(M, w) \Entails !C(M, w, k)$, we have $!T(M, w)\Entails !E(M, w)$ and therefore $!T(M, w) \lif !E(M, w)$ is valid.\end{proof}\begin{explain} To complete the verification of our claim, we also have toestablish the reverse direction: if $!T(M, w) \lif !E(M, w)$ is valid, then$M$ does in fact halt when started on input~$w$. \end{explain}\begin{lem}\ollabel{lem:halt-if-valid}If $\Entails !T(M, w) \lif !E(M, w)$, then $M$ halts on input~$w$.\end{lem}\begin{proof}Consider the $\Lang L_M$-!!{structure}~$\Struct M$ withdomain~$\Nat$ which interprets $\Obj 0$ as~$0$, $\prime$~as the successorfunction, and $<$~as the less-than relation, and the predicates $\Obj Q_q$and~$\Obj S_\sigma$ as follows:\begin{align*}  \Assign{\Obj Q_q}{M} & =\Setabs{\tuple{m, n}}{\begin{array}{ll}\text{started on~$w$, after~$n$ steps,}\\ \text{$M$ is in state $q$  scanning square~$m$}\end{array}} \\\Assign{\Obj S_\sigma}{M} & = \Setabs{\tuple{m, n}}{\begin{array}{ll}\text{started on~$w$, after $n$ steps,}\\ \text{square~$m$ of $M$ contains  symbol~$\sigma$}\end{array}}\end{align*}In other words, we construct the !!{structure}~$\Struct{M}$ so that itdescribes what $M$ started on input~$w$ actually does, step by step.Clearly, $\Sat{M}{!T(M, w)}$. If $\Entails !T(M, w) \lif !E(M, w)$,then also $\Sat{M}{!E(M, w)}$, i.e.,\[\Sat{M}{\lexists[x][\lexists[y][(\bigvee_{\tuple{q, \sigma} \in      X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))]]}.\]As $\Domain{M} = \Nat$, there must be $m$, $n \in \Nat$ so that$\Sat{M}{\Obj Q_q(\num{m}, \num{n}) \land \Obj S_\sigma(\num{m},\num{n})}$ for some~$q$ and~$\sigma$ such that $\delta(q, \sigma)$ isundefined. By the definition of~$\Struct M$, this means that $M$started on input~$w$ after~$n$ steps is in state~$q$ and readingsymbol~$\sigma$, and the transition function is undefined, i.e.,$M$~has halted.\end{proof}\end{document}

content/turing-machines/undecidability/unsolvability-decision-problem.tex

% Part: turing-machines % Chapter: undecidability % Section: unsolvability-decision-problem\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{uns} \olsection{The Decision Problem is Unsolvable}\begin{thm}\ollabel{thm:decision-prob}The decision problem is unsolvable: There is no Turing machine~$D$,which when started on a tape that contains !!a{sentence}~$!B$ offirst-order logic as input, $D$~eventually halts, and outputs~$1$ iff$!B$ is valid and $0$ otherwise.\end{thm}\begin{proof}Suppose the decision problem were solvable, i.e., suppose there were aTuring machine~$D$. Then we could solve the halting problem asfollows. We construct a Turing machine~$E$ that, given as input thenumber~$e$ of Turing machine~$M_e$ and input~$w$, computes thecorresponding !!{sentence}~$!T(M_e, w) \lif !E(M_e, w)$ and halts,scanning the leftmost square on the tape.  The machine $E \concat D$would then, given input $e$ and $w$, first compute~$!T(M_e, w) \lif!E(M_e, w)$ and then run the decision problem machine~$D$ on thatinput.  $D$ halts with output~$1$ iff $!T(M_e, w) \lif !E(M_e, w)$ isvalid and outputs~$0$ otherwise. By \olref[ver]{lem:halt-if-valid} and\olref[ver]{lem:valid-if-halt}, $!T(M_e, w) \lif !E(M_e, w)$ is validiff $M_e$ halts on input~$w$. Thus, $E\concat D$, given input $e$ and$w$ halts with output~$1$ iff $M_e$ halts on input~$w$ and halts withoutput~$0$ otherwise. In other words, $E \concat D$ would solve thehalting problem.  But we know, by \olref[hal]{thm:halting-problem},that no such Turing machine can exist.\end{proof}\begin{cor}\ollabel{cor:undecidable-sat}%It is undecidable if an arbitrary !!{sentence} of first-order logic is satisfiable.\end{cor}\begin{proof}  Suppose satisfiability were decidable by a Turing machine~$S$. Then  we could solve the decision problem as follows: Given  !!a{sentence}~$B$ as input, move $!B$ to the right one square.  Return to square~$1$ and write the symbol~$\lnot$.  Now run the Turing machine~$S$. It eventually halts with output  either $1$ (if $\lnot !B$ is satisfiable) or~$0$ (if $\lnot !B$ is  unsatisfiable) on the tape. If there is a~$\TMstroke$ on square~$1$,  erase it; if square~$1$ is empty, write a~$\TMstroke$, then halt.  This Turing machine always halts, and its output is~$1$ iff $\lnot  !B$ is unsatisfiable and $0$~otherwise. Since $!B$ is valid iff  $\lnot !B$~is unsatisfiable, the machine outputs~$1$ iff $!B$ is  valid, and $0$~otherwise, i.e., it would solve the decision problem.\end{proof}\begin{explain}So there is no Turing machine which always gives acorrect ``yes'' or ``no'' answer to the question ``Is $!B$ a valid!!{sentence} of first-order logic?'' However, there \emph{is} a Turingmachine that always gives a correct ``yes'' answer---but simply doesnot halt if the answer is ``no.'' This follows from the soundness andcompleteness theorem of first-order logic, and the fact that!!{derivation}s can be effectively enumerated.\end{explain}\begin{thm}  \ollabel{thm:valid-ce}%  Validity of first-order !!{sentence}s is semi-decidable: There is a  Turing machine~$E$, which when started on a tape that contains  !!a{sentence}~$!B$ of first-order logic as input, $E$~eventually  halts and outputs~$1$ iff $!B$ is valid, but does not halt  otherwise.\end{thm}\begin{proof}  All possible !!{derivation}s of first-order logic can be generated,  one after another, by an effective algorithm.  The machine~$E$ does  this, and when it finds !!a{derivation} that shows that $\Proves  !B$, it halts with output~$1$. By the soundness theorem, if $E$  halts with output~$1$, it's because~$\Entails !B$. By the  completeness theorem, if $\Entails !B$ there is !!a{derivation} that  shows that~$\Proves !B$. Since $E$ systematically generates all  possible !!{derivation}s, it will eventually find one that  shows~$\Proves !B$, so will eventually halt with output~$1$.\end{proof}\end{document}

content/turing-machines/undecidability/trakhtenbrot.tex

% Part: turing-machines% Chapter: undecidability% Section: trakhtenbrot\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{tur}{und}{tra}\olsection{Trakhtenbrot's Theorem}\begin{explain}  In \olref[rep]{sec} we defined !!{sentence}s $!T(M,w)$ and~$!E(M,w)$  for a Turing machine~$M$ and input string~$w$. Then we showed in  \olref[ver]{lem:valid-if-halt} and \olref[ver]{lem:halt-if-valid}  that $!T(M,w) \lif !E(M,w)$ is valid iff $M$, started on input~$w$,  eventually halts. Since the Halting Problem is undecidable, this  implies that validity and satisfiability of !!{sentence}s of  first-order logic is undecidable  (\cref{tur:und:uns:thm:decision-prob,tur:und:uns:cor:undecidable-sat}).  But validity and satisfiability of sentences is defined for  arbitrary !!{structure}s, finite or infinite. You might suspect that  it is easier to decide if !!a{sentence} is satisfiable in a finite  !!{structure} (or valid in all finite !!{structure}s). We can adapt  the proof of the unsolvability of the decision problem so that it  shows this is not the case.  First, if you go back to the proof of  \olref[ver]{lem:halt-if-valid}, you'll see that what we did there is  produce a model~$\Struct M$ of~$!T(M,w)$ which describes exactly  what machine~$M$ does when started on input~$w$.  The domain of that  model was~$\Nat$, i.e., infinite. But if $M$ actually halts on  input~$w$, we can build a finite model~$\Struct M'$ in the same way.  Suppose $M$ started on input~$w$ halts after~$k$ steps. Take as  domain~$\Domain{M'}$ the set $\{0, \dots, n\}$, where $n$ is the  larger of~$k$ and the length of~$w$, and let  \[    \Assign{\prime}{M'}(x) =     \begin{cases}      x + 1 &\text{if $x < n$}\\      n &\text{otherwise,}    \end{cases}  \]  and $\tuple{x,y} \in \Assign{<}{M'}$ iff $x < y$ or $x = y = n$.  Otherwise $\Struct{M'}$ is defined just like~$\Struct{M}$. By the  definition of~$\Struct{M'}$, just like in the proof of  \olref[ver]{lem:halt-if-valid}, $\Sat{M'}{!T(M,w)}$.  And since we  assumed that $M$ halts on input~$w$, $\Sat{M'}{!E(M,w)}$. So,  $\Struct{M'}$ is a finite model of~$!T(M,w) \land !E(M,w)$ (note  that we've replaced $\lif$ with~$\land$).    We are halfway to a proof: we've shown that if $M$ halts on  input~$w$, then $!T(M,w) \land !E(M,w)$ has a finite model.  Unfortunately, the converse of this does not hold, i.e., there are  Turing machines that don't halt on some input~$w$, but $!T(M,w)  \land !E(M,w)$ still has a finite model. For instance, consider the  machine~$M$ with the single state $q_0$ and instruction  $\delta(q_0,\TMblank) = \tuple{q_0,\TMblank,\TMstay}$. Started on  empty input~$w = \emptyseq$, this machine never halts: it is in an  infinite loop, but does not change the tape or move the head. All  configurations are the same (same state, same head position, same  tape contents). We can define a finite !!{structure}~$\Struct{M''}$  that satisfies $!T(M,\emptyseq) \land !E(M,\emptyseq)$ (exercise).  We can, however, change~$!T(M,w)$ in a suitable way so that such  !!{structure}s are ruled out.  \begin{prob}    Let $M$ be a Turing machine with the single state $q_0$ and single    instruction $\delta(q_0,\TMblank) = \tuple{q,\TMblank,\TMstay}$.    Let $\Domain{M''} = \{0, 1, 2\}$, $\Assign{\prime}{M''}(0) =    \Assign{\prime}{M'}(1) = 1$ and $\Assign{\prime}{M''}(2) = 2$, and    $\Assign{<}{M''} = \{\tuple{0,1}, \tuple{1,1}, \tuple{2,2}\}$.    Define $\Assign{\Obj Q_{q_0}}{M''}$, $\Assign{\Obj    S_{\TMblank}}{M''}$, and $\Assign{\Obj S_{\TMendtape}}{M''}$ so    that $!T(M,\emptyseq)$ and $!E(M,\emptyseq)$ become true and    explain why they are. Hint: Observe that $\delta(q_0, \TMendtape)$    is undefined. Ensure that    \begin{align*}    & \Obj Q_{q_0}(\num{1}, \num{n}) \land \Obj S_{\TMendtape}(\num{0}, \num{n})      \land       \lforall[x][(\num{0} < x \lif \Obj S_\TMblank(x, \num{n}))] \text{\quad for all $n \in \Nat$}\\    & \lexists[y][(\Obj Q_{q_0}(\num{0}, y) \land \Obj S_{\TMendtape}(\num{0}, y))]    \end{align*}    are both true in~$\Struct{M''}$.  \end{prob}\end{explain}Consider the !!{sentence}s describing the operation of the Turingmachine~$M$ on input $w = \sigma_{i_1}\dots\sigma_{i_k}$:\begin{enumerate}\item Axioms describing numbers and~$<$ (just like in the definitionof~$!T(M,w)$ in \olref[rep]{sec}).\item Axioms describing the input configuration: just like in the definitionof~$!T(M,w)$.\item Axioms describing the transition from one configuration to  the next:For the following, let $!A(x, y)$ be as before, and let\[  !B(y) \ident \lforall[x][(x < y \lif \eq/[x][y])].\]\begin{enumerate}\item \ollabel{rep-right} For every instruction $\delta(q_i, \sigma) =  \tuple{q_j, \sigma', \TMright}$, the !!{sentence}:\begin{align*}& \lforall[x][\lforall[y][(   (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\&\qquad   (\Obj Q_{q_j}(x', y') \land \Obj S_{\sigma'}(x, y') \land!A(x, y) \land !B(y')))\end{align*}\item \ollabel{rep-left} For every instruction $\delta(q_i, \sigma) =  \tuple{q_j, \sigma', \TMleft}$, the !!{sentence}\begin{align*}& \lforall[x][\lforall[y][    ((\Obj Q_{q_i}(x', y) \land \Obj S_{\sigma}(x', y)) \lif {}]]\\& \qquad   (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x', y') \land!A(x, y))) \land {}\\& \lforall[y][((\Obj Q_{q_i}(\num{0}, y) \land \Obj S_{\sigma}(\num{0},    y)) \lif {}]\\& \qquad (\Obj Q_{q_j}(\num{0}, y') \land \Obj S_{\sigma'}(\num{0},  y') \land !A(\num{0}, y) \land !B(y')))\end{align*}\item \ollabel{rep-stay} For every instruction $\delta(q_i, \sigma) =  \tuple{q_j, \sigma', \TMstay}$, the !!{sentence}:\begin{align*}& \lforall[x][\lforall[y][(   (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\&\qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x, y') \land!A(x, y) \land !B(y')))\end{align*}\end{enumerate}As you can see, the !!{sentence}s describing the transitions of~$M$ are the same as the corresponding !!{sentence}in~$!T(M,w)$, except we add $!B(y')$ at the end. $!B(y')$~ensuresthat the number $y'$ of the ``next'' configuration is different fromall previous numbers $\Obj 0$, $\Obj 0'$, \dots.% \item Sentences that express consistency conditions:% \begin{enumerate}%   \item\ollabel{rep-con-symb}%%   !!^a{sentence} that says that no square can have more than one%   symbol on it at any given time:%   \[\lforall[x][\lforall[y][(\Obj S_{\sigma}(x, y) \lif \lnot \Obj%   S_{\sigma'}(x, y))]],\]%   for every pair $\sigma \neq \sigma'$ of tape symbols of~$T$.%   \item\ollabel{rep-con-state}%%   !!^a{sentence} that says that $M$ cannot be in more than one state%   at any given time:%   \[\lforall[x][\lforall[y][(\Obj Q_{q}(x, y) \lif%   \lforall[z][\lnot \Obj%   Q_{q'}(z, y))]],\]%   for every pair $q \neq q'$ of states of~$T$.%   \item\ollabel{rep-con-tape}%%   !!^a{sentence} that says that $M$ cannot be on more than one tape%   square at any given time:%   \[\lforall[x][\lforall[y][(\Obj Q_{q}(x, y) \lif%   \lforall[z][\eq/[z][y]\lif \lnot \Obj%   Q_{q'}(z, y))]],\]%   for every pair $q$, $q'$ of states of~$T$.% \end{enumerate}\end{enumerate}Let $!T'(M, w)$ be the conjunction of all the above !!{sentence}s for Turingmachine~$M$ and input~$w$.\begin{lem}\ollabel{lem:halts-sat}  If $M$ started on input~$w$ halts, then $!T'(M,w) \land !E(M,w)$ has  a finite model.\end{lem}\begin{proof}  Let $\Struct{M'}$ be as in the proof of  \olref[ver]{lem:halt-if-valid}, except  \begin{align*}    \Domain{M'} & = \{0, \dots, n\},\\    \Assign{\prime}{M'}(x) & =     \begin{cases}      x + 1 &\text{if $x < n$}\\      n &\text{otherwise,}    \end{cases} \\    \tuple{x,y} \in \Assign{<}{M'} &\text{iff $x < y$ or $x = y = n$,}  \end{align*}  where $n = \max(k,\len{w})$ and $k$~is the least number such that  $M$ started on input~$w$ has halted after~$k$ steps. We leave the  verification that $\Sat{M'}{!T'(M,w) \land E(M,w)}$ as an exercise.\end{proof}\begin{prob}  Complete the proof of \olref[tur][und][tra]{lem:halts-sat} by  proving that $\Sat{M'}{!T(M,w) \land E(M,w)}$.\end{prob}\begin{lem}\ollabel{lem:sat-halts}  If $!T'(M,w) \land !E(M,w)$ has a finite model, then $M$ started on  input~$w$ halts.\end{lem}\begin{proof}  We show the contrapositive. Suppose that $M$ started on~$w$ does not  halt. If $!T'(M,w) \land !E(M,w)$ has no model at all, we are done.  So assume $\Struct{M}$ is a model of~$!T(M,w) \land !E(M, w)$. We  have to show that it cannot be finite.    We can prove, just like in \olref[ver]{lem:config}, that if~$M$,  started on input~$w$, has not halted after~$n$ steps, then $!T'(M,w)  \Entails !C(M, w, n) \land !B(\num{n})$. Since $M$ started on  input~$w$ does not halt, $!T'(M,w) \Entails !C(M, w, n) \land  !B(\num{n})$ for all~$n \in \Nat$. Note that by  \olref[rep]{prop:mlessk}, $!T'(M,w) \Entails \num{k} < \num{n}$ for  all~$k < n$. Also $!B(\num{n}) \Entails \num{k} < \num{n} \lif  \eq/[\num{k}][\num{n}]$. So, $\Sat{M}{\eq/[\num{k}][\num{n}]}$ for  all~$k < n$, i.e., the infinitely many terms~$\num{k}$ must all have  different values in~$\Struct{M}$. But this requires that  $\Domain{M}$ be infinite, so $\Struct{M}$ cannot be a finite model  of~$!T'(M,w) \land !E(M, w)$.\end{proof}\begin{prob}  Complete the proof of \olref[tur][und][tra]{lem:sat-halts} by  proving that if~$M$, started on input~$w$, has not halted after~$n$  steps, then $!T'(M,w) \Entails !B(\num{n})$.\end{prob}\begin{thm}[Trakhtenbrot's Theorem]  \ollabel{thm:trakhtenbrodt}  It is undecidable if an arbitrary !!{sentence} of first-order logic has  a finite model (i.e., is finitely satisfiable).\end{thm}\begin{proof}  Suppose there were a Turing machine~$F$ that decides the finite  satisfiability problem. Then given any Turing machine~$M$ and  input~$w$, we could compute the sentence~$!T'(M,w) \land !E(M,w)$,  and use~$F$ to decide if it has a finite model. By  \cref{tur:und:tra:lem:halts-sat,tur:und:tra:lem:sat-halts}, it does iff $M$  started on input~$w$ halts. So we could use $F$ to solve the halting  problem, which we know is unsolvable.\end{proof}\begin{cor}\ollabel{cor:fproof-incomp}%  There can be no !!{derivation} system that is sound and complete for  \emph{finite} validity, i.e., !!a{derivation} system which has $\Proves !B$  iff $\Sat{M}{!B}$ for every finite !!{structure}~$\Struct{M}$.\end{cor}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[tur][und][tra]{cor:fproof-incomp}. Observe that $!B$ is  satisfied in every finite !!{structure} iff $\lnot !B$ is not  finitely satisfiable.  Explain why finite satisfiability is  semi-decidable in the sense of  \olref[tur][und][uns]{thm:valid-ce}. Use this to argue that if  there were !!a{derivation} system for finite validity, then finite  satisfiability would be decidable.\end{prob}\end{document}