ipc_botの解説 決定版!

ipc_bot とは

ipc_bot は2023年5月までTwitter (現: X) で稼動していたbotで、「直観主義命題論理」と呼ばれる問題を自動で解いてくれるbotです。

https://twitter.com/ipc_bot

現在はXの読み取り系のAPIが有料化されたことから、Mastodonにお引っ越ししています。(Misskey等の他のActivityPub実装からも利用できます)

https://qnmd.info/@ipc_bot

使い方

直観主義命題論理の式をテキストで表記してメンションすると、結果が画像で返信されます。以下のような具合です。

@ipc_bot ~~(((P -> Q) -> P) -> P)

Mastodonの場合はリモートからのメンションになるため、サーバー名をつける必要があります。

@[e-mail] ~~(((P -> Q) -> P) -> P)

命題の書き方と結果の読み方

命題

「命題 (proposition)」とは、ありていに言えばbool型の式のようなものです。ただし、それが具体的に計算可能である必要はありません。重要なことは、その式の評価値の真理性(真か偽か)を議論することができるという点です。

ipc_botが対象としているのは「命題論理 (propositional calculus)」における命題であるため、実際に入力できるのは「命題変数同士の演算によって作られる命題」に限られます。一般的なプログラミングに照らし合わせると、これはbool変数の &&, ||, ! によって作られる式のようなものだと言えます。

ただし、ipc_botは古典論理ではなく直観主義論理 (intuitionistic logic) を対象にしているため、利用される基本演算は若干異なります。

直観主義論理の基本演算は以下の5種類です。

• 2個の命題の連言 $P \land Q$。これは P && Q に相当。
• 0個の命題の連言 $\top$。これは定数 true に相当。
• 2個の命題の選言 $P \lor Q$。これは P || Q に相当。
• 0個の命題の選言 $\bot$。これは定数 false に相当。
• 含意演算 $P \to Q$。これは古典論理では !P || Q に相当。

否定 $\lnot P$ は含意を用いて $P \to \bot$ とあらわされます。わざわざ含意を先に定義しているのは、直観主義論理においては否定から含意を作ることができないからです。古典論理では $\lnot P \lor Q$ とあらわせますが、直観主義論理ではこれは $P \to Q$ とは異なる意味になってしまいます。

命題の書き方には様々なバリエーションがありますが、ipc_botではよく知られた記法の多くを受け付けるようになっています。詳しくは字句解析器の実装を参考にしてください。

妥当性と充足可能性

命題論理には量化子がない^[1]ため、基本的には開論理式 (変数が残った状態の論理式) を考えることになります。開論理式に関する代表的な問題は以下の2種類です:

• 妥当性 (validity): その論理式が常に正しいといえるかを考える。 (トートロジーともいう)
• 充足可能性 (satisfiability): 変数の解釈次第で、その論理式を正しくする余地があるかを考える。

ipc_botが解くのは前者の「妥当性」の問題です。

証明図

未知の論理体系に対して、命題の正しさを定義する代表的な方法は2種類あります:

• 証明図による定義
• 意味論による定義

証明図による定義では、「その命題を結論とするような証明図が存在する」ことをもって命題が正しいとみなします。そのため、この方法は命題が妥当であることの証明に最適です。

通常、証明図によって妥当と証明されたならば、意味論上でも妥当であることが期待されます。これは 健全性 (soundness) といいます。健全性の逆は 完全性 (completeness) と呼ばれ、こちらは健全性ほど簡単には成り立ちませんが、なるべく成立してほしい性質です。健全性と完全性が成り立てば、証明図による定義と意味論による定義は同じものだとみなせます。これは組合せ最適化における弱双対性と強双対性の関係にも似ています。

証明図の体系にもいくつかの流儀があり、多くは以下の3種類に分類されます:

• 自然演繹 (natural deduction)
• 推件計算 (シークエント計算; sequent calculus)
• Hilbert計算 (Hilbert calculus)

ipc_botが出力する証明図は 自然演繹 (natural deduction) ベースの規則に従っています。実は、直観主義命題論理の自然演繹システムは、単純型つきラムダ計算との対応関係があることが知られています。(このような対応関係を一般にCurry-Howard対応といいます)

推件

自然演繹のルールを記述するには、「推件 (sequent)」と呼ばれる記法が使われます。^[2] 推件とは、前提となる論理式と帰結となる論理式を並べたもので、前提部分 (前件; antecedent) と帰結部分 (後件; succedent) を結ぶ記号には $\vdash$ が使われます。

ipc_botにおいては、前件は複数個(0個以上)の命題からなり、後件はちょうど1個の命題からなります (これは直観主義論理で広く採用される規則です)。たとえば以下が推件の例です。

$$P, P \to Q \vdash Q$$

自然演繹システムの目標は、与えられた命題 $P$ に対して $\vdash P$ という推件をルールから導出することにあります。これができれば $P$ は妥当であり、そうでなければ $P$ は妥当ではないということになります。

ある推件をルールから得るには、そのメタ的な前提条件として、別の推件を先に導出しておく必要があります。その場合、その推件の上に横棒を書き、その上に前提となる推件を書きます。もし、前提条件が必要ない場合は、その横棒の上には何も書く必要はありません。逆に、前提が複数個必要な場合は、それを全て記載する必要があります。これをすべての推件の導出が決まるまで繰り返すと、推件同士が木構造をなします。これが自然演繹システムにおける「証明図」です。

ルール

ipc_botで使われている自然演繹システムのルールはおおむね以下の通りです。横棒の上に書かれている推件が全て成立するならば、下の推件も成立するというルールです。

凡例

• $P$, $Q$, $R$ ... 命題をあらわすメタ変数。
  • つまり、以下のルール中で $P$, $Q$, $R$ が出現する箇所は、任意の命題に置き換えて適用することが許されています。 $P$, $Q$, $R$ という名前の具体的な原子命題 (命題変数) を指しているわけではないので気をつけてください。
