Completeness theorems for modal logic in second-order arithmetic

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{R}\mathrm{C}\mathrm{A}}_0$, and that, over ${\mathrm{R}\mathrm{C}\mathrm{A}}_0$, ${\mathrm{A}\mathrm{C}\mathrm{A}}_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{W}\mathrm{K}\mathrm{L}}_0$ over ${\mathrm{R}\mathrm{C}\mathrm{A}}_0$.