3.2.6: Verifying the Representation

\(\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 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) \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 fact eventually halt when run on input \(w\).

The strategy for proving these is very different. For the first result, 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 do this 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 for which we have to give a derivation, but infinitely many. So the best we can do is to prove by induction that, whatever \(M\) and \(w\) look like, and however many steps it takes \(M\) to halt on input \(w\), there will be a derivation of \(T(M, w) \lif E(M, w)\).

Naturally, our induction will proceed on the number of steps \(M\) takes before 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)\) correctly describes 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)\) will describe a halting configuration. We’ll also show that \(C(M, w, n) \Entails E(M, w)\), whenever \(C(M, w, n)\) describes a halting configuration. 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 halting configuration, 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 on input \(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 interpretation of all the \(\Obj Q_q\) and \(\Obj S_\sigma\) will be given by the configurations 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 on input \(w\), is in a halting configuration after \(n\) steps.

Definition \(\PageIndex{1}\)

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}))}\nonumber\] 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 at time \(0\), or the right-most square the tape head has visited after \(n\) steps, whichever is greater.

Lemma \(\PageIndex{1}\)

If \(M\) run on input \(w\) is in a halting configuration after \(n\) steps, then \(C(M, w, n) \Entails E(M, w)\).

Proof. Suppose that \(M\) halts for input \(w\) after \(n\) steps. There is some state \(q\), square \(m\), and symbol \(\sigma\) such that:

1. After \(n\) steps, \(M\) is in state \(q\) scanning square \(m\) on which \(\sigma\) appears.
2. The transition function \(\delta(q, \sigma)\) is undefined.

\(C(M, w, n)\) is the description of this configuration and will include the clauses \(\Obj Q_{q}(\num{m}, \num{n})\) and \(\Obj S_{\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)))}}\nonumber\] 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\). ◻

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

Lemma \(\PageIndex{2}\)

For each \(n\), if \(M\) has not halted after \(n\) steps, \(T(M, w) \Entails C(M, w, n)\).

Proof. Induction basis: If \(n = 0\), then the conjuncts of \(C(M, w, 0)\) are also 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 in state \(q\) scanning square \(m\). Since \(M\) does not halt after \(n\) steps, there must be an instruction of one of the following three forms in the program of \(M\):

1. \(\delta(q, \sigma) = \tuple{q', \sigma', \TMright}\)
2. \(\delta(q, \sigma) = \tuple{q', \sigma', \TMleft}\)
3. \(\delta(q, \sigma) = \tuple{q', \sigma', \TMstay}\)

We will consider each of these three cases in turn.

1. Suppose there is an instruction of the form (1). By Definition 13.5.1(3a), this means that

   \[\begin{aligned}
   & \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)))
   \end{aligned}\]

   is a conjunct of \(T(M,w)\). This entails the following sentence (universal instantiation, \(\num{m}\) for \(x\) and \(\num{n}\) for \(y\)):

   \[\begin{aligned}
   & (\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})).
   \end{aligned}\]

   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 \lforall{x}{(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))}\nonumber\]

   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})) \nonumber\]

   We now get

   \[\begin{aligned}
   & \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{aligned}\]

   as follows: The first line comes directly from the consequent of the preceding conditional, by modus ponens. Each conjunct in the middle line—which excludes \(S_{\sigma_m}(\num{m},\num{n}')\)—follows from the 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}\) (Proposition 13.5.1) 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. The last 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 has also visited square \(k+1\), which now is the right-most square visited. So \(C(M, w, n+1)\) has a new conjunct, \(\Obj S_\TMblank(\num{k}',\num{n}')\), and the last conjuct is \(\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}\). We have to verify that these two sentences 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, \(\Obj S_\TMblank(\num{k}',\num{n}')\) follows.

   Also, since \(T(M,w) \Proves \num{k} < \num{k}'\), the axiom for transitivity of \(<\) gives us \(\lforall{x}{(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))}\). (We leave the verification of this as an exercise.)

2. Suppose there is an instruction of the form (2). Then, by Definition 13.5.1(3b),

   \[\begin{aligned}
   & \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}(\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}\]

   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:

   \[\begin{aligned}
   & (\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}))
   \end{aligned}\]

   Otherwise, let \(l = m = 0\) and consider the following sentence entailed by the second conjunct:

   \[\begin{aligned}
   & ((\Obj Q_{q_i}(\Obj 0, \num{n}) \land \Obj S_{\sigma}(\Obj 0, \num{n})) \lif {}\\
   & \qquad (\Obj Q_{q_j}(\Obj 0, \num{n}') \land \Obj S_{\sigma'}(\Obj 0, \num{n}') \land A(\Obj 0, \num{n})))
   \end{aligned}\]

   Either sentence implies

   \[\begin{aligned}
   & \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{aligned}\]

   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 \Obj 0\).) But this just is \(C(M, w, n+1)\).

3. Case (3) is left as an exercise.

We have shown that for any \(n\), \(T(M, w) \Entails C(M, w, n)\). ◻

Problem \(\PageIndex{1}\)

Complete case (3) of the proof of Lemma \(\PageIndex{2}\).

Problem \(\PageIndex{2}\)

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 \neq m\), i.e., either \(i < m\) or \(m < i\)).

Problem \(\PageIndex{3}\)

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)}}}\).)

Lemma \(\PageIndex{3}\)

If \(M\) halts on input \(w\), then \(T(M, w) \lif E(M, w)\) is valid.

Proof. By Lemma \(\PageIndex{2}\), we know that, for any time \(n\), the description \(C(M, w, n)\) of the configuration of \(M\) at time \(n\) is entailed by \(T(M, w)\). Suppose \(M\) halts after \(k\) steps. It will be scanning square \(m\), say. Then \(C(M, w, k)\) describes a halting configuration of \(M\), i.e., it contains as conjuncts both \(\Obj Q_q(\num{m}, \num{k})\) and \(\Obj S_\sigma(\num{m}, \num{k})\) with \(\delta(q,\sigma)\) undefined. Thus, by Lemma \(\PageIndex{1}\), \(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. ◻

To complete the verification of our claim, we also have to establish the reverse direction: if \(T(M, w) \lif E(M, w)\) is valid, then \(M\) does in fact halt when started on input \(m\).

Lemma \(\PageIndex{4}\)

If \(\Entails T(M, w) \lif E(M, w)\), then \(M\) halts on input \(w\).

Proof. Consider the \(\Lang L_M\)-structure \(\Struct M\) with domain \(\Nat\) which interprets \(\Obj 0\) as \(0\), \('\) as the successor function, and \(<\) as the less-than relation, and the predicates \(\Obj Q_q\) and \(\Obj S_\sigma\) as follows: \[\begin{aligned} \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{aligned}\] In other words, we construct the structure \(\Struct{M}\) so that it describes 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)))}}}.\nonumber\] 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)\) is undefined. By the definition of \(\Struct M\), this means that \(M\) started on input \(w\) after \(n\) steps is in state \(q\) and reading symbol \(\sigma\), and the transition function is undefined, i.e., \(M\) has halted. ◻