It would be no exaggeration to say that computation changed the world in the twentieth century.Implicated in nearly all contemporary technology, today's computers empower so-called "intelligent systems" to negotiate the world of human reasoners, even driving cars.
Such a view seems to have been part of Brouwer's belief that mathematical thought is essentially unformalizable.
One might instead maintain the need for higher-order logic to formalize adequately the concepts and inferences of branches of mathematics that implicate the infinite, such as real analysis.
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.
A reader of this volume will acquire a broad acquaintance with the history of the theory of computation in the twentieth century, and with ways in which this theory will continue to develop in the twenty-first century.
At the heart of the twentieth-century revolution of computation are Gödel's incompleteness theorems of 1931, which assert the existence of arithmetic sentences that are true in the standard natural numbers but unprovable in any formalized axiomatic theory of those natural numbers.
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.
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.