• $\Gamma$ ... 複数の命題(0個以上) をあらわすメタ変数

仮説の適用 (別名: 変数、公理など)

$$\frac{}{\Gamma \vdash P} \quad (P \in \Gamma)$$

2項連言の導入

$$\frac{\Gamma \vdash P \qquad \Gamma \vdash Q}{\Gamma \vdash P \land Q}$$

0項連言の導入

$$\frac{}{\Gamma \vdash \top}$$

2項連言の除去(左)

$$\frac{\Gamma \vdash P \land Q}{\Gamma \vdash P}$$

2項連言の除去(右)

$$\frac{\Gamma \vdash P \land Q}{\Gamma \vdash Q}$$

0項連言の除去 -- なし

2項選言の導入(左)

$$\frac{\Gamma \vdash P}{\Gamma \vdash P \lor Q}$$

2項選言の導入(右)

$$\frac{\Gamma \vdash Q}{\Gamma \vdash P \lor Q}$$

0項選言の導入 -- なし

2項選言の除去

$$\frac{\Gamma \vdash P \lor Q \qquad \Gamma, P \vdash R \qquad \Gamma, Q \vdash R}{\Gamma \vdash R}$$

0項選言の除去 (別名: 爆発律 (absurdity))

$$\frac{\Gamma \vdash \bot}{\Gamma \vdash P}$$

含意の導入

$$\frac{\Gamma, P \vdash Q}{\Gamma \vdash P \to Q}$$

含意の除去

$$\frac{\Gamma \vdash P \to Q \qquad \Gamma \vdash P}{\Gamma \vdash Q}$$

前件の省略

自然演繹システムには、木構造を上(子孫側)に辿るほど前件が増える (減ることはない) という特徴があります。木構造のある位置に期待した前件があるかどうかを知るには、それに対応する規則が使われているかどうかを調べるだけで済むため、わざわざ前件を表記しなくても証明図を読むことは可能です。

そこで、ipc_botでは、実際には推件全体を表記せず、後件部分だけを表記した証明図を採用しています。

たとえば、 $P, Q \vdash P \land Q$ という推件の場合、単に後件部分だけをとって $P \land Q$ と表記します。かわりに、前件中にある命題を利用する箇所では、使おうとしている命題がどのルールから来ているかを番号で対応づけて表記しています。

意味論

証明図を使った定義では、命題そのものを解釈することなく、外部的なルールを与えることで妥当性を定義していました。いっぽう、命題に具体的な値を入れることで妥当性や充足可能性を考えることもできます。このように命題の解釈を与える方法論を 意味論 (semantics) と呼びます。

意味論による定義では、「どのように解釈しても結果が真値になる」ことをもって命題が正しいとみなします。そのため、この方法は命題が妥当ではないことの証明に最適です。

直観主義論理にはさまざまな意味論があります。特に、直観主義論理は古典論理と異なり、命題だけではなく証明の意味も無理なく解釈することが可能という特徴があります (たとえば、ラムダ計算の式であると解釈すれば、それらが同じ振る舞いをするかどうかを考えることができる)。

ただし今回のように妥当性の反証をするという目的ではこういった 証明関連的 (proof-relevant) な意味論を使う必要はありません。逆に 証明無関連的 (proof-irrelevant) な意味論に限ると、代表的な意味論は以下の2種類です。

• Heyting代数意味論
• Kripke意味論

ipc_botは、命題が妥当でない場合は、Kripke意味論にもとづく反例の出力を試みます。

Heyting代数意味論とKripke意味論の関係

論理体系が証明図のルールとして与えられたとき、その論理体系を最もよく表現している代数の体系を考えることができます。これをLindenbaum-Tarski代数といいます。これは以下のような対応によって代数を考える方法論です。

• 論理式(の同値類) → 代数の元
• 論理結合子 → 代数の演算
• 証明規則 → 代数の演算が満たすべき性質

こうして得られた代数は、その論理の意味論として使用することができ、ある意味では(証明無関連的な意味論の中では)その論理を最も素直に表現した意味論であると考えることができます。この意味論はたいてい完全性を満たします。

そして、Heyting代数は直観主義論理のLindenbaum-Tarski代数であると考えることができます。

そのHeyting代数とKripke意味論との関係を説明するには、まずBoole代数を先に説明するのがよいでしょう。

Boole代数は古典論理のLindenbaum-Tarski代数です。ありていに言うと、 $\land$, $\top$, $\lor$, $\bot$, $\lnot$ の5つの演算を持つ代数的構造です。

もっとも代表的なBoole代数は $\{0, 1\}$ に所定の演算を入れたもの (二元Boole代数) で、これは多くのプログラミング言語で bool 型や boolean 型として知られています。しかし、数学的な意味でのBoole代数はこれには限られません。たとえば、以下のような集合にもBoole代数の構造を入れることができます。

• $\{0\}$
• $\{0, a, b, 1\}$

このように例を挙げると、勘のよい読者であれば「実は、 $2^n$ 要素の集合のみがBoole代数になりえるのではないか」と思われるかもしれません。これはほぼ正しく、Boole代数は有限のものに限っていえば $2^n$ 要素のものしか存在しません。このことを正確に説明したのがBoole代数に関するStoneの表現定理です。これは簡略化すると以下のように説明できます:

定理 (Stoneの表現定理; 簡易版). 任意のBoole代数は、ある位相空間の開閉集合全体がその包含関係に関してなすBoole代数と同型である。特に、任意の有限Boole代数は、ある集合の羃集合がその要素同士の包含関係に関してなすBoole代数と同型である。

これにより、Boole代数の構造を、別のよく知られた構成で説明することができるようになります。

さらにBoole代数の場合、「冪集合は2元Boole代数の直積であるため、妥当でない命題の反証には実は2元Boole代数だけあれば十分である」といった趣旨の議論が展開できます (実際には無限の場合も考慮してBPIを使った議論をする必要がある)。一般的に2元Boole代数がBoole代数の代表例として扱われる背景にはこのような事実が隠されています。

