Modal logic semantics for ordinal analysis of bar induction
Vlad Lazar
There has been a notable increase in the utilization of provability logic within proof-theory, most of which is derived form Giorgi Japaridze’s poly-modal logic (GLP) [2]. An interesting restriction of GLP called reflection calculus (RC) [3] was developed by Lev Beklemishev to facilitate the proof-theoretic 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:
- \(\top\) is the system ACA\(_0\).
- \(\Diamond^1_\alpha A\) is ACA\(_0\) + RFN\(_{\Pi^1_\alpha} (A)\).
- \(\Diamond^2_\alpha A\) is ACA\(_0\) + \(\omega\)-RFN\(_{\Pi^1_\alpha} (A)\).
- \(\downarrow A\) is the theory: \(\{\varphi\in\Pi^1_\infty\;|\;A\vdash \forall M(M\models \varphi)\},\)
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 proof-theoretic analysis of the theory of bar induction (BI). Our current results are on the semantic development of \(\omega\)RC. We have managed to prove Kripke-completeness for this logic, and are currently working on combinatorial techniques for analyzing the relationship between formulas.
Bibliography
- Friedman, Harvey, Some systems of second order arithmetic and their use, Proceedings of the international congress of mathematicians (Vancouver, BC) (1975), pp. 235–242.
- Japaridze, Giorgi K, The polymodal logic of provability, Intensional Logics and Logical Structure of Theories: Material from the fourth Soviet–Finnish Symposium on Logic, Telavi (1985), pp. 16–48.
- Beklemishev, Lev, Positive provability logic for uniform reflection principles, Annals of Pure and Applied Logic,vol. 165 (2014), no. 1, pp. 82–105.
- Pakhomov, Fedor and Walsh, James, Reflection ranks and ordinal analysis, The Journal of Symbolic Logic,vol. 86 (2021), no. 4, pp. 1350–1384.