DISJUNCTION AND EXISTENCE PROPERTIES IN MODAL ARITHMETIC

<jats:title>Abstract</jats:title><jats:p>We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline1.png" /><jats:tex-math> $\mathrm {B}$ </jats:tex-math></jats:alternatives></jats:inline-formula>, <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline2.png" /><jats:tex-math> $\Delta (\mathrm {B})$ </jats:tex-math></jats:alternatives></jats:inline-formula>, and <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline3.png" /><jats:tex-math> $\Sigma (\mathrm {B})$ </jats:tex-math></jats:alternatives></jats:inline-formula> of formulas of modal arithmetic and study basic properties of them. Then, we prove several implications between the properties. In particular, among other things, we prove that for any consistent recursively enumerable extension <jats:italic>T</jats:italic> of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline4.png" /><jats:tex-math> $\mathbf {PA}(\mathbf {K})$ </jats:tex-math></jats:alternatives></jats:inline-formula> with <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline5.png" /><jats:tex-math> $T \nvdash \Box \bot $ </jats:tex-math></jats:alternatives></jats:inline-formula>, the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline6.png" /><jats:tex-math> $\Sigma (\mathrm {B})$ </jats:tex-math></jats:alternatives></jats:inline-formula>-disjunction property, the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline7.png" /><jats:tex-math> $\Sigma (\mathrm {B})$ </jats:tex-math></jats:alternatives></jats:inline-formula>-existence property, and the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline8.png" /><jats:tex-math> $\mathrm {B}$ </jats:tex-math></jats:alternatives></jats:inline-formula>-existence property are pairwise equivalent. Moreover, we introduce the notion of the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline9.png" /><jats:tex-math> $\Sigma (\mathrm {B})$ </jats:tex-math></jats:alternatives></jats:inline-formula>-soundness of theories and prove that for any consistent recursively enumerable extension of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline10.png" /><jats:tex-math> $\mathbf {PA}(\mathbf {K4})$ </jats:tex-math></jats:alternatives></jats:inline-formula>, the modal disjunction property is equivalent to the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S1755020322000363_inline11.png" /><jats:tex-math> $\Sigma (\mathrm {B})$ </jats:tex-math></jats:alternatives></jats:inline-formula>-soundness.</jats:p>