Speaker
Vlad Lazar
University of Ghent
Talks at this conference:
Friday, 15:40, J335 
Modal logic semantics for ordinal analysis of bar induction 
There has been a notable increase in the utilization of provability logic within prooftheory, most of which is derived form Giorgi Japaridze’s polymodal logic (GLP) [2]. An interesting restriction of GLP called reflection calculus (RC) [3] was developed by Lev Beklemishev to facilitate the prooftheoretic analysis of PA. This method proved to be quite powerful, and has since been expanded upon. Our work is primarily focused on an extension of reflection calculus called \(\omega\)RC, whose motivation comes from recent developments in ordinal analysis by iterated reflection principles [4]. The grammar of \(\omega\)RC is as follows: \[A:= p\;\;\top\;\;A\wedge B\;\; \Diamond^1_{\alpha\geq 1} A\;\;\Diamond^2_{\alpha\geq 2}\;\; \downarrow A \text{ , where } \alpha\leq \omega.\]Intended arithmetical interpretation:
where M ranges over the countably coded \(\omega\)models of ACA\(_0\). Given the equivalence between bar induction and \(\omega\)model reflections [1], the aim of this modal logic is to aid in the prooftheoretic analysis of the theory of bar induction (BI). Our current results are on the semantic development of \(\omega\)RC. We have managed to prove Kripkecompleteness for this logic, and are currently working on combinatorial techniques for analyzing the relationship between formulas. Bibliography
