Axiomatization of Hybrid Logic of Link Variations

Authors: Penghao Du and Qian Chen

In this paper, we investigate local and global dynamic modal operators which have the ability to update the accessibility relation of a model. For the global operators, the logic $\mathsf{GLV}$ of global link variations based on hybrid logic $\mathsf{H}(@)$ is introduced, which involves global link cutting, adding and rotating simultaneously. A Hilbert-style calculus $\mathsf{C_{GLV}}$ is provided. By constructing families of canonical models inductively, we prove that the calculus $\mathsf{C_{GLV}}$ is sound and strongly complete with respect to $\mathsf{GLV}$. For the local operators, we extended the logic $\mathsf{LLD}(@,\downarrow)$ of link deletion introduced in [Li, 2020] to $\mathsf{LLV}$, which is based on the hybrid logic $\mathsf{H}(\mathsf{E},\downarrow\ )$ and involves local definable link cutting, adding and rotating. By defining local named dynamic operators and providing recursion axioms for them, we obtain a sound and strongly complete calculus $\mathsf{C_{LLV}}$ for $\mathsf{LLV}$. Moreover, we show that for an arbitrary set $X$ of global and local dynamic operators, the calculus $\mathsf{C_{GLV}}(X)$ and $\mathsf{C_{LLV}}(X)$ are still sound and strongly complete w.r.t the logic $\mathsf{GLV}(X)$ and $\mathsf{LLV}(X)$, respectively.