さて、Heyting代数に話を戻します。Heyting代数にも、Stoneの表現定理の一般化が成立します。一般の場合については複数の定式化がありますが、ここでは有限の場合に対する定理であるBirkhoffの表現定理を扱います。なお、Birkhoffの表現定理の説明では「分配束 (distributive lattive)」の語が出てきますが、有限の場合に限ればHeyting代数と同義です (特殊随伴関手定理のさらに特殊な場合ともいえる)。

Birkhoffの表現定理でも、Heyting代数を別の集合の部分集合の族に対応させることを考えます。しかし、Stoneの定理で全ての部分集合の族を考えたのとは異なり、Birkhoffの定理では特定の「よい性質」を満たした部分集合だけを考えます。そのために、台集合には半順序を入れておきます。 (この半順序は、台集合をprime filterの集合として構成するさい、prime filter同士の包含関係から導出されます) あとは同じように、その半順序の全ての下方閉な集合の族が元のHeyting代数と同型になることが示されます。

直観主義論理のKripke意味論では(様相論理のそれとは異なり)、遺伝的 (hereditary) な真理値関数のみを命題の解釈として考えます。これは、Birkhoffの表現定理で下方閉な集合のみを考えることと対応しています。直観主義論理のKripke意味論で命題がとりうる真理値関数の集合は、実はそのままHeyting代数になっているというわけです。

Kripke意味論

Kripke意味論は、様相論理の意味論としてよく用いられる枠組みですが、直観主義論理の意味論としても使うことができます。構文レベルでも、直観主義論理は様相論理のひとつであるS4へ埋め込むことが可能であり、それを意味論で対応させたのが直観主義論理のKripke意味論であると考えることもできます。

Kripke意味論の基本的な考え方はこうです。通常の古典論理では、命題の真偽はその命題にあらわれる変数の状態にのみ依存して決まります。しかし様相論理では、命題は何らかの暗黙的な状態に依存して真偽が変化します。その状態が何であるかは場合によって異なりますが、たとえば時相論理であれば時間であったり、共有知識に関する論理であれば、異なる知識を持つ各々のエージェントが状態にあたると考えられます。数学的には、真理値が単一のスカラー値ではなく、こういった状態によってパラメーター化された関数で解釈されることになります。

様相論理の用語では、この暗黙の状態のことを「可能世界 (possible world)」といいます。数学的には単なる集合です。

可能世界同士は干渉します。干渉しなければ、個々の可能世界上の真理値を独立に解釈したものと同じで、自明な結果しかもたらさないたしめ、これはある意味当然です。可能世界同士の干渉関係は 到達可能関係 (accessibility relation) と呼ばれますが、これは数学的には単に可能世界全体の集合上の二項関係です。「可能世界の集合」と「到達可能関係」をあわせてKripkeフレームと呼びます。Kripkeフレームによって、Kripkeモデルにおける命題の解釈(真理値)の空間が定まります。

直観主義論理の意味論を考えるときは、到達可能関係は擬順序関係であるという制約を課します。そのため、Kripkeフレームは擬順序集合です。完全性を損なわずに半順序集合に制限することもできるので、以降はそのように考えてもらってもかまいません。

たとえば、2つの可能世界 $\{W_0, W_1\}$ を考えて、以下のように到達可能関係を定めます。

• $W_0 \leadsto W_0$
• $W_0 \leadsto W_1$
• $W_1 \leadsto W_1$

これは半順序集合をなすので、Kripkeフレームとして使うことができます。

Kripkeフレームを決めたら、命題に真理値 $\llbracket P \rrbracket$ を割り当てていきます。

まず、原子命題 (命題変数) の真理値は自由に割り当てることが可能です。妥当性を検証しようとしているため、そのような割り当て方のうちひとつでも真にならなければ、反例として使えることになります。

とはいえ、完全に自由なのではなく、遺伝的 (hereditary) という条件を満たす必要があります。これは、「ある世界で真な命題は、そこから到達可能な世界でも真である」というものです。つまり、先ほどの例では、割り当て可能な真理値の組み合わせは以下の3通りということになります。

• $\llbracket P \rrbracket_{W_0} = 0$, $\llbracket P \rrbracket_{W_1} = 0$
• $\llbracket P \rrbracket_{W_0} = 0$, $\llbracket P \rrbracket_{W_1} = 1$
• $\llbracket P \rrbracket_{W_0} = 1$, $\llbracket P \rrbracket_{W_1} = 1$

原子命題の真理値割り当てが決まると、残りの命題の真理値はそこから自動的に決まります。それは以下の通りです。

$$\llbracket P \land Q \rrbracket_W = \min\{\llbracket P \rrbracket_W, \llbracket Q \rrbracket_W\}$$

$$\llbracket \top \rrbracket_W = 1$$

$$\llbracket P \lor Q \rrbracket_W = \max\{\llbracket P \rrbracket_W, \llbracket Q \rrbracket_W\}$$

$$\llbracket \bot \rrbracket_W = 0$$

