Taming "McKinsey-like" formula: An Extended Correspondence and Completeness Theory for Hybrid Logic H(@)

TL;DR

This paper extends the class of inductive formulas in hybrid logic with a McKinsey-like formula, demonstrating that all formulas in this class have first-order correspondents and identifying a subclass that axiomatizes complete hybrid logics.

Contribution

It introduces an extended inductive fragment for hybrid logic with a McKinsey-like formula and provides a proof-theoretic method to establish first-order correspondences.

Findings

Extended the inductive fragment to include McKinsey-like formulas.

Proved that all formulas in the extended class have first-order correspondents.

Identified a subclass that axiomatizes complete hybrid logics.

Abstract

In the present article, we extend the fragment of inductive formulas for the hybrid language L(@) in [8] including a McKinsey-like formula, and show that every formula in the extended class has a first-order correspondent, by modifying the algorithm hybrid-ALBA in [8]. We also identify a subclass of this extended inductive fragment, namely the extended skeletal formulas, which extend the class of skeletal formulas in [8], each formula in which axiomatize a complete hybrid logic. Our proof method here is proof-theoretic, following [10, 19] and [3, Chapter 14], in contrast to the algebraic proof in [8].