Proof and algorithm formalizations

Question

Proofs and algorithms are a bit different. Predicate logic provides a formalization of 'proof' and Turing machine provides a formalization of 'algorithm'. Is there an easy reference on formally going from one to the other, e.g., on equivalently defining algorithm by predicate logic?

Answer 1

In a sense, yes - namely, Kleene's $T$ predicate. There is however a subtlety here: this doesn't work in a vacuum, but rather needs to be considered over a theory: we only work with the $T$-predicate in the context of a sufficiently strong theory of arithmetic (it doesn't need to be very strong at all, though - Peano arithmetic is galactic overkill). Such a theory of arithmetic proves the recursion theorem, the unsolvability of the halting problem, the Friedberg-Muchnik theorem, etc. when phrased appropriately in terms of the $T$-predicate.

The question of exactly what "base theory" is needed to prove various facts about computations is called reverse recursion theory. For example, the existence of a maximal c.e. set is strictly harder to prove than the existence of a c.e. set of Turing degree strictly between ${\bf 0}$ and ${\bf 0'}$: the latter is provable in the very weak theory $I\Sigma_1$, which is generally considered the weakest appropriate theory (or close to it anyways), while the former is not (it takes something between $B\Sigma_2$ and $I\Sigma_2$, each of which are stronger systems: in general $I\Sigma_n<B\Sigma_{n+1}<I\Sigma_{n+1}$).