Disjunction and existence properties in modal arithmetic

TL;DR

This paper explores various disjunction and existence properties in modal arithmetic, introduces new classes of formulas, and establishes equivalences between these properties under certain conditions.

Contribution

It introduces three new classes of formulas in modal arithmetic and proves their relationships with disjunction and existence properties, expanding understanding of modal arithmetic theories.

Findings

$ ext{B}$-existence and disjunction properties are equivalent for certain theories.

Modal disjunction property is equivalent to $ ext{B}$-soundness in theories extending $ ext{PA}( ext{K4})$.

New classes $ ext{B}$, $ riangle( ext{B})$, and $ ext{S}( ext{B})$ are introduced and studied.

Abstract

We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm{B}$, $\Delta(\mathrm{B})$, and $\Sigma(\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 $\Sigma(\mathrm{B})$-disjunction property, the $\Sigma(\mathrm{B})$-existence property, and the $\mathrm{B}$-existence property are pairwise equivalent. Moreover, we introduce the notion of the $\Sigma(\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 $\Sigma(\mathrm{B})$-soundness.