Robert Goldblatt, Logics of Time and Computation, 2nd Ed.

Center for the study of language and information (CSLI), 1992年

---

はじめに

本書は数理論理学の理論計算機科学への応用についてコンパクトでありながらも最先端の高度な話題まで網羅している、この分野の標準的な教科書である。まず初めに、本書が対象としている分野の概説から始めたい。

数理論理学とは数学で行われる推論自体を新たな数学の分野とみなし探究する分野である。よくある説明としては、数学という学問全体をどんな人によっても、どんな時代においても反駁できないような絶対的で無矛盾な真理の体系として確立しようとするために生まれた学問であるというものがある（数学基礎論）。このような観点で数理論理学をみたとき、ヒルベルト・プログラム、『プリンキピア・マテマティカ』、ゲーデルの不完全性定理といった話題を欠かすことはできない。しかし、そのような観点については既に様々な人が膨大な文献で語ってきているので、ここでその話を繰り返すことはしない。ここでは、計算機科学において数理論理学がどのような役割を果たしているのかという観点で述べる

数理論理学は大きく分けると古典論理と非古典論理に分類できる。古典論理とは数学をするときに実際に使われている論理体系の一部を切り取って厳密に定義した論理体系であり、数学科の学生が数学をするうえで学ぶ必要があるのはこの古典論理である。数学科の学生であれば命題論理/述語論理を学ぶが、これらの用語は正確には古典命題論理/古典述語論理のことを指し、どちらも古典論理に分類される。これらの論理体系を学んで初めて数学における「証明」とはどのようなものであるか理解した数学科の学生も多いことだろう。例えば、微積分学の初歩で扱われるイプシロン・デルタ論法には多重量化$\forall\,\exists$が出てくるが、これらの記号は量化子とよばれ、述語論理がまさに扱う対象である。

一方で、ある意味では実際の数学とは直接関係のない論理体系は非古典論理に分類される。非古典論理はさらに直観主義論理、様相論理、その他の論理の三つに分類できる。ここで「その他の論理」には量子論理、多値論理、矛盾許容論理などが該当する。それぞれの非古典論理には命題論理と述語論理がある。例えば、直観主義論理には直観主義命題論理と直観主義述語論理があり、様相論理には様相命題論理と様相述語論理がある。一般的には、単に「～論理」と言えば「～命題論理」のことを意味する。非古典論理は実際の数学で使われている論理体系ではない。例えば、直観主義論理は排中律「$A$または$A$でない」や背理法が成り立たない論理体系だが、通常の数学で排中律や背理法が禁止されているわけではなく、自由にそれらを使ってよい。よって、直観主義論理は数学の論理体系としては不十分なのである。ただし、当然あえて不十分な論理体系を考える相応の理由はあり、興味のある読者は「構成的数学」というキーワードで調べてほしい。

さて、書評の話に戻るが、本書が扱っているのは非古典論理、特に様相論理の理論計算機科学への応用についてである。様相論理にも様々な下位区分があり、時相論理とよばれる様相論理は計算機科学におけるモデル検査の理論に、動的論理とよばれる様相論理は計算機科学におけるプログラム検証（ホーア論理など）の理論に使われている。この二つの様相論理が本書で扱われている主な対象である。一方で、認識論理とよばれる様相論理は計算機科学におけるマルチエージェントシステムの理論に使われているが、こちらについては本書では扱われていない。

本書の概要と各章へのコメント

本書は三部構成になっており、第一部は命題様相論理(Propositional Modal Logic)、第二部はいくつかの時相・計算論理(Some Temporal and Computational Logics)、第三部は一階動的論理(First-Order Dynamic Logic)となっている。ここで命題様相論理と様相命題論理は同じ意味であり、一階動的論理とは正確には一階の動的述語論理のことを指す。

第一部：命題様相論理