$$\llbracket P \to Q \rrbracket_W = \min \{ \max \{ 1 - \llbracket P \rrbracket_{W'}, \llbracket Q \rrbracket_{W'} \} \mid W \leadsto W' \}$$

このうち、連言 ($\land$, $\top$) と選言 ($\lor$, $\bot$) はシンプルで、単に可能世界ごとに真理値計算をしているだけです。重要なのは含意 ($\to$) の計算です。これは、まず可能世界ごとに $\lnot P \lor Q$ 相当の計算をしてから、それが各世界から到達可能な全ての可能世界で成立するかどうかを計算しています。これによって古典論理とは異なる結果が発生することになります。

こうしてボトムアップに真理値を計算していき、最後に所望の命題の真理値を計算します。命題が妥当であれば、この時点でどの可能世界でも $1$ が代入されているはずです。もし、そうならなければ、その真理値割り当てが命題の妥当性に対する反例ということになります。

実装のありか

現行版は以下に置いてあります。OCamlで書かれています。

https://github.com/qnighy/ipc_solver

次期版(開発停止中)は以下にあります。Rustです。

https://github.com/qnighy/logic-solver-rs

計算量

一般論

一般的に、数理論理学のこのような問題は、条件を慎重に制限しない限り $\mathbf{R}$ や $\mathbf{RE}$ に入るか入らないか、あるいはそれ以上の問題まで複雑化してしまうことが多いです。そこで最もよく使われるのが「命題論理への制限」で、これにより複雑性はかなり軽減されます。

もし完全性を持つ証明体系がある場合(その他いくつかの仮定をおけば)、妥当性を $\mathbf{RE}$ に収めることができます (つまり半決定可能です)。たとえば一階述語論理はこれに該当します。いっぽう、二階述語論理の標準意味論ではこのような議論が適用できません。

もし意味論が有限モデル性質を持つのであれば(その他いくつかの仮定をおけば)、その体系は $\mathbf{R}$ です (決定可能です)。

古典命題論理

古典命題論理の妥当性は、充足可能性のde Morgan双対^[3]になっているため、co-NP完全です。

なお、co-NPになるのはモデルサイズが多項式サイズに抑えられるという特殊な事情によるもので、一般にはあまり成り立たないと考えられます (たとえばS5などでは成り立つ)。逆に妥当性判定がNP完全になる例として、線形命題論理の乗法断片などがあります。

直観主義命題論理

直観主義命題論理の妥当性はPSPACE完全であることが知られています。

証明アルゴリズム

ipc_botではまず証明図にもとづいて証明可能性を調べます。この時点で妥当か否かが確定します。妥当である場合はそこから証明図が構成されます。

証明探索の一般論: 推件計算

証明探索は推件計算をベースに行われることが多いです。

推件計算は自然演繹と同じく、推件に対して規則を適用していくことで推論を進めますが、自然演繹とは大きく異なる特徴があります。それは、除去規則のかわりに、左導入規則と呼ばれる別の規則を用いて推論するという点です。

たとえば、以下は直観主義論理の自然演繹システムにおける連言の除去規則です。

$$\frac{\Gamma \vdash P \land Q}{\Gamma \vdash P}$$

$$\frac{\Gamma \vdash P \land Q}{\Gamma \vdash Q}$$

一方、推件計算ではたとえば以下のような左導入規則をかわりに使います。

$$\frac{\Gamma, P, Q \vdash R}{\Gamma, P \land Q \vdash R}$$

左導入規則の特徴は、規則の下から上に向かって推件が小さくなる方向に進むことです。たとえば、命題の重み関数 $|\bullet|$ を $|P \land Q| = |P| + |Q| + 1$ となるように定義し、推件の重みを命題の重みの和と定義すれば、実際に推件の重みが小さくなる方向に進みます。証明探索では規則を下から上に向かって適用しながら探索するため、各ステップで重みが小さくなることが探索アルゴリズムの肝になっています。

他の導入規則も同様に重みが小さくなるように定義できるのですが、そうならない重要な規則が2つあります。それは以下の2つです。

• 切断規則 (カット規則; cut rule)
• 縮約規則 (contraction rule)

切断規則

切断規則は以下のような規則です。ポイントは規則の上側にある $A$ が対になることで下側では消滅している点です。

$$\frac{\Gamma \vdash A \qquad \Delta, A \vdash B}{\Gamma, \Delta \vdash B}$$

これは、以下の「公理」と呼ばれる規則の対になる規則であると言えます。こちらは、規則の下側で$A$ が対になって出現しています。

$$\frac{}{A \vdash A}$$

Lindenbaum-Tarski代数を構成する上では、「公理」が反射律を保証するのに対し、切断規則は推移律を保証します。また、proof netでは、「公理」がネットワークに上から蓋をするコネクタであるのに対し、切断規則はネットワークを下から塞ぐコネクタに対応します。

切断規則は、プログラミング言語におけるlet式とも類似します^[4]。let式で作られた変数は、利用箇所で式を展開すれば消すことができます (パフォーマンスや読みやすさは悪化するかもしれません)。同様に、証明中で使われている切断規則も、展開して解消することができます (論理体系によっては成立しません)。これを切断除去定理 (カット除去定理)といいます。

切断除去定理があるため、証明探索時は切断規則を使わずに探索してよいことになります。

縮約規則

いっぽう、縮約規則は構造規則とよばれる規則群のひとつで、以下のような規則です。

$$\frac{\Gamma, A, A \vdash B}{\Gamma, A \vdash B}$$

これは、導入した仮説を2回以上使ってもよいことを保証します。これは逆に仮説を使わなくてもよいことを保証する以下の規則 (弱化規則) との対応関係にあります:

$$\frac{\Gamma \vdash B}{\Gamma, A \vdash B}$$

証明探索においては、切断規則に加えて、縮約規則も問題になります。そこで、証明探索においては、全ての前件の命題^[5]が暗黙的に縮約・弱化されたものと仮定して、実際には推件中での複製・削除を行わずに探索します。

このような仮定を置くためには、他の規則を注意深く選ぶ必要があります。実は、推件計算に登場する規則の多くには、乗法的な規則と加法的な規則の2種類の亜種が存在します。

たとえば、 $\land$ の右導入規則の乗法的な亜種は以下のように記述されます。

$$\frac{\Gamma \vdash A \qquad \Delta \vdash B}{\Gamma, \Delta \vdash A \land B}$$

いっぽう、同じ右導入規則の加法的な亜種は以下のように記述されます。

$$\frac{\Gamma \vdash A \qquad \Gamma \vdash B}{\Gamma \vdash A \land B}$$

また $\land$ の左導入規則の乗法的な亜種は

$$\frac{\Gamma, A, B \vdash C}{\Gamma, A \land B \vdash C}$$

なのに対し、加法的な亜種は

$$\frac{\Gamma, A \vdash C}{\Gamma A \land B \vdash C}$$

$$\frac{\Gamma, B \vdash C}{\Gamma A \land B \vdash C}$$

と書かれます。

縮約規則と弱化規則を不要にするには、以下のように亜種を選ぶ必要があります。

• 連言 ($\land$, $\top$) ... 加法的な右導入規則と乗法的な左導入規則
• 選言 ($\lor$, $\bot$) ... 乗法的な右導入規則と加法的な左導入規則
• 含意 ($\to$) ... 選言と同様だが、面倒な事情がある (後述)
• 「公理」 ... 加法的な規則

このように規則を選ぶと、縮約除去定理が成立します。縮約除去はカット除去と両立します。

なお、あえて縮約除去が成り立たない規則の組み合わせを選んだ上で縮約規則や弱化規則を取り除くと、古典論理や直観主義論理ではなく、部分構造論理という種類の論理体系が得られます。たとえば、線形論理には乗法的連言・乗法的選言・加法的連言・加法的選言という4種類の論理結合子が出てきますが、乗法的な結合子は乗法的な導入規則で定義され、加法的な結合子は加法的な導入規則で定義されます。

可逆規則

いくつかの規則は可逆であるため、探索を効率的に行うことができます。

ある規則が可逆であるとは、横棒の下にある推件が成立するときに、横棒の上にある推件が全て成立することをいいます。たとえば、 $\land$ の右導入規則

$$\frac{\Gamma \vdash A \qquad \Gamma \vdash B}{\Gamma \vdash A \land B}$$

の逆は

$$\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}$$

