日記 (2025 年 2 月 26 日)

今回は、意味論の話を一度置いておいて、演繹体系の話に移ろうと思う。

まずは、演繹体系周りの用語と記号を確認しておこう。

定義 4.1.

式の集合を「理論 (theory)」という。

基本的に「理論」といった場合は、何らかの意味で正しいと思えるような式の集合を指す。特に、公理と推論規則から成る何らかの演繹体系において証明できる式全体の集合を指すことが多い。そこで、以降しばしば、演繹体系 󱁁 とその体系で証明できる式全体 Th(󱁁) を同一視する。以下の定義も、この同一視によるものである。

定義 4.2.

理論 󱁑 をとる。その元 A∈󱁑 を 󱁑 で「証明可能 (provable)」もしくは「定理 (theorem)」という。このとき、 ⊢󱁑A と書く。

スキーマ全体の証明可能性を論じることも多いので、そのための記号も用意しておこう。

定義 4.3.

理論 󱁑 をとる。スキーマ Σ に対して、任意の式 A∈Σ に対して A が 󱁑 で証明可能であるとき、 Σ 自身も 󱁑 で「証明可能 (provable)」であるという。このとき、 ⊢󱁑Σ と書く。

さて、我々は初回の 2 月 23 日に、様相論理における式を、命題論理の式に ◻ と ⬦ という 2 つの形の様相演算子を追加する形で定義した。この様相演算子の解釈には、「～というのは必然である」や「～ということは常識である」など様々あり、どのような解釈をするかによって成り立ってほしい定理は変わり得る。そのため、様相論理の演繹体系は様々あり、特に公理の選び方にいくつもの種類がある。そのようなもののうち、一旦我々が考えるのは、次で定義する正規性を満たす理論である。

定義 4.4.

理論 󱁑 と推論規則 Δ を考え、 Δ を A1 ⋯ An BΔ と書く。 Δ の仮定 A1,⋯,An が 󱁑 に属するならば、それに対応する結論 B も 󱁑 に属するとき、 󱁑 は Δ で「閉じている (closed)」という。

定義 4.5.

理論 󱁑 が、 3 条件

全ての命題論理的恒真式は 󱁑 に属する。
スキーマ K,Dual⬦ を、各式 A,B に対し、 KAB :≡ ◻(A⇀B)⇀(◻A⇀◻B) DualA⬦ :≡ ⬦A⥎¬◻¬A と定義するとき、これらはどちらも 󱁑 に含まれる。
推論規則 A A⇀B BMP A ◻ARN で 󱁑 は閉じている。

を満たすとする。このとき、 󱁑 は「正規 (normal)」であるという。

ここでも注意すべきなのは、正規な理論 󱁑 と式 A に対して、規則 RN により ⊨󱁑A ならば ⊨󱁑◻A が成り立つが、だからといって ⊨󱁑A⇀◻A が成り立つわけではない点である。後者は 󱁑 にかなり強い公理を加えない限り証明できない。

ここで、 2 月 24 日の意味論での議論を思い出そう。まず、正規な理論には命題論理的恒真式が全て含まれるが、命題 2.3 により、命題論理的恒真式は意味論的にも妥当である。また、正規な理論にはスキーマ K と Dual⬦ も含まれるが、命題 2.5 と命題 2.6 により、これらは意味論的にも妥当である。さらに、正規な理論は規則 MP と RN で閉じているが、命題 2.4 と命題 2.7 により、これらも意味論的に妥当である。そのため、厳密な証明は後で与えるが、この理論の健全性がこの時点で分かる。

正規性を満たす最小の演繹体系は K と呼ばれ、以降の議論のベースとなる。改めて定義しておこう。

定義 4.6.

演繹体系 K を、

公理は、全ての命題論理的恒真式と上記 K,Dual⬦ の全体とする。
推論規則は、上記 MP, RN とする。

で定める。

あらゆる命題論理的恒真式を公理に入れるのは若干乱暴ではあるが、様相論理の本質は様相なので、様相に関わらない部分の議論を省略するためにこのようにしている。これが気になる場合は、命題論理の全ての恒真式をちょうど導けるような公理系がいくつか知られているので、それだけを入れることにすれば良い。

この K は必要最低限の公理だけを入れたものなので、特定の様相演算子の解釈では成り立ってほしい式が証明できないことがある。特に、定義 3.1 にある D,T,B,4,5 はどれもこの公理だけからは証明できない。そこで、これらのうちいくつかを K に公理として追加した演繹体系も考えたく、そのために記号を用意しておこう。

定義 4.7.

スキーマ Σ1,⋯,Σn に対し、 K に Σ1,⋯,Σn の全体を公理として追加して得られる演繹体系を、 K[Σ1,⋯,Σn] で表す。

D,T,B,4,5 の追加の仕方は全部で 32 通りあるが、いくつかの追加方法は結局等価な演繹体系を与えるので、最終的に得られる異なる演繹体系はこれより少なく 15 種類であることが知られている。この 15 種類のうちで歴史的に重要なのが、 K[D],K[T],K[T,B],K[T,4],K[T,5] の 5 種類である。 K[D] は、様相を「～は義務である」と「～は許可されている」で解釈する義務論理のベースである。また K[T] は、様相を「～は必然である」と「～は可能である」と解釈する真理論理のベースである。 K[T,B] は、 Brouwer 様相論理と呼ばれてよく研究された。こう呼ばれてはいるが、 Brouwer との直接的な関係は薄いようである。最後の K[T,4] と K[T,5] は、それぞれ S4 と S5 とも呼ばれ、様相論理の黎明期に Lewis–Langford†3 が定式化したものと同型である。

さて、これで意味論と演繹体系の定義が終わったので、やはり気になるのは健全性, 完全性, 決定可能性である。この勉強ノートの一旦の目標をこれらを示すこととしよう。ただ次回はまず、最も弱い体系である K でどのような式が証明できるかを見ていくことにする。

参考文献

B. F. Chellas (1980) 『Modal Logic』 Cambridge University Press
P. Blackburn, M. de Rijke, Y. Venema (2001) 『Modal Logic』 Cambridge University Press
C. I. Lewis, C. H. Langford (1932) 『Symbolic Logic』 Dover