代表的な様相論理の体系は、有限モデル性という行儀のよい性質を満たします。本稿では、この有限モデル性の証明に用いられる濾過法という手法を見ていきます。最後に補足として、有限モデル性と決定可能性との関係を説明します。
本稿の説明のベースとなっているのはThe Open Logic Projectの様相論理の教科書です。また、妥当性の定義などは大西『論理学』をもとにしています(説明の簡略化のため一部改変しています)。本稿が、これらの文献で説明されていることを自分用に嚙み砕いて書いたメモのようなものであることを予めご了承ください。詳細を知りたい方は参考文献を参照してください。
準備
以下では、様相論理の語彙は加算無限個の命題変項の集合とからなるものとし、これにより帰納的に構成される論理式の集合をとする。その他の通常の論理結合子は糖衣構文として定義する(e.g.)。
可能世界意味論
ここでは、(正規)様相論理のモデル論として、可能世界意味論(possible world semantics)というものを導入する。詳細な説明は行わないので、興味のある方には適宜教科書などを参照していただきたい。
フレーム
様相論理のフレーム(frame)とは、以下により定まる組のことである(以下では単に「フレーム」という)。
- : 非空な集合
- これを可能世界(possible world)の集合という
-
- これを到達可能性関係(accesibility relation)という
モデル
様相論理のモデル(model)とは、以下により定まる組のことである(以下では単に「モデル」という)。
- : フレーム
-
- 付値の拡張: 付値は以下のようにしてとなるよう帰納的に拡張される
妥当性
と、モデル・フレームについて、
-
- このことを、がモデル上で妥当である(valid)という
- これが成り立たないをに対する反例モデル(counter model)という
-
以下では、全てのフレームのクラスをとする。さらに、フレームの到達可能性関係に対して、以下のような制約を加えることを考える。
- : 反射性 ()
- : 対称性 ()
- : 継続性 ()
- : 推移性 ()
- : ユークリッド性 ()
これらの制約を加えて得られるフレームのクラスを、の後ろに対応するラベルを付けた名前で表す(e.g. は反射的なを持つモデルのクラス)。慣習的に、をそれぞれという。
このようにフレームの定義を変えると、妥当になる論理式も変わる。フレームのクラスに対応して定まる妥当な式の集合を論理として定める。
論理
フレームのクラスに対して、様相論理を任意の上で妥当な論理式の集合とする。その他のフレームのクラスに対しても同様に論理を定める。
また、論理に対してとなることを、がで妥当であるという。
有限モデル性
有限モデル性
論理を定義するフレームのクラスをとする。が有限モデル性(finite model property)を満たすとは、以下が成り立つことである: 任意のに対して、に対する上の反例モデルが存在するならば、への推論に対する上の有限の反例モデルが存在する
ただし、有限のモデルとは、モデルであってが有限集合であるものを指す。
有限モデル性を証明するためには、所与の推論に対する任意の反例モデル(が無限集合でありうる)を、有限の反例モデルに変換する手続きを与える必要がある。より具体的には、の要素の個数を、反例モデルとしての性質を失わないように「減らす」ないし「圧縮する」必要がある。
そこで方針として有力なのは、適当な同値関係を定めての要素を「同一視」し、商集合を考えることで世界の個数を減らす、という方法である。このようなモデルの構成方法を濾過法 (filtration method)という。
同値関係を考えることで付値は自然に定められるが、到達可能性関係の定義はそこまで自明ではない。対象となる論理体系に応じてどのように到達可能性関係を設定するかが、有限モデル性の証明における焦点となる。
濾過法
定義
濾過法を定義するための道具立てとして、2つの概念を用意する。
について、が部分論理式について閉じている(closed under sub-formulae)とは、以下が成り立つことである。
ただしは、の部分論理式(自身も含む)の集合を表す
モデル、および部分論理式について閉じているが与えられたとき、上の同値関係を以下のように定める (これは確かに同値関係になる)
以下では、この同値関係により定まる同値類をのように(を明示せずに)表す
これらを用いて、モデルに対する「濾過」の仕様を以下のように定める。
濾過
モデル、および部分論理式について閉じているに対して、のによる濾過(filtration)とは、以下を満たすモデルである
- 任意のに対して、
の定義は一見複雑であるが、2-1はがwell-definedになるための条件であり、2-2は「がに関するの挙動を模倣すること」を要求していると(非形式的に)捉えることができる。
- 濾過は一意に定まるとは限らない(「仕様」と書いたのはそのためである)。は定義から一意に定まるが、の部分に自由度がある。
- 本当はがwell-definedになることの確認が必要であるが、割愛する。
- 濾過は部分論理式について閉じているに対してのみ定まる。よって、これ以降で「のによる濾過」と書いた場合、が部分論理式について閉じていることを(明示せずに)前提にすることがある。
前述のとおり、濾過を定義する動機は、反例モデルとしての性質を保ったまま世界の個数を減らすことであった。以下の定理は、濾過法はの範囲内では付値を変えないことを主張しており、「反例モデルとしての性質を保つ」という部分を保証している。
の構成に関する帰納法で示す。は部分式について閉じているので、帰納法の各ステップで出現するの部分式もまたの要素となることに注意する。
- の場合: 定義より明らか
- の場合: 複合式に対する付値の定義を用いて部分式の条件へと分解し、帰納法の仮定を適用すればよい(詳細は割愛)。
- の場合:
の証明: については、仮定よりであり、を仮定すると、定義8の2-2からとなるので成立。については、定義8の2-1よりとなるので成立。
例
まだ濾過の定義が与えられただけで、実際にそれが存在するかは分かっていない。以下では、一般的に構成できる2つの濾過の例を挙げる。
最も粗い・最も細かい
モデルと部分論理式について閉じているに対して、とを定義8の1,3の通りに定めたとき、
最も細かい濾過・最も粗い濾過は、どちらも実際に濾過になる。証明は割愛する。
到達可能性関係の性質
モデル中の到達可能性関係が持つ性質のうちの一部は、濾過に対してそのまま「引き継がれる」という特徴がある。
モデルのによる任意の濾過は以下を満たす。
- は反射的は反射的
- は継続的は継続的
-
- となることをが普遍的であるという。普遍的なフレームのクラスにより定まる論理はと一致することが知られている。
この定理は、対称性・推移性などに対しては一般には成り立たない。しかし、をうまく「設計」することで、濾過にも同じ性質を引き継がせることができる。この「設計」のパーツとして必要なものをまずは定義する。
モデルに対して、に関する2項述語を(メタレベルで)以下のように定義する。
ここで定義した~に対しては、直観的な説明を与えることができる。
- : 濾過の定義の2-2に該当する → 濾過となるために必要
- : (ある意味で)の「逆」になっている→ 対称性を反映
- : でが成り立つなら任意の到達可能なでもとなるということなので、を意図したものになっている → 推移性を反映
- : との両方を反映
以下の定理は、これらの説明を形式的に表現している。
モデルと部分論理式について閉じているに対して、を定義8の1,3の通りに定めたとき、
- であるならば、以下が成り立つ
- は対称的である
- が対称的ならば、はのによる濾過である
- であるならば、以下が成り立つ
- は推移的である
- が推移的ならば、はのによる濾過である
- であるならば、以下が成り立つ
- は対称的かつ推移的である
- が対称的かつ推移的ならば、はのによる濾過である
- であるならば、以下が成り立つ
- は推移的かつユークリッド的である
- が推移的かつユークリッド的ならば、はのによる濾過である
(3)の証明のみ与える(その他の場合もだいたい同様である)。
の対称性・推移性
- 対称性: を仮定する。定義より, であるから、明らかにが成り立つ。
- 推移性: を仮定する。を示すためには、上で示した対称性より、とを示せば十分である。
- : を仮定する。これとよりであり、これとよりとなるので、が成り立つ。
- : を仮定する。これとよりであり、これとよりとなるので、が成り立つ。
が濾過になること: が対称的・推移的であることを仮定する
- 定理の条件より、定義8の1,3は満たされている
- 定義8の2について:
- を仮定する。~の成立を示せば、がいえる。
- : かつを仮定する。後者とよりとなる。の方も同様。よってが成り立つ。
- : かつを仮定する。との対称性からであるから、これと後者よりとなる。の方も同様。よってが成り立つ。
- : かつを仮定する。との推移性からであるから、これと後者よりとなり、の任意性よりがいえる。の方も同様。よってが成り立つ。
- : との議論を組み合わせることで、同様に示される。
- を仮定すると、が成り立つので、2-2の条件が満たされる。
有限モデル性の証明
まず、濾過によって確かに世界の個数を有限個までに抑えられていることを確認する。
が有限集合ならば、モデルのによる任意の濾過に対して、が成り立つ(よっては有限のモデルである)。
ある関数を構成し、が単射になることを示せば、が示される。を以下のように定義する。
が単射になることを示すために、を任意にとり、を仮定する。を示すために、を仮定すると、任意のに対して以下が成り立つ。
このとき、同値関係の定義よりとなる(任意のに対してとなることは簡単に確かめられる)。よってとなり、最初の仮定に反する。以上よりは単射である。
この補題を用いると、有限モデル性は簡単に示せる。
に対しての反例モデルが存在すると仮定する。このとき、あるが存在してとなる。
とする。のによる濾過として、(たとえば)最も細かい濾過を与えると、
- は有限集合なので、上の補題より、は有限のモデルである
-
- は全てのフレームのクラスであることに注意(よって、として最も細かい濾過を与えていることに必然性はなく、何であれ1つ濾過を与えれば十分である)
- 定理1よりとなるので、はに対する反例モデルになっている
このようなモデルの存在より、は有限モデル性を満たすことが分かる。
定理2より、対称性・継続性・普遍性はもとのモデルから濾過へと引き継がれるので、の有限モデル性も同様に示される。
定理2が適用できないような論理に対しては、定理3を利用する。その例としての有限モデル性を示す。
の場合と濾過の与え方以外は同様である。濾過については、を以下のように定める。
このとき、定理3よりが対称的になるので、濾過はのモデルになる。
このように、~をうまく使えば、やなどの有限モデル性も同様に示される。ただし、この手法では、やの有限モデル性は示せない(ユークリッド性の扱いが難しい)。
決定可能性
有限モデル性は、決定可能性の証明に利用できるという点で「嬉しい」性質である。ただし、決定可能である(decidable)とは、体系内での論理式の真偽を判定する計算可能な手続き(アルゴリズム)が存在することである。本当は適当な計算理論を仮定して計算可能性について論じるべきであるが、今回は非形式的な「アルゴリズム」の概念を利用した説明に留める。
がで妥当であるかどうかを、以下2つの計算を並行して行うことで判定できる(一方が終了したら他方も終了することとする)。
- に対して健全かつ完全な証明体系(e.g. シーケント計算)によって、妥当式を枚挙する。枚挙された論理式の中にが出現したら、yesを出力して停止する。
- に出現する命題変項をと列挙する。そのうえで、に対して以下を計算する。
- とする
- を全て列挙する(個)
- として、以外には0を割り当てるようなものを全て列挙する(個)
- それぞれのに対して、以下を計算する
- 各に対して、を計算する(モデルの有限性より計算可能)。であったら、noを出力して停止する。
このように定まるアルゴリズムは、確かにがで妥当であるかどうかを判定している。実際、
- が妥当である場合: 手続き1によって妥当であることが判明するので、このとき確かに停止してyesを出力する。
- が妥当ではない場合: に対する反例モデルが存在するから、の有限モデル性より、に対する有限の反例モデルが存在する。手続き2によってこの反例モデルに相当するが見つかるので、このとき確かに停止してnoを出力する。
今回有限モデル性を示したその他の様相論理に対しても、同様の証明手法が適用できる (列挙されたが指定された性質を満たしているかどうかの判定をする計算を含めればよい)。