![[saitama.jpg]] Suppose we have a program $\mathbf{H}(p, x)$ that solves the [halting problem](https://en.wikipedia.org/wiki/Halting_problem) for any program $p$ evaluated on input $x$, returning $\mathrm{True}$ if the program halts and $\mathrm{False}$ otherwise. Consider statements of the form $\forall n \in \mathbb{N}: A(n)$, where $A$ is some proposition that can be easily evaluated for any particular natural number. Let $p(A)$ be the following program: ``` i = 1 loop forever: if not A(i): return i += 1 ``` Then the evaluation of $\neg\mathbf{H}(p, A)$ constitutes a proof of the truth or falsehood of the statement $A$ for all natural numbers, if the evaluation of $A(n)$ is guaranteed to halt. When $A(n)$ is sufficiently simple, for instance $n \leq 2^n$, we can just prove this manually via induction, and there's no reason to invoke the halting function $\mathbf{H}$. But what if checking $A(n)$ involves a procedure that may not halt? Let's try to apply the method to Fermat's Last Theorem: $\forall n > 2, \forall a, b, c \in \mathbb{Z} : a^n + b^n \neq c^n$ First, we have find out how to evaluate the statement for any given $n$. Let $\mathbb{Z}^3$ be the countably infinite set of triples of integers, and let $I(n):\mathbb{N} \rightarrow \mathbb{Z}^3$ be an enumeration of the set of triples. Let $A(n)$ be the following procedure: ``` j = 1 loop forever: x, y, z = I(j) if x^n + y^n == z^n: return False j += 1 return True // never executed ``` This procedure halts only if it finds a counterexample for a particular value of $n$. Suppose we try to apply the program $p$ that we defined above. If the condition $x^n + y^n = z^n$ is not true for any integers given a particular value of $n$, $A(n)$ doesn't halt, so $p$ (which invokes $A$) also fails to halt. For example, if $A(3)$ does not halt, the values $n > 3$ are never checked. Then the value of $\neg \mathbf{H}(p, A)$ is equivalent to $\exists n \in \mathbb{N}: A(n)$ rather than the desired $\forall n \in \mathbb{N}: A(n)$. As it turns out, we can solve this by invoking $\mathbf{H}$ again. Take a look at the following program, $q(A)$: ``` i = 3 // because the theorem says n > 2 loop forever: if H(A, i): return i += 1 ``` Instead of using a Boolean return value, we can define $A$ such that it halts if and only if the statement is false, and use the power of $\mathbf{H}$ to immediately check an infinity of cases. Now, the expression $\neg \mathbf{H}(q, A)$ constitutes a proof (or disproof) of Fermat's Last Theorem. A similar argument can be used for many difficult problems over the natural numbers; for instance, the Collatz conjecture can be solved by constructing $A$ to evaluate, term-by-term, the Collatz sequence of a number. By employing a few dumb tricks, a computer with super-Turing capabilities could prove almost any theorem over the natural numbers, including many that have stumped the best of us for centuries.