Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols

TL;DR

This paper proves an Omitting Types Theorem for a broad class of hybrid-dynamic first-order logics with rigid symbols, using a novel forcing technique, and applies it to derive fundamental model-theoretic results.

Contribution

It introduces a forcing-based proof of the OTT for hybrid-dynamic first-order logic with rigid symbols, extending to uncountable signatures without requiring compactness.

Findings

Proved OTT for hybrid-dynamic first-order logic with rigid symbols

Derived Löwenheim-Skolem theorems for the logic

Established a completeness theorem for the logic's constructor-based variant

Abstract

In the the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybriddynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across worlds) closed under negation and retrieve. The logical framework can be regarded as a parameter and it is instantiated by some well-known hybrid and/or dynamic logics from the literature. We develop a forcing technique and then we study a forcing property based on local satisfiability, which lead to a refined proof of the OTT. For uncountable signatures, the result requires compactness, while for countable signatures, compactness is not necessary. We apply the OTT to obtain upwards and downwards L\"owenheim-Skolem theorems for our logic, as well as a completeness theorem for its constructor-based variant. The main result of this paper can easily be recast in the institutional model theory framework, giving it a higher level of generality.