Long time no blog. Sorry, been busy planning my 2006 world tour. Dates will be announced shortly.
While you’re waiting, there’s a neat little piece of metamathematics that should be more widely known than it is. You all know that if T is a consistent theory satisfying the usual assumptions, then Con(T) is undecidable in T. So T + Con(T) is properly stronger than T, and itself consistent and satisfies the conditions of Gödel’s theorems. Now a very interesting question is: what happens if you keep adding consistency statements to T, i.e., look at the union of T, T + Con(T), T + Con(T) + Con(T + Con(T)), etc.?
This question was first asked (and answered) by Turing in his 1938 Princeton dissertation. The answer is, if you do this ω + 1 many times, you get all true Π10 sentences of arithmetic (if you start with T = PA). It was subsequently cleared up by Feferman, and exteneded to progressions of theories where you add other undecidable sentences to T, such as the reflection principle (Prov(A) → A). The tricky part is defining the provability predicate for theories in these progressions; you have to use Kleene’s recursive ordinals to do this for transfinite ordinals.
If you haven’t seen this, look it up in Torkel Franzén’s book, or the original papers.
Alan M. Turing, 1939, ‘Systems of logic defined by ordinals’, Proceedings of the London Mathematical Society, ser. 2, 45:161-228
Solomon Feferman, 1962. Transfinite recursive progressions of axiomatic theories. Journal of Symbolic Logic, 27:259-316.