| Research Abstract |
共通認識論理とは,共通認識を表す様相演算子を持った様相命題論理である.この論理はコンパクトでないことが,Segerberg等によって知られている.共通認識論理の述語拡大にBarcan formulaを加えたものを,共通認識述語論理とよぶが,これはrecursively enumerableにならないことがWolterによって知られている.このコンパクトでないということと,recursively enumerableでないという二つの性質のため,共通認識述語論理は,定領域のKripke frame全体に関して完全という,明快な特徴づけが存在するのに対し,十分に性質のよい証明系は得られていなかった.それに対し,本研究では,共通認識述語論理に対し,後述するような意味でよい性質を持つ,二つの証明系を与えた.一つは,非コンパクトな推論規則を一箇所にしか持たない証明系である.前述のように,共通認識述語論理はコンパクトでないから,すべての推論規則をコンパクトにすることはできない.それを,共通認識演算子の右入れ一箇所に制限することを行った.これにより,実際に証明図を与えるのが,簡単になった.もうひとつは,非コンパクトな推論規則がただ一つで,しかも,カットを持たない証明形である.この証明系は,一種のタブロー法によるもので,実際に証明図を与えるのには不向きであるが,subformula propertyを満たすことから,理論上の応用範囲は広いものである.実際,それを用いることで,Wolterの結果の拡張として,共通認識論理に含まれるformulaのうち,共通認識演算子の正の出現,量化記号,知識演算子のすべてを含むものの集合はrecursively enumerableでないが,その補集合はrecursively enumerableであることを示した.
|
