Undecidability

Explain

We can show that the set of all Turing machines is enumerable. This follows from the fact that each Turing machine can be finitely described. The set of states and the tape vocabulary are finite sets. The transition function is a partial function from $Q \times \Sigma$source to $Q \times \Sigma \times \{\TMleft, \TMright, \TMstay\}$source, and so likewise can be specified by listing its values for the finitely many argument pairs for which it is defined.

This is true as far as it goes, but there is a subtle difference. The definition of Turing machines made no restriction on what elements the set of states and tape alphabet can have. So, e.g., for every real number, there technically is a Turing machine that uses that number as a state. However, the behavior of the Turing machine is independent of which objects serve as states and vocabulary. Consider the two Turing machines in link to figure Variants of the Even machine.

These two diagrams correspond to two machines, $M$source with the tape alphabet $\Sigma = \{\TMendtape,\TMblank,\TMstroke\}$source and set of states $\{q_0,q_1\}$source, and $M'$source with alphabet $\Sigma' = \{\TMendtape,\TMblank,A\}$source and states $\{s,h\}$source. But their instructions are otherwise the same: $M$source will halt on a sequence of $n$source $\TMstroke$source's iff $n$source is even, and $M'$source will halt on a sequence of $n$source $A$source's iff $n$source is even. All we've done is rename $\TMstroke$source to $A$source, $q_0$source to $s$source, and $q_1$source to $h$source. This example generalizes: we can think of Turing machines as the same as long as one results from the other by such a renaming of symbols and states. In fact, we can simply think of the symbols and states of a Turing machine as positive integers: instead of $\sigma_0$source think $1$source, instead of $\sigma_1$source think $2$source, etc.; $\TMendtape$source is $1$source, $\TMblank$source is $2$source, etc. In this way, the Even machine becomes the machine depicted in link to figure A standard Even machine.

We might call a Turing machine with states and symbols that are positive integers a standard machine, and only consider standard machines from now on.Footnote: The terminology “standard machine” 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 that the set of standard Turing machines is enumerable. Suppose we are given a standard Turing machine $M = \tuple{Q, \Sigma, q_0, \delta}$source. How could we describe it using a finite string of positive integers? We'll first list the number of states, the states themselves, the number of symbols, the symbols themselves, and the starting state. (Remember, all of these are positive integers, since $M$source is a standard machine.) What about $\delta$source? The set of possible arguments, i.e., pairs $\tuple{q,\sigma}$source, is finite, since $Q$source and $\Sigma$source are finite. So the information in $\delta$source is simply the finite list of all $5$source-tuples $\tuple{q, \sigma, q', \sigma', d}$source where $\delta(q,\sigma) = \tuple{q', \sigma', D}$source, and $d$source is a number that codes the direction $D$source (say, $1$source for $\TMleft$source, $2$source for $\TMright$source, and $3$source for $\TMstay$source).

In this way, every standard Turing machine can be described by a finite list of positive integers, i.e., as a sequence $s_M \in (\PosInt)^*$source. For instance, the standard Even machine is coded by the sequence

Undecidability theorem

There are functions from $\Nat$source to $\Nat$source which are not Turing computable.

Proof

We know that the set of finite sequences of positive integers $(\PosInt)^*$source is enumerable (link to exercise on enumerating finite sequences of positive integers). This gives us that the set of descriptions of standard Turing machines, as a subset of $(\PosInt)^*$source, is itself enumerable. Every Turing computable function $\Nat$source to $\Nat$source is computed by some (in fact, many) Turing machines. By renaming its states and symbols to positive integers (in particular, $\TMendtape$source as $1$source, $\TMblank$source as $2$source, and $\TMstroke$source as $3$source) we can see that every Turing computable function is computed by a standard Turing machine. This means that the set of all Turing computable functions from $\Nat$source to $\Nat$source is also enumerable.

On the other hand, the set of all functions from $\Nat$source to $\Nat$source is not enumerable (link to exercise showing functions from natural numbers to natural numbers are nonenumerable). If all functions were computable by some Turing machine, we could enumerate the set of all functions by listing all the descriptions of Turing machines that compute them. So there are some functions that are not Turing computable.

Unsolved undecidability exercise

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.

Undecidability definition

If $M$source is the $e$sourceth Turing machine (in our fixed enumeration), we say that $e$source is an index of $M$source. We write $M_e$source for the $e$sourceth Turing machine.

