Bisimulations in second-order arithmetic

Abstract

This paper investigates the logical strength of two theorems in modal propositional logic - the Hennessy-Milner theorem and the van Benthem characterization theorem - within the framework of second-order arithmetic. We demonstrate that the Hennessy-Milner theorem is equivalent to ${\mathrm{ACA}}_0$ over ${\mathrm{RCA}}_0$. For the van Benthem characterization theorem, we introduce three variants: the semantic, syntactic, and hybrid forms. We show that the semantic form is provable in ${\mathrm{RCA}}_0$, the syntactic form is provable in $\mathrm{PRA}$, and the hybrid form is equivalent to the weak completeness theorem for first-order logic over ${\mathrm{RCA}}_0$.