Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Forcing and Interpolation in First-Order Hybrid Logic with rigid symbols

Daniel Găină, Go Hashimoto

TL;DR

The paper develops a forcing-based approach to Craig interpolation for a many-sorted first-order hybrid logic with rigid symbols, accommodating possibly empty domains. It dynamically extends signatures by adding new constants in a way that preserves consistency, and uses this to derive general CIP/RCP criteria via signature pushouts. The framework relies on institution-theoretic notions (signature morphisms, reducts, generated/reachable models) and yields a direct CIP proof for FOHLR that complements prior results. This contributes to modular specification and verification by clarifying when interpolation holds in complex many-sorted, hybrid logics with rigid symbols.

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 both Robinson's consistency and Craig interpolation properties.

Forcing and Interpolation in First-Order Hybrid Logic with rigid symbols

TL;DR

The paper develops a forcing-based approach to Craig interpolation for a many-sorted first-order hybrid logic with rigid symbols, accommodating possibly empty domains. It dynamically extends signatures by adding new constants in a way that preserves consistency, and uses this to derive general CIP/RCP criteria via signature pushouts. The framework relies on institution-theoretic notions (signature morphisms, reducts, generated/reachable models) and yields a direct CIP proof for FOHLR that complements prior results. This contributes to modular specification and verification by clarifying when interpolation holds in complex many-sorted, hybrid logics with rigid symbols.

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 both Robinson's consistency and Craig interpolation properties.
Paper Structure (11 sections, 13 theorems, 3 equations, 1 figure)

This paper contains 11 sections, 13 theorems, 3 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Many-sorted first-order logic (FOL)
  3. Many-sorted vs. single-sorted
  4. First-Order Hybrid Logic with rigid symbols (${\mathsf{FOHLR}}$)
  5. Basic definitions and results
  6. Presentations and theories
  7. Amalgamation
  8. Substitutions
  9. Reachable and generated models
  10. Basic sentences
  11. Forcing

Key Result

Lemma 8

The following pushout of first-order signature morphisms does not have CIP.

Figures (1)

  • Figure 1: Quantification pushout

Theorems & Definitions (37)

  • Example 5
  • Example 6
  • Definition 7: Interpolation
  • Lemma 8
  • Theorem 9: First-order interpolation gai-pop-rob
  • Remark 13
  • Lemma 14
  • Proposition 16: Local satisfaction condition
  • Definition 17: Elementary equivalent pointed models TOCL2025
  • Remark 18
  • ...and 27 more