definitions.tex

\subsection{Symbols}
The Turing machine 

\begin{itemize}
\item $\Delta$ is a finite set of sentences that describe the operation of the Turing machine.
\item $n$ is a number, the input to the Turing machine.
\item $H$ is a sentence such that $\Delta\vdash H\iff$ the machine does eventually halt when given input $n$.
\item $\mathscr{I}$ is an interpretation for $H$ and the sentences in $\Delta$. The variables range over the integers, and it uses the following definitions:
\begin{itemize}
\renewcommand{\labelitemii}{\textopenbullet}
\item $Q_i$ for $0 \le i \le k$ is a binary predicate.\\
$t Q_i x \iff $ at time $t$ the machine is in state $q_i$, scanning square number $x$.
\item $S_j$ for $0\le j\le r$ is a binary predicate.\\
$t S_j x \iff $ at time $t$ the machine is scanning the symbol $S_j$, scanning square number $x$.
\item $<$ is the standard less-than binary predicate.
\item $\z$ is the standard zero constant.
\item $'$ is the standard successor function (even when applied to negatives).
\end{itemize}
\end{itemize}

If we could solve the decision problem for validity of sentences we could determine whether the machine eventually halts, because (given the finite sequence of sentences $\delta_1,\dots,\delta_m \in \Delta$)
\[\Delta\vdash H\iff (\delta_1\land \delta_2\land \cdots \delta_m)\vdash H \iff \vdash (\delta_1 \land  \delta_2 \land  \cdots\delta_m) \rightarrow H\]
If we could prove that $\Delta\vdash H \iff $ the Turing machine halts on input $n$, we would have
\[(\delta_1 \land  \delta_2 \land  \cdots\delta_m) \rightarrow H\text{ is valid }\iff \Delta\vdash H \iff \text{ the Turing machine halts on input }n\]
So validity is tied up with the Halting problem.

\subsection{Construction}
The squares of the tape are numbered by integers, and moments of time are integers. Each moment in time is a single step in the Turing machine. The machine begins at time $t=0$ in square $x=0$ and stops when the machine halts. If $t<0$ or $t>$ the halting time, $tQ_ix \mapsto 0$ and $tS_jx\mapsto 0$.

\noindent Rule: \igEdge{q_i}{S_j:S_k}{q_m}.
\begin{equation}\label{writeTapeEdge}
\forall t\forall x\forall y \{[tQ_ix\land  tS_jx] \rightarrow [t'Q_mx\land  t'S_kx \land  (y\ne x \rightarrow (tS_0y\rightarrow t'S_0y)\land \dots\land (tS_ry\rightarrow t'S_ry))]\}
\end{equation}
Rule: \igEdge{q_i}{S_j:R}{q_m}
\begin{equation}
\forall t\forall x\forall y\{[tQ_ix\land tS_jx]\rightarrow [t'Q_mx' \land  (tS_0y\rightarrow t'S_0y)\land \dots\land (tS_ry\rightarrow t'S_ry)]\}
\end{equation}
Rule: \igEdge{q_i}{S_j:L}{q_m}
\begin{equation}
\forall t \forall x \forall y \{[tQ_ix' \land  tS_jx']\rightarrow [t'Q_mx\land  (tS_0y\rightarrow t'S_0y)\land \dots\land (tS_ry\rightarrow t'S_ry)]\}
\end{equation}
Starting condition:
\begin{equation}
\label{descOfZero}
\z Q_1 \z\ \land \ \z S_1\z\ \land \ \z S_1\z '\ \land \dots\land \ \z S_1\z^{(n-1)}\ \land \ \forall y [(y\ne \z\ \land \ y\ne \z'\ \land \dots\land \ y\ne \z^{(n-1)}) \rightarrow \z S_0y]
\end{equation}
Now we provide basic sentences to deal with integers:
\begin{itemize}
\item This sentence says that each integer is the successor of exactly one integer:
\begin{equation}\label{successorOfOneOther}
\forall z\exists x z = x'\ \land  \ \forall z\forall x\forall y (z=x'\land z=y'\rightarrow x=y)
\end{equation}
\item This sentence says that if $p,q\in\N$ and $p\ne q$, then $\forall x x^{(p)}\ne x^{(q)}$ is implied by $\Delta$. All such sentences are consequences of the following:
\begin{equation}\label{additionWorks}
\forall x\forall y\forall z (x < y\ \land \ y < z\rightarrow x<z)\ \land \ \forall x\forall y(x'=y\rightarrow x<y)\ \land \ \forall x\forall y(x<y\rightarrow x\ne y)
\end{equation}
\end{itemize}

Define $H$ as the disjunction of all sentences $\exists t\exists x (tQ_i x\ \land \ tS_jx)$ \textbf{such that there is no entry for $q_i$, $S_j$ in the table of our machine}. If there is always an entry for every $q_i$, $S_j$, then the machine never halts and we take $H$ to be some sentence that is false in $\mathscr{I}$, like $\z\ne \z$.