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$.
Categories: math.LO