$$\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}$$

の2つの規則です。この2つは証明図に直接は現れませんが、上の推件に対する証明図から下の推件に対する証明図を作ることができる(容認規則)ため、元の右導入規則は可逆だといえます。

ある規則が可逆である場合、その探索レベルにおけるバックトラックの必要がなくなります^[6]。つまり、可逆な規則を適用し、その先の探索に失敗した場合、同じ推件に対して別の規則を試す必要はなく、ただちに探索処理の親フレームに復帰することが可能です。

古典命題論理

古典命題論理の場合、カット無し・縮約無しで全ての結合子規則が可逆なものを考えることができます。そのため、「別の規則を試行する」という目的でのバックトラック (OR 演算子で繋がれたバックトラック; angelic nondeterminismに対応) は一切不要です。

いっぽう、 $\land$ の右導入や $\lor$ の左導入では、規則の上辺に2つの推件があらわれます。そのため、いずれか片方の探索に成功した場合、もう一方の推件に対する証明も探索する必要があります。この意味でのバックトラック (AND 演算子で繋がれたバックトラック; demonic nondeterminismに対応) は依然として必要です。

さてここで、探索の目的を「証明図を見つける」ことから、「証明図がないことを確認する」という形に反転し、バックトラックを非決定性とみなしてみます。つまり、 $\land$ の右導入や $\lor$ の左導入に遭遇したときは、非決定的な動作によりいずれかの分岐だけを確認することを考えます。すると、このアルゴリズムは命題の大きさに対して線形の探索ステップで動作し、「証明図がない」という結果を非決定的に出力することができます。これは、古典命題論理の妥当性判定がco-NPであることを証明論的な側面から確認した結果とみなすことができます。このとき選択された分岐から、入力された命題の反例を再構成することができます。

タブロー法と呼ばれる証明も、古典論理の推件計算を片側に寄せて^[7]、各規則の可逆性に注目して簡略化した証明図とみなすことができます。

直観主義論理に対する探索

いっぽう、直観主義命題論理の証明図を同じ手法で探索しようとすると困難が発生します。それは、 $\to$ に関する規則の取り扱いです。まず、 $\to$ の右導入規則はとても簡単です。

$$\frac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}$$

いっぽう、 $\to$ の左導入規則は以下のようになります。

$$\frac{\Gamma, A \to B \vdash A \qquad \Gamma, B \vdash C}{\Gamma, A \to B \vdash C}$$

Curry-Howard対応にもとづくと、 $A \to B$ は $A$ の証拠を受け取って $B$ の証拠を返す関数です。この関数を利用するには、 $A$ 型の引数を組み立てて渡すことになります。その引数の組み立てを行っているのが左辺の推件です。関数を呼び出すと戻り値が返ってきます。戻り値を使って後続処理を行っているのが右辺の推件です。

古典論理で $A \to B = \lnot A \lor B$ とおいたときの対応する規則は以下のようになり、左辺が大きく異なることがわかります。

$$\frac{\Gamma \vdash A, \Delta \qquad \Gamma, B \vdash \Delta}{\Gamma, A \to B \vdash \Delta}$$

直観主義論理の $\to$ の左導入規則の問題は、左辺の推件がもとの推件(横棒の下にある推件)より小さくなっていない点です。仮説である $A \to B$ を分解しようとしているのに、左辺にはそれが残ってしまっています。では、左辺からこの仮説を取り去って

$$\frac{\Gamma \vdash A \qquad \Gamma, B \vdash C}{\Gamma, A \to B \vdash C}$$

としてもよいかというと、この規則では十分な証明能力を持ちません。典型的には古典論理を特徴づける命題の二重否定、 $\lnot \lnot (P \lor \lnot P)$ や $\lnot \lnot (((P \to Q) \to P) \to P)$ などを証明してみると、仮説を2回以上利用する必要があることがわかります。

この問題を解決するには、さらに規則を見直す必要があります。この問題をはじめに解いたのはDyckhoffのLJTです。また、Hudelmaierのアルゴリズムはさらに推論規則を見直し、より効率的なアルゴリズムを提示しています。Coqのtauto tacticは前者を利用しています。また、ipc_botの現行実装は後者を利用しています。

CNFと推件

さらに、本稿ではここまで紹介した推件計算によるアプローチを別の方面から整理してみます。ここで再び古典命題論理の話に戻ります。

