RUS  ENG
Full version
SEMINARS

Seminars "Proof Theory" and "Logic Online Seminar"
June 20, 2022 18:30, Moscow, online


On provability logic of HA (continuation)

Mojtaba Mojtahedi

Tehran



Abstract: In this talk we are going to present a sketch of the proof for axiomatization and decidability of provability logic of HA. At the beginning we explain how admissibility and unification for the intuitionistic logic can be relativised to NNIL, the class of fomulas with No Nested Implications in the Left. Using this, we axiomatize several preservativity and admissibility relations for intuitionistic modal logics. Then we introduce the provability semantics in the form of a specific Kripke-style semantics. The truth of $\Box A$ at a paticular node in the sense of this semantics uses the derivability in a specific modal logic associated with the accessible nodes. Finally, we use such semantics to reduce the arithmetical completeness of the provability logic of HA to the one for its $\Sigma_1$ version.
P.S.: This is a first presentation for two manuscripts which are not refereed yet. You may find them on my home page (items 11 and 12): http://pub.mmojtahedi.ir/.

Language: English
Series of reports


© Steklov Math. Inst. of RAS, 2024