| 作成者 |
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 号 |
|
| 開始ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| 権利関係 |
|
| 関連DOI |
|
| 概要 |
In the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybrid dynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across w...orlds) 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öwenheim-Skolem theorems for our logic, as well as a completeness theorem for its constructor-based variant.続きを見る
|
Mendeley出力
