1
大学数学基礎解説
文献あり

様相論理の有限モデル性について

754
0

代表的な様相論理の体系は、有限モデル性という行儀のよい性質を満たします。本稿では、この有限モデル性の証明に用いられる濾過法という手法を見ていきます。最後に補足として、有限モデル性と決定可能性との関係を説明します。

本稿の説明のベースとなっているのはThe Open Logic Projectの様相論理の教科書です。また、妥当性の定義などは大西『論理学』をもとにしています(説明の簡略化のため一部改変しています)。本稿が、これらの文献で説明されていることを自分用に嚙み砕いて書いたメモのようなものであることを予めご了承ください。詳細を知りたい方は参考文献を参照してください。

準備

以下では、様相論理の語彙は加算無限個の命題変項の集合PV¬,,からなるものとし、これにより帰納的に構成される論理式の集合をFmlとする。その他の通常の論理結合子は糖衣構文として定義する(e.g.A=def¬¬A)。

可能世界意味論

ここでは、(正規)様相論理のモデル論として、可能世界意味論(possible world semantics)というものを導入する。詳細な説明は行わないので、興味のある方には適宜教科書などを参照していただきたい。

フレーム

様相論理のフレーム(frame)とは、以下により定まる組W,Rのことである(以下では単に「フレーム」という)。

  • W: 非空な集合
    • これを可能世界(possible world)の集合という
  • RW2
    • これを到達可能性関係(accesibility relation)という
モデル

様相論理のモデル(model)とは、以下により定まる組W,R,vのことである(以下では単に「モデル」という)。

  • W,R: フレーム
  • v:W×PV{0,1}
    • これを付値(valuation)という
  • 付値の拡張: 付値vは以下のようにしてW×Fml{0,1}となるよう帰納的に拡張される
    • v(w,¬A)=1defv(w,A)=0
    • v(w,AB)=1defv(w,A)=1 and v(w,B)=1
    • v(w,A)=1defxW.wRxv(w,A)=1
妥当性

AFmlと、モデルM=W,R,v・フレームFについて、

  • MAdefwW.v(w,A)=1
    • このことを、AがモデルM上で妥当である(valid)という
    • これが成り立たないMAに対する反例モデル(counter model)という
  • FAdefv:(F).F,vA
    • このことを、AがフレームF上で妥当であるという

以下では、全てのフレームのクラスをFKとする。さらに、フレームの到達可能性関係に対して、以下のような制約を加えることを考える。

  • T: 反射性 (xW.xRx)
  • B: 対称性 (x,yW.xRyyRx)
  • D: 継続性 (xW.yW.xRy)
  • 4: 推移性 (x,y,zW.xRy and yRxxRz)
  • 5: ユークリッド性 (x,y,zW.xRy and xRzyRz)

これらの制約を加えて得られるフレームのクラスを、Kの後ろに対応するラベルを付けた名前で表す(e.g. FKTは反射的なRを持つモデルのクラス)。慣習的に、KT4,KT5をそれぞれS4,S5という。

このようにフレームの定義を変えると、妥当になる論理式も変わる。フレームのクラスに対応して定まる妥当な式の集合を論理として定める。

論理

フレームのクラスFKに対して、様相論理Kを任意のFFK上で妥当な論理式の集合とする。その他のフレームのクラスに対しても同様に論理を定める。

また、論理Λに対してAΛとなることを、AΛで妥当であるという。

有限モデル性

有限モデル性

論理Λを定義するフレームのクラスをFΛとする。Λ有限モデル性(finite model property)を満たすとは、以下が成り立つことである: 任意のAFmlに対して、Aに対するFΛ上の反例モデルが存在するならば、Aへの推論に対するFΛ上の有限の反例モデルが存在する

ただし、有限のモデルとは、モデルM=W,R,vであってWが有限集合であるものを指す。

有限モデル性を証明するためには、所与の推論に対する任意の反例モデルM=W,R,v(Wが無限集合でありうる)を、有限の反例モデルに変換する手続きを与える必要がある。より具体的には、Wの要素の個数を、反例モデルとしての性質を失わないように「減らす」ないし「圧縮する」必要がある。

そこで方針として有力なのは、適当な同値関係を定めてWの要素を「同一視」し、商集合W/を考えることで世界の個数を減らす、という方法である。このようなモデルの構成方法を濾過法 (filtration method)という。

同値関係を考えることで付値は自然に定められるが、到達可能性関係の定義はそこまで自明ではない。対象となる論理体系に応じてどのように到達可能性関係を設定するかが、有限モデル性の証明における焦点となる。

