Forcing and Interpolation in first-order hybrid Logic with rigid symbols

TL;DR

This paper introduces a forcing technique for first-order hybrid logic with rigid symbols, establishing an interpolation property and providing criteria for signature square satisfaction.

Contribution

It develops a novel forcing method that preserves consistency when adding constants, enabling the proof of Craig interpolation in hybrid logic.

Findings

Established an analogue of Craig Interpolation Property for the logic.

Developed a forcing technique that preserves consistency with new constants.

Derived criteria for signature square to satisfy Craig interpolation.

Abstract

In this paper, we establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains. Using this forcing method, we derive general criteria that are sufficient for a signature square to satisfy Craig interpolation property.