{"id":"arxiv/2606.31879","url":"https://arxiv.org/abs/2606.31879","tags":["math.LO","cs.LO"],"score":0,"title":"Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic","domain":"math.LO","source":"arxiv","authors":["Jim de Groot","João Marcos","Rodrigo Stefanes"],"reviews":0,"subject":"math.LO","summary":"We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic. En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy-Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Los's Theorem, elementary embeddings and countable saturation.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-30","reactions":{}}