Undecidability theorem

There is a universal Turing machine $U$source which, when started on input $\tuple{e,n}$source

1. halts iff $M_e$source halts on input $n$source, and

2. if $M_e$source halts with output $m$source, so does $U$source.

$U$source thus computes the function $f\colon \Nat \times \Nat \pto \Nat$source given by $f(e,n) = m$source if $M_e$source started on input $n$source halts with output $m$source, and undefined otherwise.

Proof

To actually produce $U$source 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$source's tape contains a block of $e$source $\TMstroke$source's followed by a block of $n$source $\TMstroke$source's. It first “decodes” the index $e$source to the right of the input $n$source. This produces a list of numbers (i.e., blocks of $\TMstroke$source's separated by $\TMblank$source's) that describes the instructions of machine $M_e$source. $U$source then writes the number of the start state of $M_e$source and the number $1$source on the tape to the right of the description of $M_e$source. (Again, these are represented in unary, as blocks of $\TMstroke$source's.) Next, it copies the input (block of $n$source $\TMstroke$source's) to the right---but it replaces each $\TMstroke$source by a block of three $\TMstroke$source's (remember, the number of the $\TMstroke$source symbol is $3$source, $1$source being the number of $\TMendtape$source and $2$source being the number of $\TMblank$source). At the left end of this sequence of blocks (separated by $\TMblank$source symbols on the tape of $U$source), it writes a single $\TMstroke$source, the code for $\TMendtape$source.

$U$source now has on its tape: the index $e$source, the number $n$source, the code number of the start state (the “current state”), the number of the initial head position $1$source (the “current head position”), and the initial contents of the “tape” (a sequence of blocks of $\TMstroke$source's representing the code numbers of the symbols of $M_e$source---the “symbols”---separated by $\TMblank$source's).

It now simulates what $M_e$source would do if started on input $n$source, by doing the following:

1. Find the number $k$source of the “current head position” (at the beginning, that's $1$source),

2. Move to the $k$sourceth block in the “tape” to see what the “symbol” there is,

3. Find the instruction matching the current “state” and “symbol,”

4. Move back to the $k$sourceth block on the “tape” and replace the “symbol” there with the code number of the symbol $M_e$source would write,

5. Move the head to where it records the current “state” and replace the number there with the number of the new state,

6. Move to the place where it records the “tape position” and erase a $\TMstroke$source or add a $\TMstroke$source (if the instruction says to move left or right, respectively).

7. Repeat.Footnote: We're glossing over some subtle difficulties here. E.g., $U$source 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.

If $M_e$source started on input $n$source never halts, then $U$source also never halts, so its output is undefined.

If in step link to the universal-machine simulation step that finds a matching instruction it turns out that the description of $M_e$source contains no instruction for the current “state”/“symbol” pair, then $M_e$source would halt. If this happens, $U$source erases the part of its tape to the left of the “tape.” For each block of three $\TMstroke$source's (representing a $\TMstroke$source on $M_e$source's tape), it writes a $\TMstroke$source on the left end of its own tape, and successively erases the “tape.” When this is done, $U$source's tape contains a single block of $\TMstroke$source's of length $m$source.

If $U$source encounters something other than a block of three $\TMstroke$source's on the “tape,” it immediately halts. Since $U$source's tape in this case does not contain a single block of $\TMstroke$source's, its output is not a natural number, i.e., $f(e,n)$source is undefined in this case.

Explain

Assume we have fixed some enumeration of Turing machine descriptions. Each Turing machine thus receives an index: its place in the enumeration $M_1$source, $M_2$source, $M_3$source, dots of Turing machine descriptions.

We know that there must be non-Turing-computable functions: the set of Turing machine descriptions---and hence the set of Turing machines---is enumerable, but the set of all functions from $\Nat$source to $\Nat$source is not. But we can find specific examples of non-computable functions as well. One such function is the halting function.

Undecidability definition

[Halting function] The halting function $h$source is defined as

Undecidability definition

[Halting problem] The Halting Problem is the problem of determining (for any $e$source, $n$source) whether the Turing machine $M_e$source halts for an input of $n$source strokes.

Explain

We show that $h$source is not Turing-computable by showing that a related function, $s$source, is not Turing-computable. This proof relies on the fact that anything that can be computed by a Turing machine can be computed by a disciplined Turing machine (link to section Disciplined Machines), and the fact that two Turing machines can be hooked together to create a single machine (link to section Combining Machines).

Undecidability definition

The function $s$source is defined as

Undecidability lemma

The function $s$source is not Turing computable.

Proof

We suppose, for contradiction, that the function $s$source is Turing computable. Then there would be a Turing machine $S$source that computes $s$source. We may assume, without loss of generality, that when $S$source halts, it does so while scanning the first square (i.e., that it is disciplined). This machine can be “hooked up” to another machine $J$source, which halts if it is started on input $0$source (i.e., if it reads $\TMblank$source in the initial state while scanning the square to the right of the end-of-tape symbol), and otherwise wanders off to the right, never halting. $S \concat J$source, the machine created by hooking $S$source to $J$source, is a Turing machine, so it is $M_e$source for some $e$source (i.e., it appears somewhere in the enumeration). Start $M_e$source on an input of $e$source $\TMstroke$sources. There are two possibilities: either $M_e$source halts or it does not halt.

1. Suppose $M_e$source halts for an input of $e$source $\TMstroke$sources. Then $s(e) = 1$source. So $S$source, when started on $e$source, halts with a single $\TMstroke$source as output on the tape. Then $J$source starts with a $\TMstroke$source on the tape. In that case $J$source does not halt. But $M_e$source is the machine $S \concat J$source, so it should do exactly what $S$source followed by $J$source would do (i.e., in this case, wander off to the right and never halt). So $M_e$source cannot halt for an input of $e$source $\TMstroke$source's.

2. Now suppose $M_e$source does not halt for an input of $e$source $\TMstroke$sources. Then $s(e) = 0$source, and $S$source, when started on input $e$source, halts with a blank tape. $J$source, when started on a blank tape, immediately halts. Again, $M_e$source does what $S$source followed by $J$source would do, so $M_e$source must halt for an input of $e$source $\TMstroke$source's.

In each case we arrive at a contradiction with our assumption. This shows there cannot be a Turing machine $S$source: $s$source is not Turing computable.

Undecidability theorem

[Unsolvability of the Halting Problem] The halting problem is unsolvable, i.e., the function $h$source is not Turing computable.

Proof

Suppose $h$source were Turing computable, say, by a Turing machine $H$source. We could use $H$source to build a Turing machine that computes $s$source: First, make a copy of the input (separated by a $\TMblank$source symbol). Then move back to the beginning, and run $H$source. We can clearly make a machine that does the former (see link to exercise asking for a disciplined copier machine), and if $H$source existed, we would be able to “hook it up” to such a copier machine to get a new machine which would determine if $M_e$source halts on input $e$source, i.e., computes $s$source. But we've already shown that no such machine can exist. Hence, $h$source is also not Turing computable.

Unsolved undecidability exercise

The Three Halting (3-Halt) problem is the problem of giving a decision procedure to determine whether or not an arbitrarily chosen Turing Machine halts for an input of three $\TMstroke$source's on an otherwise blank tape. Prove that the 3-Halt problem is unsolvable.

Unsolved undecidability exercise

Show that if the halting problem is solvable for Turing machine and input pairs $M_e$source and $n$source where $e \neq n$source, then it is also solvable for the cases where $e = n$source.

Unsolved undecidability exercise

We proved that the halting problem is unsolvable if the input is a number $e$source, which identifies a Turing machine $M_e$source via an enumeration of all Turing machines. What if we allow the description of Turing machines from link to section Enumerating Turing Machines directly as input? Can there be a Turing machine which decides the halting problem but takes as input descriptions of Turing machines rather than indices? Explain why or why not.

Unsolved undecidability exercise

Show that the partial function $s'$source is defined as

is Turing computable.

Explain

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$source, a predicate symbol $\Obj Q_q$source, and for each tape symbol $\sigma$source, a predicate symbol $\Obj S_\sigma$source. The former allow us to describe the state of $M$source 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$source, and a $1$source-place function $\prime$source, the successor function. By convention it is written after its argument (and we leave out the parentheses).

For each number $n$source there is a canonical term $\num{n}$source, the numeral for $n$source, which represents it in $\Lang L_M$source. $\num{0}$source is $\Obj 0$source, $\num{1}$source is $\Obj 0'$source, $\num{2}$source is $\Obj 0''$source, and so on. More formally:

The term $\num{0}$source, i.e., $\Obj 0$source names the leftmost position on the tape as well as the time before the first execution step (the initial configuration). The term $\num{1}$source, i.e., $\Obj 0'$source 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 $<$source 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)$source, i.e., the sentences which, taken together, describe the behavior of $M$source when run on input $w$source. There will be sentences which lay down conditions on $\Obj 0$source, $\prime$source, and $<$source, sentences that describes the input configuration, and sentences that describe what the configuration of $M$source is after it executes a particular instruction.

Undecidability definition

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

1. A two-place predicate symbol $\Obj Q_q(x, y)$source for every state $q \in Q$source. Intuitively, $\Obj Q_q(\num{m}, \num{n})$source expresses “after $n$source steps, $M$source is in state $q$source scanning the $m$sourceth square.”

2. A two-place predicate symbol $\Obj S_\sigma(x, y)$source for every symbol $\sigma\in \Sigma$source. Intuitively, $\Obj S_\sigma(\num{m}, \num{n})$source expresses “after $n$source steps, the $m$sourceth square contains symbol $\sigma$source.”

3. A constant symbol $\Obj 0$source

4. A one-place function symbol $\prime$source

5. A two-place predicate symbol $<$source

Undecidability proposition

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

Proof

Exercise.

Unsolved undecidability exercise

Prove link to proposition that represented numerals preserve strict order. (Hint: use induction on $k-m$source).

Explain

In order to verify that our representation works, we have to prove two things. First, we have to show that if $M$source halts on input $w$source, then $!T(M, w) \lif !E(M, w)$source is valid. Then, we have to show the converse, i.e., that if $!T(M, w) \lif !E(M, w)$source is valid, then $M$source does in fact eventually halt when run on input $w$source.

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)$source) is valid. The easiest way to do this is to give a derivation. Our proof is supposed to work for all $M$source and $w$source, 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$source and $w$source look like, and however many steps it takes $M$source to halt on input $w$source, there will be a derivation of $!T(M, w) \lif !E(M, w)$source.