第一部では古典命題論理を予備知識として仮定したうえで、命題様相論理に関する基本事項が第一章から第五章までで簡潔に説明されている。具体的には、様相論理の構文論、クリプキ意味論、生成部分モデル、$p$射、クリプキフレームの到達可能性関係と様相論理式の対応理論、証明論、様相論理の各種公理系、カノニカルモデル、完全性定理、濾過法、決定可能性、複数様相(multimodal)の場合の構文論と意味論などである。これらの知識はどのような様相論理を使う上でも必須の知識であり、本書に限らず大抵の様相論理の教科書には記載がある。

一方で、残りの第六章と第七章では時相論理やクリプキ意味論に対して不完全な様相論理などが扱われており、これらの内容（特に第七章）はかなり高度である。本書を様相論理の教科書として使用する場合には、ひとまず第六章と第七章は飛ばして次の第二部に進んだ方がよいだろう。

第二部：いくつかの時相・計算論理

第二部でいよいよ本書のタイトルにもある時間と計算の論理についての説明が始まる。まず、第八章では第六章の内容をふまえた上で離散/連続時間の様相論理が扱われる。ここではクラスターやバルーン、そして完全性定理を証明するためのバルーン手術(balloon surgery)という興味深いモデル構成の方法が述べられる。しかし、計算機科学に様相論理がどのように応用されているのかを知りたい読者は第六章と第八章を読む必要はない。これらの章の内容はあくまでも哲学的/純粋論理学的に興味深い内容であり、計算機科学と直接の関係はない。計算機科学への応用を期待している読者が読むべきなのは、続く第九章と第十章である。

第九章の主題は時相論理である。ただし、（初学者にとっては大変紛らわしいが）第九章が扱う時相論理と第六章・第八章が扱う時相論理は全くの別物であり、両者は独立して読めるようになっている。第九章が扱う時相論理は時間の流れが線形あるいは分岐している場合の時相論理であり、それぞれ線形時相論理(Linear Temporal Logic, LTL)、計算木論理(Computational Tree Logic, CTL)とよばれる。これら二つの時相論理、すなわちLTLとCTLは計算機科学におけるモデル検査の分野で必須の知識でもあり、大抵のモデル検査の教科書にはLTLとCTLについての説明がある。本書は数理論理学の教科書なのでモデル検査に関する言及はほとんどないが、第九章の冒頭部分には並行/分散計算（システム）で必ず話題になるデッドロック、相互排他性、応答性などの重要な性質がどのような時相論理式で記述されるか簡単に言及されている。第九章で示される主要な結論は、LTLとCTLが本書で与えられる公理系に対して完全性定理を満たすこと、および工夫した濾過法によって決定可能性も示せることにある。

第十章の主題は動的論理である。より具体的には、前半で正規プログラム（正規表現と「テスト」からなるプログラム）を扱う通常の命題動的論理(Propostional Dynamic Logic, PDL)、後半でそれを拡張した並行動的論理(Concurrent Dynamic Logic, CDL)について述べられている。並行動的論理では並行に実行されるプログラムを扱える。第十章における主要な結論は第九章のそれと同様で、PDLとCDLは本書で与えられる公理系に対して完全性定理が示され、さらに工夫した濾過法によって決定可能性も示される。このように説明すると、完全性定理や決定可能性を示すことはさも簡単かのように錯覚するかもしれないが、実は世の中の多くの論理体系は完全性や決定可能性が示されていない。また、完全性/決定可能性が示されていないのではなく、いかなる方法でも完全性/決定可能性を示せない論理もあり、例えば一階の古典述語論理は完全だが決定可能ではない。従って、完全性定理や決定可能性が示せるということ自体に相当の驚きがあるということは強調しておきたい。

