Recording: https://disk.pku.edu.cn:443/link/6333F9FBDF221B6B354F73F952FB7EE8
Valid Until: 2027-05-31 23:59
Abstract: Turing introduced progressions of theories obtained by iterating the process of extension of a theory by its consistency assertion. Generalized Turing progressions can be used to characterize the theorems of a given arithmetical theory of quantifier complexity level $\Pi^0_n$, for any specific $n$. Such characterizations reveal a lot of information about a theory, in particular, yield consistency proofs, bounds on provable transfinite induction and provably recursive functions.
The conservativity spectrum of an arithmetical theory is a sequence of ordinals characterizing its theorems of quantifier complexity levels $\Pi_1$, $\Pi_2$, \etc. by iterated reflection principles. We describe the class of all such sequences and show that it bears a natural structure of an algebraic model of a strictly positive modal logic - reflection calculus with conservativity modalities.
Bio: Lev Beklemishev is a Principal researcher at Steklov Mathematical Institute of the Russian Academy of Sciences, Head of the Department of Mathematical Logic, and also an Academician of the Russian Academy of Sciences (2019). He graduated from the Faculty of Mathematics and Mechanics of Lomonosov Moscow State University in 1989 and defended Ph.D. thesis in 1992. He was awarded the Moscow Mathematical Society prize in 1994 and Alexander von Humboldt Fellowship (Germany) in 1998. His research interests are in mathematical logic, in particular in proof theory, formal arithmetic, provability logic, and modal logic.
