In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{\ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
翻译:在本文中,我们为建设性模式逻辑CK和CD中的证据提供了两种新的语义。第一个语义通过扩展组合式证据的语义,用于推理直率逻辑,在这种逻辑中,证据在线形碎片(arena net)和平行的削弱-分包碎片(skew 纤维化)中被考虑到。特别是,我们通过定向图解(现代舞台)提供了模型公式的编码,并将线性证据编码为模式场,配备了符合地形学标准的脊椎分区。第二个语义是通过在模型场上赢得一场双玩游戏的无辜策略。这是通过扩展Heijltjes-Hughes-Strasurs)汉堡在直觉式组合证据和在Hyland-Ong竞技场中赢得无辜策略之间的对应。我们利用我们的第一个结果,为在模型竞技场上赢得符合模式证据的游戏策略提供了特征。