Naturally, our induction will proceed on the number of steps $M$source takes before it reaches a halting configuration. In our inductive proof, we'll establish that for each step $n$source of the run of $M$source on input $w$source, $!T(M, w) \Entails !C(M, w, n)$source, where $!C(M, w, n)$source correctly describes the configuration of $M$source run on $w$source after $n$source steps. Now if $M$source halts on input $w$source after, say, $n$source steps, $!C(M, w, n)$source will describe a halting configuration. We'll also show that $!C(M, w, n) \Entails !E(M, w)$source, whenever $!C(M, w, n)$source describes a halting configuration. So, if $M$source halts on input $w$source, then for some $n$source, $M$source will be in a halting configuration after $n$source steps. Hence, $!T(M, w) \Entails !C(M, w, n)$source where $!C(M, w, n)$source describes a halting configuration, and since in that case $!C(M, w, n) \Entails !E(M, w)$source, we get that $!T(M, w) \Entails !E(M, w)$source, i.e., that $\Entails !T(M, w) \lif !E(M, w)$source.

The strategy for the converse is very different. Here we assume that $\Entails !T(M, w) \lif !E(M, w)$source and have to prove that $M$source halts on input $w$source. From the hypothesis we get that $!T(M, w) \Entails !E(M, w)$source, i.e., $!E(M, w)$source is true in every structure in which $!T(M, w)$source is true. So we'll describe a structure $\Struct{M}$source in which $!T(M, w)$source is true: its domain will be $\Nat$source, and the interpretation of all the $\Obj Q_q$source and $\Obj S_\sigma$source will be given by the configurations of $M$source during a run on input $w$source. So, e.g., $\Sat{M}{\Obj Q_q(\num{m}, \num{n})}$source iff $M$source, when run on input $w$source for $n$source steps, is in state $q$source and scanning square $m$source. Now since $!T(M, w) \Entails !E(M, w)$source by hypothesis, and since $\Sat{M}{!T(M, w)}$source by construction, $\Sat{M}{!E(M, w)}$source. But $\Sat{M}{!E(M, w)}$source iff there is some $n \in \Domain{M} = \Nat$source so that $M$source, run on input $w$source, is in a halting configuration after $n$source steps.

