Three faces of recursion axioms: the case of constructive dynamic logic of relation changers
Three faces of recursion axioms: the case of constructive dynamic logic of relation changers
复制标题
递归公理的三个方面：关系变换器的构造动态逻辑的情况
DOI：
10.1093/logcom/exac013
复制
发表时间：
2022
影响因子：
0.7
通讯作者：
Ryo Hatano and Katsuhiko Sano
中科院分区：
文献类型：
--
作者：
Katsuhiko Sano and Tomoyuki Yamada;Youan Su and Katsuhiko Sano;Hiroakira Ono and Katsuhiko Sano;Ryo Hatano and Katsuhiko Sano
本文直观地推广了van Benhim和Liu的关系变更器的动态逻辑，其中关系变更器是改写每个主体的可及性关系的动态算子。我们使用Nishimura的Klipke语义作为构造性命题动态逻辑来定义关系变更器的语义。通过由内而外和外而内的递归公理两种重写策略，建立了关系变更器的构造性动态逻辑的Hilbert型公理的强完备性结果。为了通过由外而内的策略建立语义完备性，我们提出了关系变更器组合的概念和适当定义的公式长度的概念。此外，我们还揭示了递归公理还有两个面：语义面和证明面。对于语义面，我们为关系变更器的动态逻辑引入了另一种语义，以明确内向外策略中使用的递归公理的语义含义。这使得我们得到了原始语义公理化的语义完备性证明，它不需要基于递归公理的重写策略。对于证明面，我们将由外而内策略所需的每一个递归公理转化为两条(左、右)推理规则，为关系变更器的动态逻辑提供顺序演算。由于得到的序列演算是无割半解析的，所以它仍然利用前原法的克雷格插值定理。
This paper proposes an intuitionistic generalization of van Benthem and Liu’s dynamic logic of relation changers, where relation changers are dynamic operators that rewrite each agent’s accessibility relation. We employ Nishimura’s Kripke semantics for a constructive propositional dynamic logic to define the semantics of relation changers. Strong completeness results of Hilbert-style axiomatizations for constructive dynamic logic of relation changers are established by two types of rewriting strategies via recursion axioms: inside-out and outside-in strategies. To establish the semantic completeness by outside-in strategy, we propose the notion of composition of relation changers and an appropriately defined notion of length of a formula. Moreover, we reveal that recursion axioms have additional two faces: semantic and proof-theoretic ones. As for the semantic face, we introduce an alternative semantics for dynamic logic of relation changers to specify the semantic meaning of recursion axioms used in the inside-out strategy. This leads us to a semantic completeness proof of the axiomatization for the original semantics, which does not require a rewriting strategy based on recursion axioms. As for the proof-theoretic face, we transform each of recursion axioms required in the outside-in strategy into two (left and right) inference rules to provide a sequent calculus for dynamic logic of relation changers. Since the resulting sequent calculus is cut-free but semi-analytic, it still enjoys the Craig interpolation theorem by Maehara’s method.