Systems of Logic Based on Ordinals†

TL;DR. In his 1939 Princeton thesis, Turing proposed a way to outrun Gödel: whenever a formal system hits an unprovable truth, add a new axiom asserting its own consistency, and iterate — transfinitely, along the ordinals. He proved this works surprisingly well, but only if something non-mechanical ("intuition") keeps choosing the right next step, while everything else ("ingenuity") stays mechanical and checkable. The same paper invented oracle machines in a single throwaway section. Eighty-seven years later, the intuition/ingenuity split is precisely the LLM-generator-plus-Lean-verifier architecture — yet nobody has built the actual loop Turing described: a system that grows its own trusted axiomatic base round after round. Every ingredient now exists.

The paper: climbing out of Gödel's hole one axiom at a time

The context is 1938–39, Turing working under Church at Princeton, three years after "On Computable Numbers." Gödel's second incompleteness theorem says any consistent, effectively axiomatized theory T containing arithmetic cannot prove its own consistency statement \mathrm{Con}(T) — a true sentence, if T is sound. Everyone treated this as a wall. Turing treated it as a staircase.

If T_0 (say, Peano arithmetic) can't prove \mathrm{Con}(T_0), define T_1 = T_0 + \mathrm{Con}(T_0). That's a strictly stronger sound theory — which has its own unprovable \mathrm{Con}(T_1), so define T_2, and so on. At stage \omega take the union of everything so far; then keep going: T_{\omega+1}, T_{\omega+2}, \ldots through the constructive ordinals. Turing called the resulting object an ordinal logic.

His main theorem is startling: this progression is complete for true \Pi_1 sentences (statements of the form "for all n, the computation f(n) halts with output 0" — Goldbach and Riemann are in or near this class). Every true \Pi_1 sentence becomes provable somewhere in the tower, and in fact by stage \omega+1.

Then comes the honest part, and it's the heart of the paper. The catch is that ordinals must be handed to the machine as notations — programs coding well-orderings — and deciding whether a given notation really denotes an ordinal is not just undecidable but \Pi^1_1-complete: far beyond anything arithmetic, let alone computable. Turing's completeness proof works by smuggling the truth of the target sentence into the choice of notation. The tower doesn't mechanize mathematical truth; it relocates all the non-mechanizable content into one repeated act: choosing, and trusting, the next step up.

Turing named the two faculties explicitly: ingenuity — constructing derivations inside a fixed system, in principle mechanizable — and intuition — the judgments no fixed system can derive, paradigmatically "this system is sound, so its consistency statement is true." His stated goal (paraphrasing; the passage is in section 11) was not to eliminate intuition but to confine it to specific, isolated steps, with everything downstream mechanically checkable.

Almost as an aside, section 4 introduces the o-machine: a Turing machine with a black box answering questions no machine can answer. One paragraph. It founded relative computability, Turing degrees via Post's 1944 work, and — conceptually — every architecture in which a mechanical process consults something outside itself.

Why it stayed pure logic

