The Gödel completeness theorem for first-order logic entails that P is a first-order consequence of a first-order theory T if and only if P can be deduced from T by first-order logic.
Taking P as the conclusion of the given computation/deduction and T as the premises of this deduction, the completeness theorem yields that there is a first-order deduction of P from T.
This coding takes two steps: firstly, Gödel shows that syntactic relations of a formal theory (such as "x is a proof of y") can be defined by a recursive relation, where "recursivity" is a condition codified by Hilbert and Ackermann to capture finite stepwise definition; secondly, he shows that every recursively-defined relation can be expressed by an arithmetic relation (in this volume, Martin Davis's article presents a proof of this second step that Davis judges more direct than Gödel's).
Gödel recognized that the generality of his results depended upon the details of this coding, since its applicability to other formal theories requires a correspondingly general means of mechanizing syntactic derivation.
Saul Kripke's article contends that the Church-Turing thesis is provable, arguing in a way he says resembles arguments given by Turing and Church.
In particular, Kripke wants to prove that every intuitively computable function is recursive.Kripke holds that even if his thesis is only understood as a reduction of Church's thesis to Hilbert's thesis, he has amplified the Church-Turing thesis in a substantive way.Stewart Shapiro's article makes the case, in contrast to Kripke's, that the Church-Turing thesis cannot be proved.He was unsure that recursivity provided such a means.In the years after 1931 Gödel would seize instead upon Turing's analysis of computability, published in 1936, as providing this generality.Many have wondered whether this thesis is mathematically provable, or whether it is too imprecise to admit of mathematical proof.This question is the subject of two of this volume's articles, to which we now turn.The cogency of this argument comes down, of course, to whether one accepts Hilbert's thesis.One might hold that an informal deduction cannot be expressed in a first-order way, since informal notions are too rich for their meanings to be settled by any single finite expression.Shapiro continues by arguing that the notion of informal computability at issue in the Church-Turing thesis is subject to open texture in this way.He recounts the sharpenings of computability during the twentieth century, noting that there were other options along the way, other idealizations of computation, that could have been chosen (such as computable in polynomial time or space).