Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols
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.
Cite
@article{arxiv.2203.08720,
title = {Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols},
author = {Daniel Gaina and Guillermo Badia and Tomasz Kowalski},
journal= {arXiv preprint arXiv:2203.08720},
year = {2022}
}