濾過法

定義

濾過法を定義するための道具立てとして、2つの概念を用意する。

ΓFmlについて、Γ部分論理式について閉じている(closed under sub-formulae)とは、以下が成り立つことである。
AΓ.sub(A)Γ
ただしsub(A)は、Aの部分論理式(A自身も含む)の集合を表す

モデルM=W,R,v、および部分論理式について閉じているΓFmlが与えられたとき、W上の同値関係Γを以下のように定める (これは確かに同値関係になる)
xΓydefAΓ.v(x,A)=1v(y,A)=1
以下では、この同値関係により定まる同値類を[w]のように(Γを明示せずに)表す

これらを用いて、モデルに対する「濾過」の仕様を以下のように定める。

濾過

モデルM=W,R,v、および部分論理式について閉じているΓFmlに対して、MΓによる濾過(filtration)とは、以下を満たすモデルM=W,R,vである

  1. W={[w]wW}
  2. 任意のx,yWに対して、
    1. xRy[x]R[y]
    2. [x]R[y](AΓ.v(x,A)=1v(y,A)=1)
  3. v([w],p)=v(w,p)

Rの定義は一見複雑であるが、2-1はRがwell-definedになるための条件であり、2-2は「Rに関するvの挙動を模倣すること」を要求していると(非形式的に)捉えることができる。

  • 濾過は一意に定まるとは限らない(「仕様」と書いたのはそのためである)。W,vは定義から一意に定まるが、Rの部分に自由度がある。
  • 本当はR,vがwell-definedになることの確認が必要であるが、割愛する。
  • 濾過は部分論理式について閉じているΓFmlに対してのみ定まる。よって、これ以降で「MΓによる濾過」と書いた場合、Γが部分論理式について閉じていることを(明示せずに)前提にすることがある。

前述のとおり、濾過を定義する動機は、反例モデルとしての性質を保ったまま世界の個数を減らすことであった。以下の定理は、濾過法はΓの範囲内では付値を変えないことを主張しており、「反例モデルとしての性質を保つ」という部分を保証している。

モデルMΓFmlによる任意の濾過M=W,R,vは以下を満たす。
AFml.wW.AΓ(v(w,A)=1v([w],A)=1)

Aの構成に関する帰納法で示す。Γは部分式について閉じているので、帰納法の各ステップで出現するAの部分式もまたΓの要素となることに注意する。

  • A=pPVの場合: 定義より明らか
  • A=¬B,A=BCの場合: 複合式に対する付値の定義を用いて部分式の条件へと分解し、帰納法の仮定を適用すればよい(詳細は割愛)。
  • A=Bの場合:
    v(w,B)=1xW.wRxv(x,B)=1[x]W.wRxv(x,B)=1()[x]W.[w]R[x]v(x,B)=1[x]W.[w]R[x]v([x],B)=1()v([w],B)=1

()の証明: ()については、仮定よりBΓ, v(w,B)=1であり、[w]R[x]を仮定すると、定義8の2-2からv(x,B)=1となるので成立。()については、定義8の2-1よりwRx[w]R[x]となるので成立。

まだ濾過の定義が与えられただけで、実際にそれが存在するかは分かっていない。以下では、一般的に構成できる2つの濾過の例を挙げる。

最も粗い・最も細かい

モデルM=W,R,vと部分論理式について閉じているΓFmlに対して、Wvを定義8の1,3の通りに定めたとき、

  • 最も細かい濾過は、Rを以下のように定義することで得られる
    [x]R[y]defx[x].y[y].xRy

  • 最も粗い濾過は、Rを以下のように定義することで得られる
    [x]R[y]defAΓ.v(x,A)v(y,A)=1

最も細かい濾過・最も粗い濾過は、どちらも実際に濾過になる。証明は割愛する。

到達可能性関係の性質

モデル中の到達可能性関係が持つ性質のうちの一部は、濾過に対してそのまま「引き継がれる」という特徴がある。

モデルMΓFmlによる任意の濾過M=W,R,vは以下を満たす。

  1. Rは反射的Rは反射的
  2. Rは継続的Rは継続的
  3. R=W2R=(W)2
    • R=W2となることをRが普遍的であるという。普遍的なフレームのクラスにより定まる論理はS5と一致することが知られている。

定義8の2-1(xRy[x]R[y])より、明らかに成り立つ。

