Suppose we have a program \(\mathbf{H}(p, x)\) that solves the
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. Essentially, the halting function \(\mathbf{H}\) automatically performs the process of mathematical induction.
When \(A(n)\) is sufficiently simple, for instance \(n \leq 2^n\), we can just perform the induction manually, 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 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, termbyterm, the Collatz sequence of a number. By employing a few dumb tricks, a computer with superTuring capabilities could prove almost any theorem over the natural numbers, including many that have stumped the best of us for centuries.
I think this is a pretty strong argument in favor of the ChurchTuring thesis,^{1} which states that a function that Turing machines cannot compute cannot be evaluated by any method whatsoever. That is to say, the function \(\mathbf{H}\) cannot be physically instantiated, because the universe does not allow it.

Technically, this is the converse of the CTT; see the Stanford philosophy page ↩︎