In 1939 there was no computer. Not a slow one — none. The first stored-program machine ran in Manchester in 1948; the first automated theorem provers (Logic Theorist, Davis's Presburger prover) appeared around 1954–56; proof assistants that could check real mathematics arrived with Automath (~1968) and LCF (~1972). Turing's "ingenuity" half had no substrate for decades.

The "intuition" half was worse: there was no candidate mechanism at all. Intuition in Turing's sense is a fallible, non-derivable judgment about which extension of your foundations is sound and worth making. Nothing before large-scale statistical models of mathematical text could even pretend to play that role. Learned premise selection appeared around 2016 (DeepMath); language-model provers around 2020 (GPT-f).

And even with machines, the economics of formal verification were prohibitive until very recently. Gonthier's team took roughly six years and on the order of 170,000 lines of Coq to formalize the Feit–Thompson theorem (finished 2012). A loop that mints thousands of verified lemmas per day was science fiction until about 2022.

What changed

The generator–verifier decomposition that dominates AI-for-math today is Turing's split, implemented:

• Ingenuity is now fully mechanical and cheap: Lean's kernel checks proofs at machine speed against a trusted base of roughly 1.5 million lines (mathlib); Isabelle's AFP is several million lines more. Proof search — tactics, hammers, tree search — is ingenuity too, and it scales with compute.
• Intuition is now approximated statistically: an LLM proposes lemmas, proof sketches, definitions, and formalizations of informal statements. Crucially, in the good systems the intuition is never trusted — its output must pass the kernel before it counts. AlphaProof (2024) solved four of six IMO problems this way; DeepSeek-Prover and successors run reinforcement learning where the only reward signal is "the kernel accepted it," so the model trains on a growing corpus of self-generated, machine-certified mathematics.

That last clause is the quiet arrival of Turing's progression: verified output at round t becomes the trusted substrate for round t+1. But today's loops grow only the theorem library, never the axiomatic base. They climb within T_0. Turing's tower climbs through theories.

A 2026 revival: the progression as an engineering loop

Here is the experiment the paper is asking for. Keep Turing's architecture exactly; replace his unspecified "intuition" with a learned model, and his unbuilt "ingenuity" with Lean.

1. Base. L_0 = Lean + mathlib over a fixed foundation.
2. Conjecture (intuition). The model proposes three kinds of objects: new lemmas, new definitions (concept formation — arguably the harder half of intuition), and, rarely, new base extensions: reflection principles ("everything L_t proves about numbers is true"), consistency statements, or stronger axioms.
3. Certify (ingenuity). Proof search + kernel check. Lemmas and definitions that verify enter L_{t+1}. Base extensions can't be verified — that's Gödel — so they enter a separately tagged layer: theorems are marked with the exact extension they depend on, and the whole corpus stays stratified, exactly like large-cardinal hypotheses in set theory. For sound bases, adding a reflection principle is safe; soundness is precisely the judgment that can't be discharged mechanically. Turing tells you where the irreducible risk lives; the engineering keeps it labeled and quarantined.
4. Close the loop. L_{t+1} becomes retrieval context and RL training data. Measure whether stratified base-growth ever pays: are there natural theorems reached dramatically faster (or at all) with the extension layer? Proof-theoretic speed-up results say the accelerations can be enormous in principle; nobody has measured them in a learned system.

The failure mode Turing's own logic predicts: Feferman (1962) extended the progression with uniform reflection and showed completeness for all true arithmetic sentences along suitable paths — but Feferman–Spector (1962) showed other paths through the ordinal notations yield progressions that miss almost everything. Path quality is everything, and path quality is exactly what the learned intuition must supply. Whether an LLM trained on human mathematics carries a usable prior over "which extensions are sound and fruitful" is a genuinely open empirical question — arguably the question the revival would answer.

Verdict: partly vindicated, core untested

Vindicated: oracle machines became the backbone of computability theory and, loosely, of every tool-augmented AI system. The intuition/ingenuity split is now standard engineering practice under other names (generator/verifier, proposer/checker), and the "train only on kernel-certified outputs" loop is producing real results. Kreisel, Feferman, and later Franzén developed the logic of ordinal progressions thoroughly; Feferman's analysis of exactly where Turing's completeness proof cheats is the definitive post-mortem.

Untested: the self-extending part. No deployed system proposes and adopts new axioms, definitions-as-foundations, or reflection principles as part of its learning loop. Concept formation — Turing's intuition applied to definitions, not just proofs — is barely touched; today's provers mostly manipulate concepts humans already formalized. And nobody knows whether transfinite-style base extension buys practical proving power or only proof-theoretic curiosities. That's a clean, well-posed, currently unclaimed experiment.

Where to read it

The paper is at doi.org/10.1112/plms/s2-45.1.161 (PLMS s2-45, 1939; bibliographic details verified). It's long and the notation is pre-modern; read sections 4 (oracle machines), 9 (the completeness theorem), and 11 (intuition vs. ingenuity) first. Alongside it: Feferman's "Transfinite recursive progressions of axiomatic theories" (JSL 1962) and his essay "Turing in the Land of O(z)" for the definitive analysis of what the ordinal logics do and don't achieve; Torkel Franzén's Inexhaustibility for a readable book-length treatment; and, for the modern half, the AlphaProof announcement and the DeepSeek-Prover papers — which are running Turing's inner loop without, so far, citing the man who drew it.