古典命題論理の充足可能性問題を解く際は、対象となる命題を連言標準形に制限するのが一般的です。充足可能性を保ちながら、一般の命題を連言標準形に変換することができることが知られています。これは、入力された命題の各部分命題をあらわすあらたな変数を導入し、その変数がもとの部分命題と同値になるように制約を足すという方法で実現されます。

これはここまで考えてきた妥当性の問題とは一見関係のない話のように見えますが、実は密接な関係があります。というのも、妥当性と充足可能性はde Morgan双対の関係にあるからです。これを踏まえると、たとえば

$$(x \lor y \lor \lnot z) \land (\lnot y \lor z)$$

の充足可能性を判定する問題は

$$x \lor y \lor \lnot z, \lnot y \lor z \vdash$$

という推件の妥当性を判定する問題 (の結論を否定したもの) とみなすことができます。 (推件の後件に命題がない場合は、 $\bot$ が置かれている場合とほぼ同義です)

……とはいえ、この推件を解くための実際のアルゴリズムという意味では、古典論理の証明探索と一般的なSATソルバーのアルゴリズムは完全には対応しません。

• SATソルバーのアルゴリズムでは変数単位での場合分けが一般的です。
  • Davis-Putnamアルゴリズムの命題パートでは、導出という手順により変数を1つずつ消していきます。
  • Davis-Putnamの命題パートを改良したDPLLアルゴリズムでは、各ステップで変数をひとつ選び、場合分けにより変数を消していきます。
  • DPLLを改良したCDCLアルゴリズムも、変数に対する場合分けをする点は同じです。
• 一方、古典論理の証明探索では、変数ではなく節に注目して場合分けを行います。

直観主義への一般化

ここではCNFの考え方を直観主義命題論理に一般化します。このアイデアはipc_botの次期バージョン(開発停止中)に実装されています。

ここで説明する内容は筆者が独自に考えたアイデアですが、他の人でも思いつきそうなので新規性はないかもしれません。

ここではこの標準形を ICNF (Implication-Conjunction Normal Form) と呼ぶことにします。CNFと異なり、ICNFには3種類の異なる節があります。

• 通常の節は $p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n$ ($m, n \geq 0$) の形をしています。古典的には $\lnot p_1 \lor \cdots \lor \lnot p_m \lor q_1 \lor \cdots \lor q_n$ と同値です。
  • $m = n = 0$ の場合は $\bot$ です。
  • $m = 0$, $n > 0$ の場合は $q_1 \lor \cdots \lor q_n$ です。
  • $m > 0$, $n = 0$ の場合は $\lnot(p_1 \land \cdots \land p_m)$ です。
• 含意節は必ず3つの変数を含み $(p \to q) \to r$ の形をしています。古典的には $(p \lor r) \land (\lnot q \lor r)$ という2つの節からなる式と同値です。
• ゴール節は1つの変数からなり $\vdash p$ の形をしています。ゴール節はICNF内にちょうど1つだけ存在する必要があります。古典的には $\lnot p$ と同値です。

このように定義すると、ある命題をその妥当性を変えずにICNFに変換することができます。これは命題の構造に対して再帰的に以下のように構成されます。

• $p \land q$ の形の命題を新規の変数 $r$ に置き換えます。以下の節を追加します。
  • $p \land q \to r$
  • $r \to p$
  • $r \to q$
• $\top$ の形の命題を新規の変数 $p$ に置き換えます。以下の節を追加します。
  • $p$
• $p \lor q$ の形の命題を新規の変数 $r$ に置き換えます。以下の節を追加します。
  • $p \to r$
  • $q \to r$
  • $r \to p \lor q$
• $\bot$ の形の命題を新規の変数 $p$ に置き換えます。以下の節を追加します。
  • $\lnot p$
• $p \to q$ の形の命題を新規の変数 $r$ に置き換えます。以下の節を追加します。
  • $(p \to q) \to r$
  • $r \land p \to q$
• 最終的に入力された命題全体が変数で $p$ のように表されたら、それを以下の形の節にします。
  • $\vdash p$

ICNFソルバ

切断規則なし・縮約規則なしの直観主義命題論理の推論規則システムをICNFに制限すると、途中で出てくる推件も「ほぼ」ICNFに閉じていることがわかります。「ほぼ」と言っているのは、後件に一時的に $p_1 \land \cdots \land p_m$ の形の命題と $p \to q$ の形の命題が出てくることがあるからです。しかし、いずれも右導入規則の可逆性があることに注目すると、これらはただちに分解されるものと仮定できます。すると、推論規則をICNFの形式に特化させて、以下のように置き直すことができます。

$$\frac{\Gamma \vdash p_i \; (\forall i) \qquad \Gamma, q_j \vdash r \; (\forall j)}{\Gamma \vdash r} \quad ((p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n) \in \Gamma)$$

$$\frac{\Gamma, p \vdash q \qquad \Gamma, r \vdash s}{\Gamma \vdash s} \quad (((p \to q) \to r) \in \Gamma)$$

$$\frac{}{\Gamma \vdash p} \quad (p \in \Gamma)$$

いずれの規則も後件には変数しか導入しません。そこで、最初に与えられるICNFの節と、証明探索中に追加される変数を別の環境として分離し、 $\Gamma \mid \Delta \vdash p$ ($\Gamma$ はICNFの節の集合、$\Delta$ は変数の集合)のような推件で表記することを考えます。すると規則は以下のように置き直すことができます。

$$\frac{\Gamma \mid \Delta \vdash p_i \; (\forall i) \qquad \Gamma \mid \Delta, q_j \vdash r \; (\forall j)}{\Gamma \mid \Delta \vdash r} \quad ((p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n) \in \Gamma)$$

$$\frac{\Gamma \mid \Delta, p \vdash q \qquad \Gamma \mid \Delta, r \vdash s}{\Gamma \mid \Delta \vdash s} \quad (((p \to q) \to r) \in \Gamma)$$