計算機科学の観点から完全性定理と決定可能性の意義を述べるなら次のようになる。まず、ある公理系を計算機上で実装できたと仮定しよう。このとき、計算機がその公理系に基づいて「証明」した結果は本当に信頼できるのだろうか。公理系の理論を実装に落とし込むうえで、何らかのバグが混入している可能性はないだろうか。完全性定理とは意味論（実装対象）と証明論（実装）の同等性を主張する定理であり、計算機が何らかの主張を「証明できた」と返すときその主張は確かに真である（健全性）ということと、計算機が「証明できない」と返すならその主張は確かに偽である（完全性）ということの二つを合わせて完全性定理とよぶ。ここで、「証明できない」とは「証明できるかもしれないが証明を思いつかなかった」ということではなく、「どれほど努力しても絶対に証明は発見できない」ことを意味する。また、決定可能性とは何らかの性質を満たしているかどうかを有限ステップで停止する手続き（アルゴリズム）によって判定できるということを指す。今回の文脈では、特に論理式の恒真性（証明可能性）が決定可能であると主張している。ただし、理論的に恒真性（証明可能性）を判定するアルゴリズムがあると証明できたとしても、それを有限の記号列しか扱えない現実の計算機で実装できるかという話はまた別問題である。多くの場合、それはうまくいかず、理論的なアルゴリズムの一部を実装することで満足せざるをえない。しかし、（予想に反するが）そのような中途半端な実装であっても、一部の現実世界の問題を解決するうえでは大変有益なのである。

第三部：一階動的論理

第三部は第十章で述べられたPDLを拡張した一階動的論理が扱われる。PDLを一階動的論理に拡張する主な動機はプログラムに現れる変数の全称/存在量化や代入を記述することにある。この段階に至って初めてホーア論理とよばれる計算機科学でプログラム検証に利用される論理体系との関連が明瞭になる。すなわち、一階動的論理とはホーア論理の拡張でもあり、ホーア論理では扱えないような様々なプログラムを扱えるようになる。つまり、通常のホーア論理では条件分岐プログラム(if-then-else)やwhileプログラム(while-do)などしか扱えないが、一階動的論理ではそれらのみならず、モデル検査で使用されるガード付きコマンド文やuntil文(repeat-until)なども扱えるようになる。ホーア論理が扱えるのは入力に対して出力が一意に定まるという意味で決定論的(deterministic)なプログラムだけだが、例えばガード付きコマンド文は非決定論的(non-deterministic)なプログラムである。ただし、本書ではホーア論理に関する言及はないので、動的論理とホーア論理の関係性については『コンピュータサイエンスにおける様相論理』（鹿島亮、森北出版）または“Dynamic Logic” (David Harel, Dexter Kozen, and Jerzy Tiuryn. MIT Press.)を参照してほしい。本章における主要な結論は、一階動的論理が本書で与えられる公理系に対して完全性定理を満たすということにある。残念ながら、第九章や第十章のように決定可能性まで示すことはできない。見方を変えれば、決定可能でない一階動的論理を扱いやすいように決定可能な部分に制限したのが第十章のPDLであるともいえる。実際、歴史的には最初に一階動的論理が考案され、その後PDLが誕生したという経緯がある。

本書全体に対するコメント

本書は様相論理（時相論理および動的論理）の計算機科学（モデル検査およびプログラム検証）への応用に関する標準的な教科書といってよいだろう。ただし、著者のGoldblattはあくまでも論理学者であり計算機科学者ではないため、論理学の教科書として書かれていることには注意が必要である。様相論理の計算機科学への応用について、計算機科学寄りの視点で学びたい場合は“Logic in Computer Science” (Michael Huth and Mark Ryan. Second Edition. Cambridge University Press.)を読むとよい

また、純粋論理学の観点からみても第七章や第八章には大変興味深い内容が書かれている。特に第七章ではクリプキ意味論に対して不完全な様相論理が述べられており、様相論理とクリプキ意味論（状態遷移系）が同等であるというよくある誤解を打ち砕いてくれるだろう。もちろん、クリプキ意味論に対して完全な様相論理は大変扱いやすいので、少なくともそのような扱いやすい部分があるという点が様相論理の利点であるという意見に異論はない。

一方で、本書の難点はコンパクトゆえに初学者向けではないという点である。例えば第一部では古典論理に関する説明がほとんど省かれている上に、それを前提にした様相論理の解説の部分も簡潔すぎて、これまで一度も様相論理の学習をしたことがない読者はついていくことが難しいだろう。より丁寧な様相論理の教科書（“Modal Logic: An Introduction” (Brian F. Chellas. Cambridge University Press.)など）を読んだ後で本書を読むとよい。

