Today I finally read Feferman’s “Turing in the Land of O(z)” I was hoping for an explanation of recursive ordinals, but was instead given history of Turing’s work on ordinal logics.

There is an idea that one can take an axiom system such as PA, and add to it it’s Gödel statement to get PA + G_{PA}. Then one can repeat this process again and again. One can even do this an infinite number of times, by taking a union of all these axioms. One can repeat this process again, all the way through the recursive ordinals.

More formally, one defines the following sequence of axiom systems for recursive ordinals.

`S`_{0}≝ PA`S`_{α + 1}≝`S`_{α}+ G_{Sα}`S`_{λ}≝ ∼{S_{α}|`α`<`λ`} for`λ`a limit ordinal.

Unfortunately the reality isn’t so pretty. A funny thing happens at *ω* + 1. Constructing the Gödel sentence G_{Sα} requires one to find a formula to represent the axiom system `S`_{α}. The usual way of generating the formula is based on the Turing machine that decides the axioms system `S`_{α}. So the Gödel sentence could depend on the particular Turing machine representing `S`_{α}.

So the definition of `S`_{α} above doesn’t actually make sense. Instead one must define `S`_{a} for *ordinal notations* `a`. But does the resulting system depend on which ordinal notation we use?

In fact, it does depend on the particular notation. It is so bad that for any true Π_{1} sentence, ∀`x`.`φ`(`x`), there exists a way of creating a `S`_{ω + 1} such that
`S`_{ω + 1} ⊦ ∀`x`.`φ`(`x`).
One does this by creating a Turing machine that computes:

One then uses this function to select a set of G_{Sn}’s to create a list of axioms. Since we have picked a true Π_{1} sentence, `f`(`n`) = `n`_{O} for all `n` and we select all the first *ω* Gödel sentences. If we used a false Π_{1} sentence the technical stuff would create a inconsistent system. Another consequence of the technical stuff is that it creates a G_{Sω} such that
`S`_{ω + 1} ⊦ ∀`x`.`φ`(`x`). Suppose the Π_{1} sentence weren’t true. Then, because of the techinical stuff, `S`_{ω} would be inconsistent. But `S`_{ω + 1} assumes that `S`_{ω} is consistent. So
`S`_{ω + 1} ⊦ ∀`x`.`φ`(`x`). I haven’t given all the details here, but the idea is that we can encode the fact that the Π_{1} sentence is true into our presentation of the axiom system `S`_{ω}.

I may have made some errors here; feel free to correct me. I believe the general idea is correct.

Turing seems suggests, from the rest of his work, finding strong, sound deduction systems boils down to deciding if a given Turing machine represents an ordinal or not; something that is undecidable. Something that must be taken on faith.