Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

Jim de Groot, João Marcos, Rodrigo Stefanes

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 o…