また、本書は一部で様相論理の高度な話題を扱っているとはいえ、様相論理自体を研究するためには大幅に内容不足である。様相論理自体の研究をしたい読者は“Modal Logic” (Chagrov and Zakharyaschev. Clarendon Press.)を読むべきである。

本書は読者の目的に応じて読む部分と読まない部分を分けるべきであり、一冊を通して読もうとすることは（よほど時間に余裕があるなら別だが）推奨しない。この本はコンパクトゆえに通読できそうに思うかもしれないが、動機や背景が大きく異なる分野（計算機科学への応用と純粋論理学）が一冊の中で扱われている上に密度が濃いため、そう容易ではない。

文献案内

ここでは様相論理に関する文献案内を行う。以下に挙げるいずれの文献も古典命題論理（できれば古典述語論理も）を前提知識としてもっておいた方がよいので、その知識が欠けている読者は『数理論理学』（鹿島亮、朝倉書店）や『数理論理学』（戸次大介、東京大学出版会）などをまず読むべきである。

初学者向け（和書）

まだ研究を始めていない/始めるつもりのない読者は和書から読み始めるのがよいと思われる。

『数学における証明と真理』（第一部、佐野勝彦、共立出版）：この本の第一部「様相論理入門」は様相論理を学ぶ誰もが知っておくべき内容を丁寧に網羅している。記述も大変分かりやすく、全てはこの本を読むことから始めるべきといっても過言ではない。第二部以降は高度な話題が含まれるため、読者の興味に応じて読むかどうか決めればよい。

『コンピュータサイエンスにおける様相論理』（鹿島亮、森北出版）：二冊目に読むとしたらこの本である。タイトル通り、計算機科学において重要な様相論理であるCTLやPDL、そして様相ミュー計算についての記述がある。さらに、動的論理とホーア論理の関係も扱っている。

以上が様相論理を専門に扱う和書である。様相論理が本全体のうちの一部のテーマとして扱われている本であれば他にもたくさんの和書がある。しかし、当然それらの（様相論理に関する）内容は上記の本よりも薄いので、基本的には上記の二冊だけ読めばよいだろう。

初学者向け（洋書）

洋書に抵抗のない読者は和書よりも以下に挙げる教科書を読むべきである。基本的に和書よりも洋書の方が丁寧な記述であり、扱っている内容も豊富である。

“Modal Logic: An Introduction” (Brian F. Chellas. Cambridge University Press.)：第一部の全てと第二部の第五章まででは様相論理を学ぶ誰もが知っておくべき内容を丁寧に網羅している。この本は評者が知っている様相論理の教科書のなかで最も基本的なレベルから説明が始まっているうえに、説明も最も丁寧である。第二部の第六章以降は高度な話題が含まれるため、読者の興味に応じて読むかどうか決めればよい。第六章の義務論理(deontic logic)や第十章の条件論理(conditional logic)では類書にはみられないテーマを扱っており、特に哲学の観点から様相論理に興味のある場合は読むとよい。第七章から第九章までは非正規様相論理および（現代でいう）近傍意味論を扱っており、計算機科学または純粋論理学の観点から様相論理に興味のある場合は読むとよい。また、本書には興味深くかつ有益な演習問題がたくさん掲載されている。時間はかかるが、これらの演習問題に取り組んだ暁には様相論理の研究を開始するための基礎体力が十全についていることだろう。

中級者向け

上記の初学者向けの本で挙げた本の内容を概ね理解したのであれば、下記に挙げる本に進むとよい。ここで挙げる本は、様相論理あるいは関連分野の研究を始めている/始めるつもりのある読者が読むべき本である。

“Modal Logic” (Patrick Blackburn, Maarten de Rijke, and Yde Venema. Cambridge University Press.)：本格的に様相論理の学習を開始するなら、この本から読むべきである。この本の特徴はその網羅性にあり、これまでに挙げてきたどの本よりも内容が濃い（ただし、重複していない話題も多いので大が小を兼ねるわけではない）。辞書的に読むべきというわけでもなく、いずれも様相論理を研究する上で必須に近い標準的内容である。特に第五章の様相論理の代数的意味論や第六章の様相論理の計算可能性/計算量の話題は重要である。

