 and he assumes that the proof relation is recursive and hence that the provability relation is semirecursive. Thus, the argument runs as follows: (1) Let \(A\) be a valid mathematical argument that is a calculation, “where one is computing a function (say, in the language of arithmetic)”. Then, (2) by Hilbert’s thesis, the steps of \(A\) can be stated in a first order language (and so the premises and conclusion of \(A\) can be stated in such a language). But then (3) by the completeness theorem, there is a formal derivation of the conclusion of \(A\)—the final result of the calculation—from its premises, and so (4) “it immediately follows” that the function representing the calculation is recursive. This is a proof of Church’s thesis, assuming Hilbert’s, and, as Kripke mentions, it might therefore be viewed alternatively as a reduction of Church’s thesis to Hilbert’s.