この定理は、対称性・推移性などに対しては一般には成り立たない。しかし、Rをうまく「設計」することで、濾過にも同じ性質を引き継がせることができる。この「設計」のパーツとして必要なものをまずは定義する。

モデルM=W,R,vに対して、Wに関する2項述語を(メタレベルで)以下のように定義する。

  • C1(x,y)defAΓ.v(x,A)=1v(y,A)=1
  • C2(x,y)defAΓ.v(y,A)=1v(x,A)=1
  • C3(x,y)defAΓ.v(x,A)=1v(y,A)=1
  • C4(x,y)defAΓ.v(y,A)=1v(x,A)=1

ここで定義したC1C4に対しては、直観的な説明を与えることができる。

  • C1: 濾過の定義の2-2に該当する → 濾過となるために必要
  • C2: (ある意味で)C1の「逆」になっている→ 対称性を反映
  • C3: xAが成り立つなら任意の到達可能なyでもAとなるということなので、AAを意図したものになっている → 推移性を反映
  • C4: C2C3の両方を反映

以下の定理は、これらの説明を形式的に表現している。

モデルM=W,R,vと部分論理式について閉じているΓFmlに対して、W,vを定義8の1,3の通りに定めたとき、

  1. [x]R[y]C1(x,y) and C2(x,y) であるならば、以下が成り立つ
    • Rは対称的である
    • Rが対称的ならば、W,R,vMΓによる濾過である
  2. [x]R[y]C1(x,y) and C3(x,y) であるならば、以下が成り立つ
    • Rは推移的である
    • Rが推移的ならば、W,R,vMΓによる濾過である
  3. [x]R[y]C1(x,y) and C2(x,y) and C3(x,y) and C4(x,y) であるならば、以下が成り立つ
    • Rは対称的かつ推移的である
    • Rが対称的かつ推移的ならば、W,R,vMΓによる濾過である
  4. [x]R[y]C1(x,y) and C3(x,y) and C4(x,y) であるならば、以下が成り立つ
    • Rは推移的かつユークリッド的である
    • Rが推移的かつユークリッド的ならば、W,R,vMΓによる濾過である

(3)の証明のみ与える(その他の場合もだいたい同様である)。

  1. Rの対称性・推移性

    • 対称性: [x]R[y]を仮定する。定義よりC1(w,w)C2(w,w), C3(w,w)C4(w,w)であるから、明らかに[y]R[x]が成り立つ。
    • 推移性: [x]R[y],[y]R[z]を仮定する。[x]R[z]を示すためには、上で示した対称性より、C1(x,z)C3(x,z)を示せば十分である。
      • C1: v(x,A)=1を仮定する。これとC3(x,y)よりv(y,A)=1であり、これとC1(y,z)よりv(z,A)=1となるので、C1(x,z)が成り立つ。
      • C3: v(x,A)=1を仮定する。これとC3(x,y)よりv(y,A)=1であり、これとC3(y,z)よりv(z,A)=1となるので、C3(x,z)が成り立つ。
  2. W,R,vが濾過になること: Rが対称的・推移的であることを仮定する

    • 定理の条件より、定義8の1,3は満たされている
    • 定義8の2について:
      1. xRyを仮定する。C1C4の成立を示せば、[x]R[y]がいえる。
        • C1: AΓかつv(x,A)=1を仮定する。後者とxRyよりv(y,A)=1となる。の方も同様。よってC1(x,y)が成り立つ。
        • C2: AΓかつv(y,A)=1を仮定する。xRyRの対称性からyRxであるから、これと後者よりv(x,A)=1となる。の方も同様。よってC2(x,y)が成り立つ。
        • C3: AΓかつv(x,A)=1を仮定する。xRy,yRzRの推移性からxRzであるから、これと後者よりv(z,A)=1となり、zの任意性よりv(y,A)=1がいえる。の方も同様。よってC3(x,y)が成り立つ。
        • C4: C2C3の議論を組み合わせることで、同様に示される。
      2. [x]R[y]を仮定すると、C1(x,y)が成り立つので、2-2の条件が満たされる。

有限モデル性の証明

まず、濾過によって確かに世界の個数を有限個までに抑えられていることを確認する。

ΓFmlが有限集合ならば、モデルMΓによる任意の濾過M=W,R,vに対して、|W|2|Γ|が成り立つ(よってMは有限のモデルである)。

ある関数π:WP(Γ)を構成し、πが単射になることを示せば、|W||P(Γ)|=2|Γ|が示される。πを以下のように定義する。
π([w])=def{AΓw[w].v(w,A)=1}