$$\frac{}{\Gamma \mid \Delta \vdash p} \quad (p \in \Delta)$$

さらにゴールの循環を防ぐため、訪問済みのゴールを記録しておきます。新たに変数の集合 $\Theta$ を導入して $\Gamma \mid \Delta \vdash p \mid \Theta$ と書き、以下のようなルールを考えます。 $\mid$ がないときは $\Theta$ は空集合とみなします。

$$\frac{\Gamma \mid \Delta \vdash p_i \mid \Theta, r \; (\forall i) \qquad \Gamma \mid \Delta, q_j \vdash r \; (\forall j)}{\Gamma \mid \Delta \vdash r \mid \Theta} \quad ((p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n) \in \Gamma)$$

$$\frac{\Gamma \mid \Delta, p \vdash q \qquad \Gamma \mid \Delta, r \vdash s}{\Gamma \mid \Delta \vdash s \mid \Theta} \quad (((p \to q) \to r) \in \Gamma)$$

$$\frac{\Gamma \mid \Delta \vdash q \mid \Theta, s \qquad \Gamma \mid \Delta, r \vdash s}{\Gamma \mid \Delta \vdash s \mid \Theta} \quad (((p \to q) \to r) \in \Gamma)$$

$$\frac{}{\Gamma \mid \Delta \vdash p \mid \Theta} \quad (p \in \Delta)$$

このとき、含意節 $(p \to q) \to r$ の適用ルールは2つに分けておきます。これは、環境に $p$ を導入する目的で適用されるケースと単に $q \to r$ に弱化して適用しているだけのケースを区別する必要があるからです。

このように推件に情報を足しておくと、ループ防止のための以下の制約を加えることができます。

• $\Delta$ に対する制約
  • 通常の節 $p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n$ を適用できるのは $q_1, \ldots, q_n$ のいずれも前件に存在しない場合に限る。
    • さもなくば、規則の右辺から同じ推件の証明を取り出せる。 ($\Theta$ の差異は無視できる)
  • 含意節 $(p \to q) \to r$ を適用できるのは $r$ が前件に存在しない場合に限る。
    • さもなくば、規則の右辺から同じ推件の証明を取り出せる。 ($\Theta$ の差異は無視できる)
  • 含意節 $(p \to q) \to r$ を適用できるのは $p$ が前件に存在しない場合に限る。ただし、 $\Theta$ を継承するルールを適用する場合はこの限りではない。
    • さもなくば、規則の左辺から同じ推件の証明を取り出せる。 ($\Theta$ の差異は無視できる)
• $\Theta$ に対する制約
  • 通常の節 $p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n$ を適用できるのは $p_1, \ldots, p_m$ のいずれも $\{r\} \cup \Theta$ に属さない場合に限る。 ($r$ は現在のゴール, $\Theta$ は後件の命題集合)
    • さもなくば、規則の左辺から同じ推件の証明を取り出せる。
  • 含意節 $(p \to q) \to r$ を適用できるのは $q$ が $\{s\} \cup \Theta$ に属さない場合に限る。 ($s$ は現在のゴール, $\Theta$ は後件の命題集合)
    • さもなくば、規則の左辺から同じ推件の証明を取り出せる。

このように定義しても $\Gamma \vdash p$ の証明可能性は変わりません。

この推論規則のシステムにそった探索は停止します。そのためには、ICNFに出現する全ての変数の集合を $V$ とおき、 $\Gamma \mid \Delta \vdash p \mid \Theta$ の重みを $|V \setminus \Delta| \cdot |V| + |\{p\} \cup \Theta| - 1$ と定めればOKです。

この探索はさらに最適化の余地があります。たとえば通常の節 $p_1 \land \cdots \land p_m \to q_1 \lor \cdots \lor q_n$ の適用は $p_1, \ldots, p_m \in \Delta$ であれば可逆であるため、バックトラックを回避して優先適用することができます。

証明図の再構成

ここで説明した証明探索アルゴリズムはいずれも、探索向けに最適化された特殊な推論規則を使って実装されています。これらを、より一般的な利用に適した証明図に変換するのが望ましいでしょう。

ipc_botの場合は、探索を推件計算ベースで行いつつ、出力は自然演繹で行っています。これは以下の理由からです。

• 筆者のいた大学の授業では自然演繹が教えられており、他の学生にも理解しやすいと考えたため。
• 正規形の導出を見慣れたアルゴリズムで行えるため。

さて、探索した結果を別の証明図に変換するには、元の証明図の各ステップを変換先の規則の組み合わせで表現すればOKです。しかし、そうして作られた証明図は、いわばユーティリティー関数がインライン化されずに残っているような状態で、やや不恰好です。そこで、これらを一掃することを目的として正規化を行います。

自然演繹は(ANDやORなどを加えた)単純型つきラムダ計算であるため、基本的には以下の2種類の正規化でかなり綺麗になります。

• β簡約 -- 導入規則の下でただちに除去規則を適用している箇所を簡約する。
• η変換 -- 除去規則 + 公理 + 導入規則 を適用しており、全体が公理と同じ形になっている箇所を簡約する。

加えて、ここでは意味の異なる証明図を区別する必要がないため、部分証明図が同じ推件を証明している場合は持ち上げるなどの簡略化も可能です。

理論的には正規化は最悪ケースのオーダーがかなり悪いですが、経験上はipc_botに入力されるようなレベルではそれほど問題にはなりません。

推件計算の再構成

ipc_botでは推件計算の証明図の再構成は行っていませんが、切断除去が自然演繹におけるβ簡約に近い役割を担うため、不可能ではなさそうです。ただ、自然演繹ではラムダ計算に由来してde Bruijn indexなどの束縛変数管理がよく知られており、かなりうまく適合しますが、推件計算における束縛変数管理はそれよりもやや面倒になるかなと思います。

また、推件計算の証明図を表示するにあたっては、なるべく弱化をはやめに暗黙的に適用するなど、図の圧縮を試みたほうがいいかもしれません。

