Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder

TL;DR

This paper develops a proof-theoretic Sahlqvist-type completeness theory for hybrid logic with satisfaction operators and binders, extending previous work with a new proof strategy and an adapted algorithm.

Contribution

It introduces skeletal Sahlqvist formulas for hybrid logic with binders and proves their completeness using a proof-theoretic approach and a modified algorithm.

Findings

Established a class of skeletal Sahlqvist formulas for hybrid logic with binders.

Proved completeness of these formulas with respect to corresponding frame classes.

Extended the algorithm $ extsf{ALBA}^{ abla}$ for this logic setting.

Abstract

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 $\phi$ and its hybrid pure correspondence $\pi$, $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+\phi$ proves $\pi$, therefore $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+\phi$ is complete with respect to the class of frames defined by $\pi$, using a restricted version of the algorithm $\mathsf{ALBA}^{\downarrow}$ defined in \cite{Zh21c}.