The Kripke semantics of various logics arises via categorical dualities between a category of relational frames and their maps, and a category of algebras and logical homomorphisms. When the relational frames are considered as computational systems (e.g. the states of a machine), the corresponding algebra is one of logical predicates on these systems (e.g. predicates on these states, i.e. program logics). Our aim is to extend this phenomenon to relations, putting well-behaved relations between systems (e.g. bisimulations) in correspondence with relations between predicates. This is achieved by constructing particular relational extensions of Tarski duality (for infinitary classical propositional logic) and Thomason duality (for infinitary classical modal logic). We sketch how these dualities give rise to a proof system that relates formulae between different systems.

翻译：多种逻辑的克里普克语义源于关系框架及其映射范畴与代数及逻辑同态范畴之间的范畴对偶性。当关系框架被视为计算系统（例如机器状态）时，相应的代数成为这些系统上的逻辑谓词代数（例如状态上的谓词，即程序逻辑）。我们的目标是将这一现象扩展至关系层面，使系统之间良行为的关系（例如互模拟）与谓词之间的关系相对应。这通过构建塔斯基对偶性（用于无穷经典命题逻辑）和托马森对偶性（用于无穷经典模态逻辑）的特定关系扩展来实现。我们简要勾勒了这些对偶性如何催生出一个关联不同系统间公式的证明系统。