Hilbert計算の再構成

Hilbert計算は自然演繹や推件計算のように一意に決まる気の利いた正規形はなさそうなので、最も気の利いた証明列を与えるためのヒューリスティックスを考えるのはなかなか大変かもしれません。ipc_botには実装されていません。

反証アルゴリズム

証明アルゴリズムが終了し、FALSEを出力した場合は、その論理式が妥当でないことがわかります。そこで、妥当ではないことの証拠を提示することを試みます。

ipc_bot では、この場合には証明アルゴリズムの探索の跡から情報を取り出すことはせず、まっさらの状態から別のアルゴリズムでモデルを探します。このときは外部のSATソルバーを利用します。

反証に使うのは、Kripkeモデルです。Kripkeフレームとその上の真理値の代入をうまく選んで、入力された命題の評価値がTRUEでなくなるケースを探します。Kripkeモデルは $\{0, 1\}$ であらわされる値の組で表現されるため、SATソルバーへの入力に適しています。もちろん、すでに説明したように、KripkeモデルとHeyting代数モデルには対応関係があるため、あとでHeyting代数に変換して提示することも難しくはないでしょう。 (ipc_botではHeyting代数による表示は実装していません)

漸進的な探索

反証はなるべく単純なほうが望ましいです。ここでは、Kripkeフレームの大きさが小さいほどよいと考えます。そこで、Kripkeフレームの大きさを1からはじめ、1ずつ増やしながら毎回SATソルバーを呼び直しています。

Kripkeフレームに対する追加の制約

Kripkeフレームにはいくつかの制約を仮定できます。まず対称性より、 $W_i \leadsto W_j$ ならば $i \leq j$ と仮定できます。 (つまり、到達可能関係は可能世界の番号の大小関係に埋め込まれると考えることができます)

さらに、あるKripkeモデルが入力命題の妥当性の反証となるときは、ある可能世界 $W_i$ があってその可能世界における真理値が0であることになります。もし、 $W_i$ から到達可能でない可能世界があれば、それは $W_i$ の真理値に寄与しないため、その可能世界を除いても同様に反例として成立するはずです。しかし、すでに1つ小さい大きさのKripkeモデルは探索済みであることから、このような場合はありえません。ですから、この $W_i$ からは全ての可能世界が到達可能だと仮定することが可能です。先ほどの仮定とあわせると、 $i = 0$ も確定します。

SATへのエンコード

以上を考慮した上で、あとはKripkeフレームの構造とKripkeモデルの計算をSATにエンコードするだけです。以下を変数として持つことになります。

• Kripkeフレームの到達可能関係 ($W_i \leadsto W_j$ か否か？)
• 原子命題の真理値 ($\llbracket P \rrbracket_{W_i} = 1$ か否か？)
• 複合的な命題の真理値
• $\llbracket P \to Q \rrbracket$ を計算するための中間変数 etc.

デコード

SATがSatisfiableを出力したら、その代入をデコードしてKripkeモデルを構成し、ユーザーに提示します。

Unsatisfiableの場合はサイズを1つ大きくして再試行するか、試行をあきらめてユーザーに証明可能性の結果のみを提示します。

ベンチマーク

The ILTP Library に直観主義論理 (一階 / 命題) のベンチマーク用のデータセットがあります。これはTPTPの直観主義論理版と言えます。

ipc_bot のベンチマーク結果は手元にはないのですが、一応一通り流して確認したような記憶はあります。

今後の展望

一番要望を多く感じたのは、一階述語論理や二階命題論理への一般化です。後者は意外に思われるかもしれませんが、たとえば「排中律と二重否定除去の同値性」のように関心を集めやすいトピックで必要になります。いずれも一般的にはかなり難しいので基本的にはいい感じの半決定アルゴリズムを考えていくことになるかなと思いますが、そもそも命題の表現で束縛変数の管理をするだけで実装の手間が半端ないのでベースライン実装だけでもかなり気合が必要そうです。

また、他のファンシーな論理 (様相論理、線形論理、μ計算、Bunched Logicなど) も面白そうですね。これも実装が大変そうなので実際に実現することはないだろうなと思います。

最後に

学生時代に思い付きで作ったものをここまで愛用していただいてありがたい限りです。Mastodonに移ってからめっきり使われなくなりましたが、細々と運用は続けていこうと思うので、よろしくお願いします。

一方で、ipc_botがこのままで終わってしまうのを勿体なくも感じています。それがこの記事を書いた理由でもあります。私から出せる知見はほとんど出し切ったと思うので、今度は皆さんにipc_botの未来を切り開いていってほしいです。もちろん、ipc_botそのものに貢献していただく必要は(必ずしも)ありません。読者の皆さんの中には私よりも熱意に溢れていて時間をたくさん使える人もいるはずです。もし興味があれば、ぜひipc_botを完全に置き換えるような最強のツールを作ってみてはいかがでしょうか。

脚注

1. 「二階命題論理」のように量化が明示されている場合は別です。

2. その名前に反して、推件計算は推件を利用する唯一の流儀ではありません。

3. このde Morgan双対は、内側の否定は対象レベルで、外側の否定はメタレベルで行われているという意味でやや特殊です

4. 一方、Prologの同名の演算子は切断規則との直接の関係はないと考えられます。

5. 古典論理の場合は後件の命題も構造規則の対象なので、これらも同様に考える

6. Prologにおける切断演算子は (切断規則との関係は薄いですが) このような可逆規則に対する最適化処理には対応するといえます。

7. 古典論理では、推件計算を前件または後件のみで定義することができる。そのためにはまず否定を原子命題に対してのみ許し、一般的な否定は命題に対してde Morgan双対を計算するメタ的な演算と考える。否定が一般の論理結合子ではなくなることで、推論の途中で命題を右から左に、あるいは左から右に移動させる必要がなくなる。これをone-sided sequent calculusという。タブロー法のほかにもproof netなどでも用いられる。