Forcing and Interpolation in first-order hybrid Logic with rigid symbols
It provides a foundational result for hybrid logic, which is relevant to logicians and computer scientists working on modal and hybrid logics.
The paper proves Craig Interpolation Property for a many-sorted first-order hybrid logic by developing a forcing technique that adds constants while preserving consistency, even with possibly empty domains.
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.