3.2.5: Representing Turing Machines

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

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.

We introduce two kinds of predicate symbols, both of them 2-place: For each state \(q\), a predicate symbol \(\Obj Q_q\), and for each tape symbol \(\sigma\), a predicate symbol \(\Obj S_\sigma\). The former allow us to describe the state of \(M\) and the position of its tape head, the latter allow us to describe the contents of the tape.

In order to express the positions of the tape head and the number of steps executed, we need a way to express numbers. This is done using a constant symbol \(\Obj 0\), and a \(1\)-place function \(\prime\), the successor function. By convention it is written after its argument (and we leave out the parentheses). So \(\Obj 0\) names the leftmost position on the tape as well as the time before the first execution step (the initial configuration), \(\Obj 0'\) names the square to the right of the leftmost square, and the time after the first execution step, and so on. We also introduce a predicate symbol \(<\) to express both the ordering of tape 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 sentences which, taken together, describe the behavior of \(M\) when run on input \(w\). There will be sentences which lay down conditions on \(\Obj 0\), \(\prime\), and \(<\), sentences that describe the input configuration, and sentences that describe what the configuration of \(M\) is after it executes a particular instruction.

Definition \(\PageIndex{1}\)

Given a Turing machine \(M = \tuple{Q, \Sigma, q_0, \delta}\), the language \(\Lang L_M\) consists of:

1. A two-place predicate symbol \(\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.”
2. A two-place predicate symbol \(\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\).”
3. A constant symbol \(\Obj 0\)
4. A one-place function symbol \(\prime\)
5. A two-place predicate symbol \(<\)

For each number \(n\) there is a canonical term \(\num{n}\), the 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 so on. More formally: \[\begin{aligned} \num{0} & = \Obj 0 \\ \num{n+1} &= \num{n}'\end{aligned}\]

The sentences describing the operation of the Turing machine \(M\) on input \(w = \sigma_{i_1}\dots\sigma_{i_k}\) are the following:

1. Axioms describing numbers:
   1. A sentence that says that the successor function is injective: \[\lforall{x}{\lforall{y}{ (\eq[x'][y'] \lif \eq[x][y])}}\nonumber\]
   2. A sentence that says that every number is less than its successor: \[\lforall{x}{x < x'}\nonumber\]
   3. A sentence that ensures that \(<\) is transitive: \[\lforall{x}{\lforall{y}{\lforall{z}{ ((x < y \land y < z) \lif x < z)}}}\nonumber\]
   4. A sentence that connects \(<\) and \(=\): \[\lforall{x}{\lforall{y}{(x < y \lif \eqN[x][y])}}\nonumber\]
2. Axioms describing the input configuration:
   1. After \(0\) steps—before the machine starts—\(M\) is in the inital state \(q_0\), scanning square \(1\): \[\Obj Q_{q_0}(\num{1}, \num{0})\nonumber\]
   2. The first \(k+1\) squares contain the symbols \(\TMendtape\), \(\sigma_{i_1}\), …, \(\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})\nonumber\]
   3. Otherwise, the tape is empty: \[\lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{0}))}\nonumber\]
3. Axioms describing the transition from one configuration to the next:

   For the following, let \(A(x, y)\) be the conjunction of all sentences of the form \[\lforall{z}{ (((z < x \lor x < z) \land \Obj S_\sigma(z, y)) \lif \Obj S_\sigma(z, y'))}\nonumber\] 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 as after \(n\) steps.”

   1. For every instruction \(\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMright}\), the sentence: \[\begin{aligned} & \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{aligned}\] 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\) now contains \(\sigma'\), and every square other than \(x\) contains the same symbol as it did after \(y\) steps.
   2. For every instruction \(\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMleft}\), the sentence: \[\begin{aligned} & \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}(\Obj 0, y) \land \Obj S_{\sigma}(\Obj 0, y)) \lif {}}\\ & \qquad (\Obj Q_{q_j}(\Obj 0, y') \land \Obj S_{\sigma'}(\Obj 0, y') \land A(\Obj 0, y)))\end{aligned}\] Take a moment to think about how this works: now we don’t start with “if scanning square \(x\) …” but: “if scanning square \(x+1\) …” A move to the left means that in the next step the machine is scanning square \(x\). But the square that is written on is \(x+1\). We do it this way since we don’t have subtraction or a predecessor function.

      Note that numbers of the form \(x+1\) are \(1\), \(2\), …, i.e., this doesn’t cover the case where the machine is scanning square \(0\) and is supposed to move left (which of course it can’t—it just stays put). That special case is covered by the second conjunction: it says that if, after \(y\) steps, the machine is scanning square \(0\) in state \(q_i\) and square \(0\) contains symbol \(\sigma\), then after \(y+1\) steps it’s still scanning square \(0\), is now in state \(q_j\), the symbol on square \(0\) is \(\sigma'\), and the squares other than square \(0\) contain the same symbols they contained ofter \(y\) steps.

   3. For every instruction \(\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMstay}\), the sentence: \[\begin{aligned} & \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{aligned}\]

Let \(T(M, w)\) be the conjunction of all the above sentences for Turing machine \(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 transition function 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)))}}\nonumber\]

If we use a Turing machine with a designated halting state \(h\), it is even easier: then the sentence \(E(M, w)\) \[\lexists{x}{\lexists{y}{\Obj Q_h(x, y)}}\nonumber\] expresses that the machine eventually halts.

Proposition \(\PageIndex{1}\)

If \(m < k\), then \(T(M, w) \Entails \num{m} < \num{k}\)

Proof. Exercise. ◻

Problem \(\PageIndex{1}\)

Prove Proposition \(\PageIndex{1}\). (Hint: use induction on \(k-m\)).