Systems of Logic Based on Ordinals

Turing argues that Gödel's incompleteness theorem, while showing every formal system to be incomplete, also indicates a constructive path beyond each system's limits: from a logic L, one can form a stronger logic L′ by adding statements—such as consistency—that ought to be accepted but are not derivable in L. By iterating this process along constructive ordinals, one obtains a transfinite sequence of logics, each more complete than its predecessors. The paper rejects the fatalistic reading of Gödel as a terminal limit on formalization. Turing's aim is to determine whether such a sequence is complete in the sense that every number-theoretic problem is solvable by some ordinal-indexed logic, and he obtains a striking but equivocal partial completeness result .

An ordinal logic is a systematic assignment of a formal system to each constructive ordinal notation, built by iterating the adjunction of a consistency statement (or similar Gödelian 'ought') at successor stages and taking unions at limit stages. Turing constructs a particular ordinal logic, often denoted S*, by iterating consistency statements. The construction is technically demanding because it requires a notation system for ordinals that is itself effective. Feferman notes that Turing's presentation in the λ-calculus made the paper notoriously difficult, and it was only when Feferman translated the work into conventional recursive function theory around twenty years later that it began to be properly evaluated . The framework influenced later work on autonomous progressions and characterizations of predicative proof .

Turing introduced oracle machines in section 4 of the paper, almost incidentally, to produce an arithmetical problem that is not 'number-theoretical' in his technical sense. He asked readers to imagine an unspecified means of solving number-theoretic problems—'a kind of oracle'—and defined an o-machine as one with access to this oracle as a fundamental process. He then showed that the halting problem for o-machines is not solvable even by the oracle itself . Turing did nothing further with the idea, but Emil Post took it up in 1944 as the basis for a theory of degrees of unsolvability, crediting Turing with the result that for any set of natural numbers there is another of higher degree. This transformed computability from an absolute notion into a relative one, inaugurating the field of relative computability .

The paper's reception was limited for several reasons. It was formulated in the λ-calculus, at what Feferman suspects was Church's behest, making the expressions for ordinals and formal systems extremely difficult to decipher . Turing's name was already established through his 1936 work on computability, but the ordinal logics paper addressed a narrower technical problem and did not announce a dramatic new concept like the universal machine. It was only when Feferman translated the work into conventional recursive function theory around twenty years later that its results began to be properly evaluated and appreciated . Even now, Feferman notes, the paper 'is still not widely understood and appreciated' . The 2012 Princeton University Press edition of the thesis, edited by Andrew Appel with Feferman's commentary, has made it more accessible .

The 1939 paper extends the 1936 analysis in a new direction. In 'On Computable Numbers,' Turing had defined the absolute limits of mechanical computability through the universal machine. The ordinal logics paper takes up the question of what happens after those limits are reached: how can formal systems be strengthened systematically, and can the process be extended into the transfinite? The oracle machine concept, introduced here, generalizes the 1936 machine by relativizing computation to an external source, thereby opening the space of relative computability that the 1936 paper had left closed. The thesis thus complements the earlier work: where the 1936 paper mapped the boundary of the computable, the 1939 paper explores the structured landscape beyond it.

A common misconception treats Turing's partial completeness result as a full solution to the problem of overcoming Gödelian incompleteness. It is not. Turing obtained a striking but equivocal result: for a certain class of 'number-theoretical' problems (those in ∀∃ form), he showed that some ordinal-indexed logic in his sequence decides them, but only under conditions that do not guarantee invariance across different notations for the same ordinal. Feferman calls the completeness results 'equivocal' for this reason . Turing himself did not continue the line of research, and the problem of finding a canonical, invariant ordinal logic remained open. The paper's lasting value lies less in its completeness theorem than in the framework it established and the oracle concept it introduced.

Turing's motivation for ordinal logics is partly philosophical. He wants to distinguish clearly between steps in a proof that are purely formal and steps that rely on intuition—specifically, the intuitive recognition that a given expression is a notation for an ordinal. As he puts it, when we have an ordinal logic, 'we are in a position to prove number-theoretic theorems by the intuitive steps of recognizing [natural numbers as notations for ordinals]' . The logic must be constructed so that it leads to correct results whenever those intuitive steps are correct. This concern with isolating and disciplining intuition connects the paper to Turing's broader interest in the foundations of mathematical reasoning, and it anticipates later debates about the role of human insight in proof.