Abstract: Letterless formulas of GLP play the role of ordinal notations in the analysis of Peano Arithmetic based on graded provability algebras. They provide an alternative view of epsilon_0. Interrelations between ordinals and modal logic formulas will be discussed.
Reading:
Abstract: The reduction property of GPA is an algebraic analog of cut-elimination. It states that a Pi_{n+2} sentence of the form <n+1>A has the same Pi_{n+1}-consequences as all the sentences {<n>A, <n>(<n>A & A), ... }. In particular, it generalizes the well-known theorem of Parsons on the conservativity of ISigma_1 over PRA.
Reading:
Abstract: For a formulation of the Worm Principle see, e.g., here. The talk will cover the correctness and indepence proofs for the Worm Principle.
Reading: L. Beklemishev. Applications, a chapter on applications of provability logic to proof theory of arithmetic. Section 7.11, 7.12. Warning! This paper is still in an unfinished state.
Abstract:
KP_Omega is one of the relatively weak fragments of set theory that plays an important role in the theory of admissible sets. From the proof-theoretic point of view it is interesting, because it is one of the simplest examples of the so-called impredicative theories. Therefore, the calculation of the proof-theoretic ordinal of KP_Omega involves some significant novel features and, thus, is more difficult that the one of PA. By now, several methods have been developed to do this task. Moreover, KP_Omega has become a standard example to test the new methods. Ultimately, we are interested in developing the graded provability algebra approach to an extent sufficient for the analysis of KP_Omega. In the present talks we will start learning the basics of KP_Omega and its proof-theoretic analysis.
Starting with an introduction of some of the basic notions of generalized recursion theory (as there are $\omega_1^{CK}$, the first nonrecursive ordinal; Gödels constructible hierarchy $L$; inductive definitions; admissibility), we try to explain the ideas and results underlying impredicative proof theory. After that, we give some equivalent definitions of the proof-theoretic ordinal of an impredicative theory as an absolute measure of its strength. Finally, we treat the reductive proof theory of Kripke-Platek set theory (with infinity), $KP\omega$, and Kreisels theory of inductive definitions, $ID_1$, since both are paradigms of impredicative theories, thereby giving an overview of history and state-of-the-art of ordinal analysis.
Reading:
Abstract: The talk is non-technical and mainly a discussion of issues around the `problem of natural ordinal notations'. I will discuss the notions of proof-theoretic ordinals, various pathological and non-pathological examples and the relations with the notion of graded provability algebra.
Abstract: The main ideas underlying the proof-theoretic ordinal analysis of KP_omega will be explained.
Reading: C. Duchhardt. Diplomarbeit. Münster, 2001.