Fri, 03.11.2017, 13:30 |
From Cut Elimination to Pi^1_1-Comprehension Logik-Seminar Speaker: Anton Freund, University of Leeds Room: S2|15-201 I will begin with an informal explanation of cut elimination and its use in the ordinal analysis of Peano arithmetic. The latter shows that Pi^{^0}_2-soundness is equivalent to the primitive recursive well-foundedness of an ordinal notation system. On a conceptual level, we observe that the focus is on low logical complexity. Next, I explain how an ordinal notation system can be relativized to a given well-order. This brings us to the level of Pi^{^1}_2-statements. Many well-known axioms of that complexity have been characterized in terms of relativized ordinal notation systems: from arithmetical comprehension (Girard, Hirst) up to the existence of omega-models of bar induction (Rathjen and Vizcaíno). Finally, I present a new result at the next type-level: Following a suggestion by Montalbán and Rathjen, I relativize an ordinal notation system to a relativized ordinal notation system. In this way one can get a characterization of Pi^{^1}_1-comprehension, which is a Pi^{^1}_3-statement (preprint available as arXiv:1704.01662). |
---|
Fachbereich Mathematik
Technische Universität Darmstadt
Schlossgartenstraße 7
64289 Darmstadt