Hilbert's 2nd Problem

Big thing about Turing Machine: its computation is local. That is the reason Turing Machine is more oftenly used in our proofs than things like ``Java''.

Hilbert's 2nd Problem: Axiomatize number theory.

Theorem 7   There doesn't exist a finite collection or Axioms $A$ such that

$$\{S\mid A \vdash S\} = \{ S \mid N \models S\}$$

$N$ is the Standard model of natural numbers with $=,<,\ldots, +, \times, -, / \ldots$.

Proof. Assume to reach a contradiction that such an $A$ exists. Show how to get an algorithm for $\mathrm{HALT}$. Intuition: $\mathrm{HALT}\leq \mathrm{Theoremhood}$.

Consider the program for Halting Problem. Read program $P$, input $I$. Here we use $S = f(P, I)$, so that $S =\exists w, \alpha(w)$¹⁵. If $S$ is a theorem then output ``$P$ halts on $I$''. Else, output ``$P$ doesn't halt on $I$''. Since $A$ exists, to do this, do BFS search on the tree, we can find the proof of $S$ or $\neg S$ in finite steps.

Then, come to our implementation of $f$.

Start: p, q, h=halt symbols: 0, 1, $\sqcup$

$$(p, 0) \rightarrow (q, 0, right)$$

$$(p, 1) \rightarrow (p, 1, right)$$

$$(q, 0) \rightarrow (p, 0, left)$$

$$(q, 1) \rightarrow (p, right)$$

$$(p, \sqcup ) \rightarrow (h, \sqcup , stay)$$

$$(q, \sqcup ) \rightarrow (h, \sqcup , stay)$$

Input: $0110\sqcup \sqcup \sqcup$

Computation History: $\char93 p0110\char93 0q110\char93 01p10\char93 011p0\char93 0110q\sqcup \char93 0110h\sqcup \char93$.

Take $0=0,1=1,p=2,q=3,h=4,\sqcup =5,\char93 =6$, treat the whole computation history as a decimal number. The last state in the computation history should be $h$. That is, $\exists x, (w \mod 10^x)/10^{x-1} = 4\textrm{ and not } \exists y, y < x, (w \... ...xtrm{ or }(w \mod 10^y)/(10^{y-1}) = 2\textrm{ or }(w \mod 10^y)/(10^{y-1}) = 3$. Similarly, other rules can be put here, and $\alpha$ is to confirm that $w$ represents a valid computation history.

To conclude, if we can axiomize $N$, there will be an algorithm solving $\mathrm{HALT}$, and thus such an axiomization system cannot exist. $\qedsymbol$