| 研究課題/領域番号 |
20K03718
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| 研究分担者 |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | omitting types theorem / hybrid logic / dynamic logic |
|---|
| 研究実績の概要 |
We proved an Omitting Types Theorem for an arbitrary fragment of hybrid- dynamic first-order logic with rigid symbols (that is, 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 developed a forcing technique and then we study a forcing property based on local satisfiability, which lead to a refined proof of the Omitting Types Theorem. For uncountable signatures, the result requires compactness, while for countable signatures, compactness is not necessary. We apply the Omitting Types Theorem to obtain upwards and downwards Lowenheim-Skolem theorems for our logic, as well as a completeness theorem for its constructor-based variant.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
Everything is going according to the plan described in the application.
|
| 今後の研究の推進方策 |
Within 2022FY, we are planning to study a Robinson consistency theorem for a class of many-sorted hybrid logics as a consequence of an Omitting Types Theorem. An important corollary of this result is an interpolation theorem.
|
| 次年度使用額が生じた理由 |
Due to the COVID-19 pandemic, there were strict travel restrictions. I hope that in FY2022 I can travel abroad and engage in research activities with my collaborators in Europe.
|