“Neighborhood Semantics for Modal Logic” (Eric Pacuit. Springer.)：この本は非正規様相論理およびその意味論である近傍意味論に特化した本である。ChellasのModal Logicの第七章から第九章までに興味をもった読者はこちらも読むとよいだろう。近傍意味論に関してはChellasの本よりも詳しく、類書にはない話題を取り扱っている。そして、この本はコンパクトにまとまっており、内容もさほど難解ではない（上記の初学者向けの本レベルの知識は要求される）ので、比較的短期間で読めるだろう。

“A New Introduction to Modal Logic” (M.J. Cresswell and G.E. Hughes. Routledge.)：この本は哲学の観点から様相論理に興味のある読者なら絶対に読むべきである。哲学と関連する話題として、厳密含意、確定記述、様相述語論理などに関する説明が詳しく載っている。これらの話題は言語分析哲学/分析的形而上学において重要なテーマだった時代もあり、哲学史を語る上では欠かせない。また、この本での記法や用語の使い方はかなり哲学者風であり、純粋論理/計算機科学の観点から様相論理を学んできた読者にとっては読みにくいだろう。ただし、記述が数学的に厳密でないわけではないので、その点は安心してよい。ところで、この本の出版より30年ほど前の1968年に同じ著者らが出版した“An Introduction to Modal Logic”という本があるが、こちらの内容は古すぎて現代人にとっては読むのが相当困難である（こちらについては和訳が出版されている）。一方で、様相論理の哲学史に興味のある読者は、こちらも読んでおくべきだろう。また、古いゆえに現代では忘れ去られているが重要な様相論理の概念も散見されるので、純粋論理の観点から様相論理に興味のある読者は読むとよいかもしれない。ところで、同じ著者らがこれら二冊の間（1984年）に出版した“A Companion to Modal Logic”という本もある。こちらは内容がコンパクトになっており、読む必要性は薄いかもしれない。

上級者向け

ここで挙げる本を読むべきなのは、純粋論理の観点から様相論理を研究する研究者である。

“Modal Logic” (Chagrov and Zakharyaschev. Clarendon Press.)：この本は類書に比べて極めて高度な話題を扱っている。この本の内容が概ね理解できれば様相論理の専門家と名乗っても誰も文句はいえないだろう（この意味で評者は様相論理の専門家ではない）。一方で、この本の前半部分は比較的理解が容易かつ様相論理として重要なテーマが扱われているため、できれば読んだ方がよい。直観主義論理と様相論理の関係、濾過法の種類、クリプキ意味論に対して不完全な様相論理、代数的意味論についての類書よりも詳細な説明は特に注目に値する。個々の様相論理ではなく、様相論理のクラスについて抽象的な議論を行う点にこの本の高度さがあり、様相論理という分野の奥深さに感心せざるにはいられない。自分がいかに無知な存在であるかを忘れないためにも入手して飾っておきたい一冊である。

“Tools and Techniques in Modal Logic” (Marcus Kracht. Elsevier.)：前述の教科書の難易度をさらに超えた難易度をもつ。この本を理解できる人は世界に何人いるのだろうか。評者はこの本よりも高度な話題を扱っている様相論理の教科書をみたことがない。こちらは代数的意味論に重きが置かれていることと、PDLについての独立した章があることが特徴である。また、序盤から高度に抽象的な議論が展開されており、第一章ですら最後まで読むことは困難である。

謝辞

久保埜雄大さんと渡部耀介さんには本書評の草稿に対する有益なコメントをいただきました。この場を借りて感謝申し上げます。

出版元公式ウェブサイト

Center for the study of language and information (CSLI)

http://web.stanford.edu/group/cslipublications/cslipublications/site/0937073946.shtml

評者情報

高木 翼（たかぎ つばさ）

現在、北陸先端科学技術大学院大学（JAIST）准教授。専門は理論計算機科学、特に数理論理学および形式検証。日本学術振興会特別研究員（東京工業大学）を経て現職。

Researchmap：https://researchmap.jp/takagitsubasa