Turing's Cathedral: The Origins of the Digital Universe

by George Dyson

David Hilbert, whose ambitious program of formalization set the course for mathematics between World War I and World War II. The Hilbert school believed that if a proposition could be articulated within the language of mathematics, then either its proof or its refutation could be reached, by logic alone, without any intervening leaps of faith. In 1928, Hilbert posed three questions by which to determine whether an all-encompassing mathematical universe could be defined by a finitary set of rules: Are these foundations consistent (so that a statement and its contradiction cannot ever both be proved)? Are they complete (so that all true statements can be proved within the system itself)? Does there exist a decision procedure that, given any statement expressed in the given language, will always produce either a finite proof of that statement or else a definite construction that refutes it, but never both?