Completeness theorems for modal logic in second-order arithmetic
Sho Shimomichi, Yuto Takeda, Keita Yokoyama
TL;DR
This work maps the reverse-mathematical strength of modal propositional completeness theorems in second-order arithmetic. It shows that weak completeness for modal logics built on $\mathbf{K}$ is provable in $\mathrm{RCA}_0$, while strong completeness via canonical models requires $\mathrm{ACA}_0$, and a simpler strong completeness form without canonical models matches $WKL_0$. The authors formalize modal logic inside $\mathrm{RCA}_0$, prove weak completeness for $\mathbf{K}\Sigma$ logics (with $\Sigma\subseteq\{T,B,4,D\}$) and for $\mathbf{GL}$ in $\mathrm{RCA}_0$, and then establish a tight equivalence between strong completeness (via canonical models) and $\mathrm{ACA}_0$ over $\mathrm{RCA}_0$, while also exploring FO-based formulations that align with $\mathrm{WKL}_0$. The results illuminate the precise strength needed for strong modal completeness and connect modal semantics with classical reverse mathematics, highlighting the role of low basis techniques in the canonical-model construction. Open questions remain about completeness for logics involving $5$ and the full cube/S4.2 systems within $\mathrm{RCA}_0$.
Abstract
This paper investigates the logical strength of completeness theorems for modal propositional logic within second-order arithmetic. We demonstrate that the weak completeness theorem for modal propositional logic is provable in $\mathrm{RCA}_0$, and that, over $\mathrm{RCA}_0$, $\mathrm{ACA}_0$ is equivalent to the strong completeness theorem for modal propositional logic using canonical models. We also consider a simpler version of the strong completeness theorem without referring to canonical models and show that it is equivalent to $\mathrm{WKL}_0$ over $\mathrm{RCA}_0$.