论文标题
与粘合剂的混合逻辑的Sahlqvist型完整性理论
Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder
论文作者
论文摘要
在本文中，我们在\ cite {zh21c}中继续进行研究，以使用满意度运算符和DownArow binders $ \ Mathcal {l}（@@，@\，\ downarrow）$开发混合逻辑的SAHLQVIST型完整性理论。我们根据\ cite {conrob}的想法为$ \ Mathcal {l}（@，\ downarrow）$定义骨骼sahlqvist formulas c。 $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$ proves $π$, therefore $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$ is complete with respect to the class of frames defined by $π$, using a restricted version of the algorithm $ \ Mathsf {alba}^{\ downarrow} $在\ cite {zh21c}中定义。
In the present paper, we continue the research in \cite{Zh21c} to develop the Sahlqvist-type completeness theory for hybrid logic with satisfaction operators and downarrow binders $\mathcal{L}(@, \downarrow)$. We define the class of skeletal Sahlqvist formulas for $\mathcal{L}(@, \downarrow)$ following the ideas in \cite{ConRob}, but we follow a different proof strategy which is purely proof-theoretic, namely showing that for every skeletal Sahlqvist formula $ϕ$ and its hybrid pure correspondence $π$, $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$ proves $π$, therefore $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$ is complete with respect to the class of frames defined by $π$, using a restricted version of the algorithm $\mathsf{ALBA}^{\downarrow}$ defined in \cite{Zh21c}.
