Ordinal Logics and Gödel Sentences

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.

1. S₀ ≝ PA
2. S_α + 1 ≝ S_α + G_Sα
3. 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 Π₁ 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 Π₁ sentence, f(n) = n_O for all n and we select all the first ω Gödel sentences. If we used a false Π₁ 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 Π₁ 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 Π₁ 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.