Undecidability definition

Let $!C(M, w, n)$source be the sentence

where $q$source is the state of $M$source at time $n$source, $M$source is scanning square $m$source at time $n$source, square $i$source contains symbol $\sigma_i$source at time $n$source for $0 \le i \le k$source and $k$source is the right-most non-blank square of the tape at time $0$source, or the right-most square the tape head has visited after $n$source steps, whichever is greater.

Undecidability lemma

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

Proof

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

1. After $n$source steps, $M$source is in state $q$source scanning square $m$source on which $\sigma$source appears.

2. The transition function $\delta(q, \sigma)$source is undefined.

$!C(M, w, n)$source is the description of this configuration and will include the clauses $\Obj Q_{q}(\num{m}, \num{n})$source and $\Obj S_{\sigma}(\num{m}, \num{n})$source. These clauses together imply $!E(M, w)$source:

since $\Obj Q_{q}(\num{m}, \num{n}) \land \Obj 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}))$source, as $\tuple{q,\sigma} \in X$source.

Explain

So if $M$source halts for input $w$source, then there is some $n$source such that $!C(M, w, n) \Entails !E(M,w)$source. We will now show that for any time $n$source, $!T(M, w) \Entails !C(M, w, n)$source.

Undecidability lemma

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

Proof

Induction basis: If $n = 0$source, then the conjuncts of $!C(M, w, 0)$source are also conjuncts of $!T(M, w)$source, so entailed by it.

