Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder

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}(\mathrm{@},\downarrow )$. We define the class of skeletal Sahlqvist formulas for $\mathcal{L}(\mathrm{@},\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}(\mathrm{@},\downarrow )}+\phi$ proves $\pi$, therefore ${\mathbf{K}}_{\mathcal{H}(\mathrm{@},\downarrow )}+\phi$ is complete with respect to the class of frames defined by $\pi$, using a restricted version of the algorithm ${\mathsf{A}\mathsf{L}\mathsf{B}\mathsf{A}}^{\downarrow }$ defined in \cite{Zh21c}.