日記 (2025 年 3 月 6 日)
今回は、 様相論理版の de Morgan の法則を証明して、 様相式に対するその応用を考える。
まずは、 式の双対を定義しよう。
定義 7.1.
式 A に対して、 式 A∗ を次のように帰納的に定義する。
pn∗ :≡ ¬pn ⊤∗ :≡ ⊥ ⊥∗ :≡ ⊤ (¬A)∗ :≡ ¬A∗ (A∧B)∗ :≡ B∗∨A∗ (A∨B)∗ :≡ B∗∧A∗ (A⇀B)∗ :≡ B∗∖A∗ (◻A)∗ :≡ ⬦A∗ (⬦A)∗ :≡ ◻A∗
この A∗ を A の 「双対 (dual)」 という。
なお上記で、 式 A,B に対して、
B∖A:≡B∧¬A
と書いた。
すると、 de Morgan の法則は次のように述べられる。
式変形のための道具はすでにかなり揃っているので、 証明はただやるだけである。
命題 7.2.
正規な理論 をとる。
式 A に対し、
⊢A⥎¬A∗
が成り立つ。
したがって特に、
⊢A⟺⊢¬A∗
も成り立つ。
証明.
後半の主張は、 前半の主張と命題 5.1 から従う。
以降、 前半の主張を示す。
A の構造に関する帰納法による。
A≡pn のとき。
双対の定義によって示すべきは ⊢pn⥎¬¬pn であるが、 これは明らかに成り立つ。
A≡⊤ や A≡⊥ のときも、 同様に明らかに命題の主張は成り立つ。
A≡X∧Y のとき。
帰納法の仮定により、
⊢X⥎¬X∗⊢Y⥎¬Y∗
がともに成り立つ。
ここで、
⊢¬X∗∧¬Y∗⥎¬(Y∗∨X∗)
である。
上の 2 つの式と命題 6.2 を使うことでこの式の ¬X∗ と ¬Y∗ を書き換えることで、
⊢X∧Y⥎¬(Y∗∨X∗)
が得られる。
¬(X∧Y)∗≡¬(Y∗∨X∗) だから、 これがまさに示すべき主張である。
A≡X∨Y や A≡X⇀Y や A≡¬X のときも、 上記と同様に示される。
A≡◻X のとき。
帰納法の仮定により、
⊢X⥎¬X∗
が成り立つ。
これと命題 5.3 により、
⊢◻X⥎◻¬X∗♡
が分かる。
さて一方、 正規な理論が Dual⬦ を含むことから、
⊢⬦X∗⥎¬◻¬X∗
が成り立つ。
ここからは、 命題 5.1 などによって、
⊢◻¬X∗⥎¬⬦X∗
が分かる。
これと命題 6.2 によって、 主張 ♡ に含まれる ◻¬X∗ の部分を置き換えることで、
⊢◻X⥎¬⬦X∗
が得られる。
¬(◻X)∗≡¬⬦X∗ だから、 これがまさに示すべき主張である。
A≡⬦X のときも、 これと同様に示される。
これで全ての場合が尽くされたので、 命題の主張が示された。
この命題の応用として、 様相式の双対に関する主張を紹介しよう。
主張を述べやすくするために、 まず 「様相列」 という概念を導入する。
定義 7.3.
◻ もしくは ⬦ から成る有限の長さの列 (空でも良い) を 「様相列 (modality sequence)」 という。
定義 7.4.
様相列 φ に対し、 φ を構成している ◻ と ⬦ を入れ替えて得られる様相列を、 φ の 「双対 (dual)」 といって φ∗ で表す。
例えば、 ◻◻⬦ や ⬦◻⬦⬦◻⬦ などが様相列である。
これらの双対は、 それぞれ ⬦⬦◻ と ◻⬦◻◻⬦◻ である。
また、 様相列 φ と式 A に対し、 φ を構成する様相を右から順に A に適用して得られる式を φA と書くことにする。
例えば、 様相列 φ:≡◻◻⬦ に対し、 φA とはそのまま ◻◻⬦A のことである。
また、 任意の様相列 φ と式 A に対し、 (φA)∗≡φ∗A∗ となることにも注目したい。
様相列の双対については、 命題 7.2 によって以下の命題が成り立つ。
厳密性は欠けるが端的に言ってしまえば、 様相列 φ に対して、 φ と ¬φ∗¬ は同値な演算子だということである。
命題 7.5.
正規な理論 をとる。
様相列 φ と式 A に対し、
⊢φA⥎¬φ∗¬A
が成り立つ。
証明.
まず命題 7.2 によって、
⊢φA⥎¬(φA)∗
が成り立つ。
双対の定義から (φA)∗≡φ∗A∗ であるから、 これは
⊢φA⥎¬φ∗A∗
が成り立つということである。
さて、 命題 7.2 を命題 5.1 で少し変形することで、
⊢A∗⥎¬A
が得られるから、 これら 2 つの式に命題 6.2 を使うことで、
⊢φA⥎¬φ∗¬A
が示された。
この命題からは、 様相式から様相式への含意の形をしたスキーマがそれの (含意式としての) 双対と同値であることが分かる。
命題 7.6.
正規な理論 をとる。
様相列 φ,ψ に対し、 2 条件
- 任意の式 A に対し、
⊢φA⇀ψA
が成り立つ。
- 任意の式 A に対し、
⊢ψ∗A⇀φ∗A
が成り立つ。
は同値である。
証明.
条件 1 ⇒ 条件 2:任意に式 A をとる。
仮定から、
⊢φ¬A⇀ψ¬A
が成り立つ。
命題 7.5 と命題 6.2 により、
⊢¬φ∗¬¬A⇀¬ψ∗¬¬A
が得られる。
ここからは、 まず命題 5.1 により、
⊢ψ∗¬¬A⇀φ∗¬¬A
が分かる。
そして ⊢¬¬A⥎A であるから、 命題 6.2 により、
⊢ψ∗A⇀φ∗A
が示された。
条件 2 ⇒ 条件 1:こちら向きも上記とほぼ同様に示せる。
任意の式 A をとると、 仮定から、
⊢ψ∗¬A⇀φ∗¬A
が成り立つ。
命題 5.1 により、
⊢¬φ∗¬A⇀¬ψ∗¬A
が分かる。
命題 7.5 と命題 6.2 を使えば、
⊢φA⇀ψA
が示された。
さて、 2 月 25 日では、 重要なスキーマとして D,T,B,4,5 を紹介した。
改めてここで定義を確認しておくと、 各式 A に対して、
DA :≡ ◻A⇀⬦A TA :≡ ◻A⇀A BA :≡ A⇀◻⬦A 4A :≡ ◻A⇀◻◻A 5A :≡ ⬦A⇀◻⬦A
であった。
これらは全て、 様相式から様相式への含意の形をしている。
そこで、 それぞれの双対として、 スキーマ D†,T†,B†,4†,5† を、 各式 A に対して、
DA† :≡ ◻A⇀⬦A TA† :≡ A⇀⬦A BA† :≡ ⬦◻A⇀A 4A† :≡ ⬦⬦A⇀⬦A 5A† :≡ ⬦◻A⇀◻A
と定義しよう。
D だけその双対が自分自身と一致しているが、 それ以外は異なる形のスキーマが得られている。
しかし命題 7.6 により、 T を公理として追加することと T† を公理として追加することは結局同値である。
他のスキーマについても同じことが言える。
次回は、 ベースとなる演繹体系 K に対してスキーマ D,T,B,4,5 を追加するとどうなるかについて詳しく見ていく。
参考文献
- B. F. Chellas (1980) 『Modal Logic』 Cambridge University Press
- P. Blackburn, M. de Rijke, Y. Venema (2001) 『Modal Logic』 Cambridge University Press