| 研究概要 |
様相述語論理において,Barcan formulaの名で知られる論理式BFは,様相述語論理が定領域のKripkeモデル全体に関して完全になるために必要である上,現実の問題を記述する際にもしばしば要請されることから,重要な論理式とされている.不思議なことに,BFをさまざまに変形させたものが,無限論理や共通認識論理など他の論理のKripke完全性,種々の代数の埋め込みの連続性,coalgebraの振る舞いの記述など,いろいろな分野で重要な役割を果たしている.本研究では,そうしたBFの変形の幾つかと,それらの働きを分類・整理することを行った.
これらの内では,様相代数の埋め込みの連続性が,基本的な役割を果たしていることが分かった.様相代数の埋め込みの連続性が,Kripkeフレームと様相代数との双対性を,無限和や無限積のレベルまで拡張するため,様相述語論理と様相無限論理のKripke完全性を成り立たせている.また,共通認識論理は,様相無限論理のfragmentとしてとらえられることから,共通認識論理におけるBF(に相当する論理式)の役割も,ここから説明できることがわかった.
一方,coalgebraにおいて,BFに相当する性質である,predicate liftingのintersection preserving propertyと他の現象との関係は,まだほとんどわからない.ただ,Kripkeフレーム,様相代数のいずれもcoalgebraの枠組みでとらえられることを考えると,この方面から,より本質的な性質が抽出できる可能性は考えられる.
|
