The paper and its dates
Alan M. Turing’s paper appeared in the Proceedings of the London Mathematical Society, second series, volume 42, pages 230–265. Its opening page records receipt on 28 May 1936 and presentation on 12 November 1936. The volume is conventionally cited as 1936–1937. Receipt, presentation, and bibliographic publication dates should therefore not be treated as interchangeable.
A separate correction occupies pages 544–546 of volume 43. Often cited as the 1937 correction, it is labelled 1938 in the publisher’s current metadata. Retaining that distinction is more accurate than assigning an unsupported single publication day to both documents.
Making computation explicit
The starting point is the generation of a number’s digits by a finite procedure. Turing analyzes rule-following computation and gives it a precise mechanical representation: finitely many internal states, a tape divided into squares, and elementary operations on the symbols being scanned. An automatic machine’s next action follows from its state and the scanned symbol rather than an additional judgment by an operator.
A machine’s rules can themselves be encoded as a finite description. Turing’s universal machine takes such a description as data and simulates the described computation. This is universality within a mathematical model, not a claim that an actual device possesses unlimited storage or can solve every mathematical question.
The undecidability argument
An important original distinction concerns machines that continue producing output digits indefinitely. Turing calls these circle-free. A machine can run forever while producing only finitely many digits, so circle-freeness is not simply the modern condition of nontermination. His argument rules out a general procedure that correctly classifies arbitrary machine descriptions in the required way.
The application to the Entscheidungsproblem connects machine behavior with provability in a logical calculus. A hypothetical procedure deciding whether every such formula is provable would also decide whether an associated machine ever prints a specified symbol. The latter decision procedure is unavailable, so the proposed general logical procedure cannot exist. The limitation concerns an algorithm answering correctly for all inputs; it does not imply that every individual instance is insoluble or merely expensive to compute.
Correction and significance
The correction acknowledges Paul Bernays for identifying formal errors, repairs the logical encoding used in the proof, and discusses difficulties arising from representations of real numbers. It does not reverse the conclusion that the general decision problem is unsolvable.
The paper’s lasting contribution combines a concrete account of mechanical calculation with a proof of its limitations. It belongs alongside Church’s independent work, rather than replacing that history with a single-inventor story. Its mathematical results must also be distinguished from stronger claims about what every physical system or human mind can do.