{"id":"arxiv/2607.01970","url":"https://arxiv.org/abs/2607.01970","tags":["math.LO"],"score":0,"title":"Bisimulations in second-order arithmetic","domain":"math.LO","source":"arxiv","authors":["Yuto Takeda","Keita Yokoyama"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-02","reactions":{}}