2021 Fiscal Year Research-status Report
Mathematical foundations for the reconfiguration paradigm
| Project/Area Number |
20K03718
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
GAINA Daniel 九州大学, マス・フォア・インダストリ研究所, 准教授 (80595778)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 教授 (80209783)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | omitting types theorem / hybrid logic / dynamic logic |
|---|
| Outline of Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Everything is going according to the plan described in the application.
|
| Strategy for Future Research Activity |
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.
|
| Causes of Carryover |
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.
|
