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 + GPA. 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. S0 ≝ PA
  2. Sα + 1 ≝ Sα + GSα
  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 GSα 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 Sa 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:

f(n) ≝ if φ(n) then nO else [some important, recursive, technical stuff]

One then uses this function to select a set of GSn’s to create a list of axioms. Since we have picked a true Π1 sentence, f(n) = nO 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 GSω 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.


Russell O’Connor: contact me