Truth and Proof in Edinburgh

The 2006 RZ World tour just started at the “Truth and Proof” conference in Edinburgh. Thanks Jeff Ketland and Jean-Louis Hudry for putting this on and inviting me! So far we had some excellent talks by John Dawson on the history of the notion of truth and use of semantic methods in logic; by Hannes Leitgeb on his work on modal predicates; and by Phil Welch on games describing supervaluation fixpoints and Hannes’ dependency stuff. Met some people I’ve been hoping to meet for a long time, including Jeff, John, Peter Smith, Stewart Shapiro, Phil Ebert, Aatu Koskensilta, and seeing some old friends again. Ok, no time to put in links, Stewart is speaking in a few minutes, and then Panu Raatikainen.

Ordinal Logics

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.