By the completeness theorem, there is a formal derivation of the conclusion of A from its premises

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