Hilbert’s famous “Decision problem” (“Entscheidungsproblem” in German) was to establish whether it is in principle possible to find an effectively computable decision procedure which can infallibly, and in a finite time, reveal whether or not any given proposition P is provable from a given set of axioms and rules (in particular, a set of axioms and rules designed to capture arithmetical truths). An “effectively computable” procedure is supposed to be one that can be performed by systematic application of clearly specified rules, without requiring any inspirational leaps or spontaneous intellectual insights. So if such a decision procedure could be discovered, this would mean that the provability (or otherwise) of any arithmetical proposition could be determined mechanically, by an appropriate computing machine. For rigorous consideration of this issue, however, vague notions of “effective computability” are not enough – how exactly are we to specify what counts as a “systematic” or “mechanical” procedure, as opposed to one that is inspirational or spontaneous? Turing’s answer was to design a kind of machine with a very precise and limited repertoire of operations, but which is capable – if suitably instructed – of carrying out a vast range of possible computations.