Abstract

It is shown that the propositional modal logic IRM (interpretability logic with Montagna's principle and with witness comparisons in the style of Guaspari's and Solovay's logicR) is sound and complete as the logic ofII 1-conservativity over each∑ 1-sound axiomatized theory containingI∑ 1. The exact statement of the result uses the notion of standard proof predicate. This paper is an immediate continuation of our paper [HM]. Knowledge of [HM] is presupposed. We define a modal logic, called IRM, which includes both ILM andR (the logic of [GS]) and prove an arithmetical completeness theorem in the style of [GS], thus showing that IRM is the logic ofII 1-conservativity with witness comparisons. The reader is recommended to have Smoryński's book [Sm] at his/her disposal