Departamento de Matemática
Universidade de Lisboa
Thursday, 19 September 2013, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Ordinal notations is one of the central ingredients of ordinal analysis, a part of proof theory whose primary goal is connecting consistency of mathematical theories to well-foundedness of certain primitive-recursive orderings of natural numbers. A distinctive feature of the set O ⊆ N of codes of recursive ordinals involved is, always, its primitive-recursiveness, in that both O and the relation { (s,t) | s, t ∈ O & |s| < |t| } are primitive-recursive sets, |t| standing for the set-theoretical meaning of a term t. The methods here, most often, employ cut-elimination and collapsing techniques for infinite derivations. Apart of mere consistency, usually they provide additional information, like reducing classical theories to intuitionistic ones.
In the recent years there has been some research on re-proving some of those results by different methods, including originating from Gödel's functional interpretation. For example, Ferreira [1] shows how it can be done in the case of Kripke-Platek set theory with Infinity. Ferreira's work, too, does use ordinal notations, but their built-up is very different, it is a variant of Howard's system of abstract constructive ordinals [2]. An obvious question arises whether it is, mathematically, essentially different from ordinal notation systems traditionally used in ordinal analysis.
We show that this is, indeed, the case. While the systems O of codes of ordinal terms of [1] and [2] are obviously primitive-recursive, the relations { (s, t) | s, t ∈ O & |s| < |t| } are not so, even not decidable. In other words, for solving the question "|s| vs. |t|" there cannot be any program, in principle. Indeed, using those terms, it is possible to code the halting problem of a Turing machine as an |s| < |t| question.
This work has arisen thanks to correspondence with Fernando Ferreira and Jeremy Avigad.
References