Inductive hypothesis: If $M$source has not halted before the $n$sourceth step, then $!T(M,w) \Entails !C(M, w, n)$source. We have to show that (unless $!C(M, w, n)$source describes a halting configuration), $!T(M, w) \Entails !C(M, w, n+1)$source.

Suppose $0 \le n$source and after $n$source steps, $M$source started on $w$source is in state $q$source scanning square $m$source. Since $M$source does not halt after $n$source steps, there must be an instruction of one of the following three forms in the program of $M$source:

1. $\delta(q, \sigma) = \tuple{q', \sigma', \TMright}$source

2. $\delta(q, \sigma) = \tuple{q', \sigma', \TMleft}$source

3. $\delta(q, \sigma) = \tuple{q', \sigma', \TMstay}$source

We will consider each of these three cases in turn.

1. Suppose there is an instruction of the form link to right-move case in the configuration induction. By link to definition of the first-order machine-description languagelink to right-move representation sentence, this means that

   $$& \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}'))]$$source

   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 $\Obj S_{\sigma_m}(\num{m},\num{n}')$source---follows from the corresponding conjunct in $!C(M, w, n)$source together with $!A(\num{m}, \num{n})$source.

   If $m < k$source, $!T(M,w) \Proves \num{m} < \num {k}$source (link to proposition that represented numerals preserve strict order) and by transitivity of $<$source, we have $\lforall[x][(\num{k} < x \lif \num{m} < x)]$source. If $m = k$source, then $\lforall[x][(\num{k} < x \lif \num{m} < x)]$source by logic alone. The last line then follows from the corresponding conjunct in $!C(M, w, n)$source, $\lforall[x][(\num{k} < x \lif \num{m} < x)]$source, and $!A(\num{m}, \num{n})$source. If $m<k$source, this already is $!C(M, w, n+1)$source.

   Now suppose $m=k$source. In that case, after $n+1$source steps, the tape head has also visited square $k+1$source, which now is the right-most square visited. So $!C(M, w, n+1)$source has a new conjunct, $\Obj S_\TMblank(\num{k}',\num{n}')$source, and the last conjunct is $\lforall[x][(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))]$source. 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}'))]$source. In particular, this gives us $\num{k} < \num{k}' \lif \Obj S_\TMblank(\num{k}', \num{n}')$source. From the axiom $\lforall[x][x < x']$source we get $\num{k} < \num{k}'$source. By modus ponens, $\Obj S_\TMblank(\num{k}',\num{n}')$source follows.

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

2. Suppose there is an instruction of the form link to left-move case in the configuration induction. Then, by link to definition of the first-order machine-description languagelink to left-move representation sentence,

   $$& \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}'))]$$source

   as before. (Note that in the first case, $\num{l}' \ident \num{l+1} \ident \num{m}$source and in the second case $\num{l} \ident \num{0}$source.) But this just is $!C(M, w, n+1)$source.

3. Case link to stay-put case in the configuration induction is left as an exercise.