πが単射になることを示すために、[x],[y]Wを任意にとり、[x][y]を仮定する。π([x])π([y])を示すために、π([x])=π([y])を仮定すると、任意のAΓに対して以下が成り立つ。
w[x].v(w,A)=1w[y].v(w,A)=1
このとき、同値関係Γの定義よりxΓyとなる(任意のAΓに対してv(x,A)=1v(y,A)=1となることは簡単に確かめられる)。よって[x]=[y]となり、最初の仮定に反する。以上よりπは単射である。

この補題を用いると、有限モデル性は簡単に示せる。

Kは有限モデル性を満たす。

AFmlに対してKの反例モデルM=W,R,vが存在すると仮定する。このとき、あるw0Wが存在してv(w0,A)=0となる。

Γ=sub(A)とする。MΓによる濾過M=W,R,vとして、(たとえば)最も細かい濾過を与えると、

  • Γは有限集合なので、上の補題より、Mは有限のモデルである
  • W,RFK
    • FKは全てのフレームのクラスであることに注意(よって、Mとして最も細かい濾過を与えていることに必然性はなく、何であれ1つ濾過を与えれば十分である)
  • 定理1よりv([w0],A)=0となるので、MAに対する反例モデルになっている

このようなモデルMの存在より、Kは有限モデル性を満たすことが分かる。

定理2より、対称性・継続性・普遍性はもとのモデルから濾過へと引き継がれるので、KT,KD,S5の有限モデル性も同様に示される。

定理2が適用できないような論理に対しては、定理3を利用する。その例としてKBの有限モデル性を示す。

KBは有限モデル性を満たす

Kの場合と濾過の与え方以外は同様である。濾過については、Rを以下のように定める。
[x]R[y]defC1(x,y) and C2(x,y)
このとき、定理3よりRが対称的になるので、濾過MKBのモデルになる。

このように、C1C4をうまく使えば、K4S4などの有限モデル性も同様に示される。ただし、この手法では、K5KD5の有限モデル性は示せない(ユークリッド性の扱いが難しい)。

決定可能性

有限モデル性は、決定可能性の証明に利用できるという点で「嬉しい」性質である。ただし、決定可能である(decidable)とは、体系内での論理式の真偽を判定する計算可能な手続き(アルゴリズム)が存在することである。本当は適当な計算理論を仮定して計算可能性について論じるべきであるが、今回は非形式的な「アルゴリズム」の概念を利用した説明に留める。

Kは決定可能である。

AFmlKで妥当であるかどうかを、以下2つの計算を並行して行うことで判定できる(一方が終了したら他方も終了することとする)。

  1. Kに対して健全かつ完全な証明体系(e.g. シーケント計算)によって、妥当式を枚挙する。枚挙された論理式の中にAが出現したら、yesを出力して停止する。
  2. Aに出現する命題変項をp1,,pkと列挙する。そのうえで、n=1,2,に対して以下を計算する。
    • W={0,,n1}とする
    • RW×Wを全て列挙する(n2個)
    • v:W×PV{0,1}として、p1,,pk以外には0を割り当てるようなものを全て列挙する(2k個)
    • それぞれのv,Rに対して、以下を計算する
      • wWに対して、v(w,A)を計算する(モデルの有限性より計算可能)。v(w,A)=0であったら、noを出力して停止する。

このように定まるアルゴリズムは、確かにAFmlKで妥当であるかどうかを判定している。実際、

  • Aが妥当である場合: 手続き1によって妥当であることが判明するので、このとき確かに停止してyesを出力する。
  • Aが妥当ではない場合: Aに対する反例モデルが存在するから、Kの有限モデル性より、Aに対する有限の反例モデルが存在する。手続き2によってこの反例モデルに相当するW,R,vが見つかるので、このとき確かに停止してnoを出力する。

今回有限モデル性を示したその他の様相論理に対しても、同様の証明手法が適用できる (列挙されたRが指定された性質を満たしているかどうかの判定をする計算を含めればよい)。

参考文献

[1]
The Open Logic Project, Boxes and Diamonds: An Open Introduction to Modal Logic, 2019
[2]
大西琢朗, 論理学, 3ステップシリーズ, 昭和堂, 2021
投稿日:2022329
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

⊥
25
8593

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中
  1. 準備
  2. 可能世界意味論
  3. 有限モデル性
  4. 濾過法
  5. 定義
  6. 到達可能性関係の性質
  7. 有限モデル性の証明
  8. 決定可能性
  9. 参考文献