模态算术中的析取与存在性质
Disjunction and existence properties in modal arithmetic
摘要：
系统地研究了模态算术中的析取和存在性的几种形式。首先，我们新引入了三类模态算术公式$\mathrm{B}$、$Δ(\mathrm{B})$和$Σ(\mathrm{B})$，并研究了它们的基本性质。然后，我们证明了性质之间的几个含义。特别是，除其他事项外，我们证明，对于任何一致的递归可扩展$T$的$\mathbf{PA}(\mathbf{K})$与$T \nvdash \Box \bot$，$Σ(\mathrm{B})$ -析取属性，$Σ(\mathrm{B})$ -存在性，和$\mathrm{B}$ -存在性是成对等价的。引入了理论的$Σ(\mathrm{B})$ -可靠性的概念，证明了对于$\mathbf{PA}(\mathbf{K4})$的任意相容递归可列扩张，模态析取性质等价于理论的$Σ(\mathrm{B})$ -可靠性.
英文摘要：
We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm{B}$, $Δ(\mathrm{B})$, and $Σ(\mathrm{B})$ 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 $T$ of $\mathbf{PA}(\mathbf{K})$ with $T \nvdash \Box \bot$, the $Σ(\mathrm{B})$-disjunction property, the $Σ(\mathrm{B})$-existence property, and the $\mathrm{B}$-existence property are pairwise equivalent. Moreover, we introduce the notion of the $Σ(\mathrm{B})$-soundness of theories, and prove that for any consistent recursively enumerable extension of $\mathbf{PA}(\mathbf{K4})$, the modal disjunction property is equivalent to the $Σ(\mathrm{B})$-soundness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
