■ 1. 概要
Coqは、公理的集合論ですら符号化できる表現力の高い言語です。なので論理学もそこで展開することができます。そこで、自然演繹を証明系として持つ古典命題論理を符号化して、完全性定理や関連する定理を証明してみました。
もちろん、誰でもこんなことは考え付きます。先行事例もあります。特にCoqの公式サードパーティ―製の成果物を集めたレポジトリに coq-community/propcalc というのがあります。しかし後述するように、論理学の観点からすると全くもって不十分です。なので別の実装を作るモチベーションが生まれます。
さて、論理学の観点からすると完全性定理とはできるだけはやく証明すべき定理です。証明を考えるより充足性の確認をする方が圧倒的に簡単だからです。例えばドモルガンの法則など、各種論理記号の分配則は、その証明を考えるよりそれらをSAT問題として確認する方が圧倒的に楽です。
というわけで、私が実装したのは最短経路に近い完全性定理の実装です 。ユーティリティに 100行程度、証明すべき定理の符号化に100行、証明に300行くらいの規模感です。Coqの標準ライブラリのみを使います。なおメタレベルで古典的な推論をするため、Classicalライブラリはつかいます。
完全性定理の証明の手順はいくつかありますが、そのミニマリスト的なアプローチと、教科書のアクセシビリティと、その明晰さから、故Rautenberg教授の 論理学の教科書を踏襲します。以下のリンクで公開されている教科書は、命題論理の部分は完全に無料公開されているうえ、極めて上質な議論がなされているので、読んでみて気に入ったら購入することをかなり強く勧めます。とはいえ、本稿を読むだけで大まかな流れがつかめるように配慮はします。
-
A Concise Introduction to Mathematical Logic by Rautenberg
- 1章と2章が無料公開され、2章が命題論理にあてられています
■ 2. 論理学から見た全体像
まず、論理記号は否定記号¬と連言記号∧の2つのみです。選言記号∨や含意記号→は、それらを使って定義します。命題変数の全体は決定可能で可算無限であることを仮定します（注:Rautenbergでは非可算無限の議論もしますが、その場合ツォルンの補題が必要になるので可算無限にすることにしました）。矛盾記号⊥は、任意だけれど固定した命題変数$x_0$ を使って $x_0∧¬x_0$ で定義します。
証明系は、ゲンツェン流自然演繹を採用します。つまり、妥当なシーケントの木構造で証明を表現します。推論規則はたったの6個です。Coqでの証明時に場合分けの数がかなり少なくなるので、かなりうれしいです:
一般に大文字アルファベット・大文字ギリシャ文字は論理式の集合です。小文字のギリシャ文字は論理式です。シーケントの左側に出てくるカンマは和集合で $X,α⊢β$ は $X∪\{α\}⊢β$ と読みます。シーケントの右側に出てくるカンマは二つのシーケントの省略形です。つまり$X⊢α,β$ は $X⊢α$, $X⊢β$ の二つを意味します。
「$Γ⊢α ⇒Γ⊨α $」を健全性定理、「$Γ⊨α ⇒Γ⊢α $」を完全性定理と呼びます。コンパクト性定理は、まず $⊢$ について証明し、完全性定理から $⊨$ についても成り立つよね、という形で証明することにします。本成果物では、健全性定理、完全性定理、コンパクト性定理をCoqで符号化して証明します。
□ 2-1. 健全性定理
健全性定理は、証明図を構成するシーケントの健全性が伝播することを示すことで証明します。論理学の教科書でいうところの「推論規則による帰納原理」と呼ばれる帰納法を使うわけです。前述の6つの各推論規則において、上から下に健全性が保存されていることを確かめるだけです。これってほとんど見ただけで成立するとわかります。Coqでの証明も30行もかからないくらいです。なお、Coqでは、「推論規則による帰納原理」に相当する帰納原理は「証拠による帰納原理」と呼ばれ、Inductiveに性質を定義するときに自動生成されてすぐに使えるようになります。
□ 2-2. コンパクト性定理
コンパクト性定理の証明には、まず Γ ⊢ α ならΓの有限部分集合Gが存在して G ⊢ α となることを証明しておきます(有限性と呼びましょう)。後で完全性定理が証明できれば、⊢ を ⊨ に置き換えます。そしてその系としてコンパクト性定理はすぐに出てきます。⊢バージョンの有限性の証明は前述の「推論規則による帰納原理」をつかえば、これもまた見ただけでほとんど自明に成立することがわかりますし、Coqでの証明も同じく30行程度です。なお、集合の有限性に関する性質はCoqライブラリの Finite_sets_facts に Ensemble の性質として登録されています。
□ 2-3. 完全性定理
つまり我々が行うべき証明のほとんどは完全性定理の証明のためのものです。無矛盾性や充足可能なモデル構築など複数の概念が必要になり議論が込み入ってきます。
◆ 無矛盾性
完全性定理の証明には、一見無関係に見える無矛盾性の議論が絡んできます。なぜかというと、完全性定理の結論部は、「$Γ' := Γ∪\{¬α\}$ が矛盾する」と言い換えられるからです。さらに、完全性定理の証明は対偶命題の証明で示すので、証明すべき言明の仮定部/前提部が 「Γ'が無矛盾である」となります。なお、一連の議論の中で 演繹定理 は欠かせないので派生規則として早々に証明します。
◆ もうひとつの完全性
以上のように完全性定理の対偶における仮定部は「Γ'が無矛盾なシステムである」となります。さて一般に無矛盾なシステムには、独立な命題――証明もできないし、反証もできない命題――がありえますが（例: ZFにおける選択公理）、独立な命題がないような無矛盾なシステムがある可能性があります。任意の命題の証明可能性にYes/Noをはっきり言える無矛盾なシステムを極大無矛盾なシステムと呼びます。（余談：完全なシステムとも呼びますが、この意味での「完全」は完全性定理での完全と別の意味なのでややこしい）。そこで、仮定部を「Γ'を拡大した極大無矛盾なYが存在する」に置き換えても問題ありません。（一般にA⇒Bという形の命題の証明において、前提部の成立条件を弱めても問題ないです。A⇒A' A'⇒B ならば A⇒B だからです）。そしてそれが証明のキモになります。つまり、任意の無矛盾なシステムを極大無矛盾なシステムにできるのか？という課題がでてきました。
◆ 理論の保存拡大と枚挙可能性
前述の議論から、極大無矛盾なシステムの構成方法、つまり極大無矛盾な保存的拡大方法が問題となりますが、Lindenbaumの構成手順を使います。そのための条件が「論理式の全体が可算無限で枚挙可能である」です。枚挙可能性とは、何らかの手順で次々と言語の論理式を出力する手順が存在することです。ここで、論理式を重複して出力しても可です。自然数全体から論理式全体へのTotalな写像といって構いません。つまり各論理式にそれぞれ別の番号を振る（ゲーデル数化）ができれば十分です。そしてそれは、古典命題論理では満たせます。
◆単射性と枚挙可能性（ユーティリティ）
といったわけで、ゲーデル数化の構成とその単射性の証明が必要となってきます。この実現のために、カントールの対関数によるゲーデル数化を採用します。カントールの対関数とその単射性関してはユーティリティモジュールに入れました。ゲーデル数化は、対関数があれば簡単に構成できますしその単射性も簡単に証明できます。また、一般にAから自然数全体への単射があれば、自然数全体からAへの全射が存在します。そして、その写像を枚挙と呼んで差し支えないでしょう。ということで「natへの単射があるなら、枚挙を構成できる」という事実の証明もまた、それもまたユーティリティに入れました。本成果物のユーティリティは、この２つだけです。あわせて100行くらいで書けます。対関数の単射性のみが必要で逆写像の構成は必要がないから短くなりました。
◆充足可能性問題への変形
これまでは、完全性定理の対偶命題の 仮定部/前提部 にフォーカスしましたが、今度は 結論部/帰結部 にフォーカスをあてます。つまり、 $ Γ ⊭ α$ です。これもまた 「Γ' が充足可能である」と言い換えることができます。そしてその証明は、具体的なモデル/解釈を構成することです。
◆まとめ
以上、完全性定理の証明をするためには、Γ'の保存拡大であり極大無矛盾なシステムYを構成して、Yを充足させる解釈を構成してあげればよい、ということになります。復習がてらに逆向きに議論を言いなおしてみます:
Γ ⊬ α と同値な「Γ'の無矛盾性」から、「極大無矛盾な Y を構成し Yがモデル w を持つ」を導けたとします。Γ' は Y の部分集合ですので当然 Γ' を充足します。このΓ'の充足可能性は、$Γ ⊭ α$ の成立と言い換え可能です。つまり、Γ ⊬ α の成立 ⇒ (Y,w)の存在 ⇒ Γ ⊭ α の成立がいえたわけですが、これは（真ん中の命題を無視すると）、完全性定理の対偶命題に一致します。したがって、Y,w の構成法さえ示せれば、完全性定理が証明できたことになります。実際、Y は Lindenbaum の方法により構成できますし（前提となる言語の枚挙可能性はゲーデル数化を構成することで示せます）、w は（ここでは言及してませんが）サクッと簡単に構成できます。
■ 3. Coqから見た全体像
Coqでの実装上のハマリどころ、工夫点、課題などを列挙します
□ 3-1. 関数よりも関係
例えば意味論におけるモデル/解釈による論理式の付値は、(propvar -> bool) -> formula -> bool のような型を持つFixpointで実装したくなりますし、それは実際可能です。しかし、関数の構成は、停止性の条件を満たすのが大変だったり、Propの場合分けが許されていなかったりと扱いずらいものになります。今回のケースでは、極大無矛盾なシステムのモデルをFixpointで直接実装することは（たぶん）不可能です。なので関数ではなく、そのリレーショナルな形を採用するのがよいです。 つまり、命題変数のEnsemble として true となる命題変数の集合を特定して、かくFormulaへの付値はInductiveに定義しましょう。例えばこんな感じです:
Inductive value (w: Ensemble PV) (a: fm): bool -> Prop :=
| valPrime1 p : a = Var p -> In _ w p -> value w a true
| valPrime2 p : a = Var p -> ~In _ w p -> value w a false
| valNot a' b: a = Not a' -> value w a' b -> value w a (negb b)
| valAnd a1 a2 b1 b2: a = And a1 a2 ->
value w a1 b1 -> value w a2 b2 -> value w a (b1 && b2).
もちろんこれが関数的であることの証明をするべきですし、関数として扱いたいときはその定理を使います:
Lemma value_deterministic: forall w a, exists! b, value w a b. (*後略*)
本当に関数が必要であれば、Require Import ClassicalChoice をして choice を value に適用することでその存在を示せます。その代わり、選択公理がAxiomに追加されるので好ましいとは考えません。
このあたりの都合は、枚挙に関連しても言えます。命題の枚挙関数 (nat->fm) が存在することと、命題のトータルな枚挙関係 (nat->fm->Prop) が存在することは似ているようで違います(帰納的集合と帰納的可算集合)。Cantorの対関数やゲーデルのオリジナルなゲーデル数化では、その復号は有界なサーチなので原始再帰的でFixpointとして書けますが、一般には選択公理が必要だったりすると思います。復号化の実装も停止性の問題から実装がめんどうですし、完全性定理証明のためには、別に関数が必須というわけでもないので、やはり枚挙関係の構成のほうが好ましいといえるでしょう:
Lemma enumR_spec1 : forall n, exists a, enumR n a. (* 後略 *)
Lemma enumR_spec2 : forall n n' a, (* 後略 *)
Lemma enumR_spec3 : forall n a a', (* 後略 *)
□ 3-2. 数学の集合はMSetやlistではない
CoqでのListやMSetは確かに集合のように扱えるし、帰納原理もあるし、色々な便利関数が付随しているしで、集合を list や MSet で符号化したくなりますが、多くの場合はそれは間違いです。なぜならそれらは有限濃度しか持てないからです。なので数学の集合を符号化するのはEnsembleである必要があります。
前述の coq-community/propcalcではシーケントの前件をlist で符号化していました。個々の証明においては、前提となる論理式の集合は有限なので問題がないとは言い切れませんが、システムとしてのΓは有限とは限らないので、Ensembleで符号化する必要があります。特に完全性定理を証明しましたといったときに Γ⊢α <-> Γ⊨α のΓがlistで符号化されていたらそれは完全性定理の証明ではありません。
なお、EnsembleであってもそれがFiniteであれば帰納原理が存在し、何回か使いました。⊢ の有限性によって、Yの部分集合Gの存在を言って、Gについて帰納原理を使うことで、Gに関する性質を証明できるというわけです。
□ 3-3. Classical モジュール採用の是非
Classical モジュールを使うことの是非は問題になるかもしれませんが、結論からいうと問題ないでしょう。
論理学では、対象言語での推論規則と、メタ言語での推論規則は別物として扱うことが多いです。選択公理をつかって証明したりするのをみたこともあるはずです。なお、ゲーデルの第二不完全性定理とかを考えると、メタでの行為自体を対象言語に対応させるので、いつでもどこでも、メタ言語に何でもかんでも使える、という常識があるというわけではありませんがその辺の事情はよく知りません。
以前似たような課題感の記事を書いたような気がします:
とはいえ、あまり多くのAxiomを追加すると今度はCoq自体が矛盾するかもしれないという不安があるので無制限に、とはいかないと思います。完全性定理で依存するAxiomは、Ensembleの外延性と、Classicalくらいのものなので（あとCountableInfiniteな命題変数の存在ですが、それはArith.Natというwitnessがあるので問題にはならないでしょう）
つまり、Coq＋Classical+Ensemble Extensionality が矛盾していなければ、完全性定理を証明できたと思います（符号化に文句がつかなければ、という前提もありますが……）
■ 4. 実装ダイジェスト
□ 4-1 統語論・意味論・証明系
論理記号が2つしかないので命題論理式のInductiveな定義は極めて単純です
Inductive fm: Type :=
| Var : PV -> fm
| Not : fm -> fm
| And : fm -> fm -> fm.
意味論は前述したようにリレーショナルに定義しますが、関数的であることも併せて示すことで失われる情報は何もありません:
Inductive value (w: Ensemble PV) (a: fm): bool -> Prop :=
| valPrime1 p : a = Var p -> In _ w p -> value w a true
| valPrime2 p : a = Var p -> ~In _ w p -> value w a false
| valNot a' b: a = Not a' -> value w a' b -> value w a (negb b)
| valAnd a1 a2 b1 b2: a = And a1 a2 ->
value w a1 b1 -> value w a2 b2 -> value w a (b1 && b2).
Lemma value_deterministic: forall w a, exists! b, value w a b.
証明系も推論規則が6個しかないので短いです。これはInductionをするときのGoalの少なさにつながるので論理記号を少なくとることの利点にもなっています
Reserved Notation "Γ ⊢ A" (at level 80).
Inductive SysPrf : Ensemble fm -> fm -> Prop :=
| IS A: Singleton _ A ⊢ A
| MR Γ Γ' A : Included _ Γ Γ' -> Γ ⊢ A -> Γ' ⊢ A
| AndI A B Γ : Γ ⊢ A -> Γ ⊢ B -> Γ ⊢ A ∧ B
| AndE1 A B Γ: Γ ⊢ A ∧ B -> Γ ⊢ A
| AndE2 A B Γ: Γ ⊢ A ∧ B -> Γ ⊢ B
| Not1 A B Γ: Γ ⊢ A -> Γ ⊢ ¬A -> Γ ⊢ B
| Not2 A B Γ: (Add _ Γ A) ⊢ B -> (Add _ Γ ¬A) ⊢ B -> Γ ⊢ B
where "Γ ⊢ A" := (SysPrf Γ A).
□ 4-2 ゲーデル数化
カントールの対関数を使います。一つ目の数が構成子を指定します。当然 injective であることを証明する必要があります:
Fixpoint toNat (x:fm): nat := match x with
| Var p => cpair 0 (PropVar.f p)
| Not x1 => cpair 1 (toNat x1)
| And x1 x2 => cpair 2 (cpair (toNat x1) (toNat x2))
end.
Lemma toNat_inj : forall x y, toNat x = toNat y -> x = y.
逆関数は実装しません。nat への単射性をもとに、枚挙関係を構築する一般的な方法をユーティリティモジュールで定義しているので、数行で必要な仕様を満たす枚挙関係を構築できます
Definition enumR := util.enumR _ ⊥ toNat.
Lemma enumR_spec1 : forall n, exists a, enumR n a.
Proof. now apply (util.enumR_spec1 _ ⊥ _ toNat_inj). Qed.
Lemma enumR_spec2 : forall n n' a,
a <> ⊥ -> enumR n a -> enumR n' a -> n = n'.
Proof. now apply util.enumR_spec2. Qed.
Lemma enumR_spec3 : forall n a a',
enumR n a -> enumR n a' -> a = a'.
□ 4-3 各種性質の符号化
特筆すべきことはありませんが、有限性などを表現するためには論理式の集合はEnsembleで符号化する必要がありますね
Definition Soundness Γ A := Γ ⊢ A -> Γ ⊨ A.
Definition Finiteness Γ A := Γ ⊢ A -> exists G, Finite _ G /\ Included _ G Γ /\ G ⊢ A.
Definition Completeness Γ A := Γ ⊨ A -> Γ ⊢ A.
Theorem Deduction : forall Γ A B, Γ ⊢ A → B <-> (Add _ Γ A) ⊢ B.
Definition Cons Γ := ~(Γ ⊢ ⊥).
Definition MCons Γ := ~(Γ ⊢ ⊥) /\ (forall A, ~In _ Γ A -> Add _ Γ A ⊢ ⊥ ).
□ 4-4 Lindenbaumの構成法
無矛盾な(X0: Ensemble fm) と 論理式の枚挙 {a0, a1, a2, a3, ... } が与えられたときに、列の先頭から順にそれを付け加えたシステムが無矛盾であればその論理式を加えた拡大をし、もし矛盾しちゃったらその否定の論理式を付け加えて拡大していきます。これをω回繰り返してできた集合は極大無矛盾になります、というのがLindenbaumの構成法であり、以下のように符号化しました:
Section ConservertiveExpansion.
Variable X0: Ensemble fm.
Variable HX0: Cons X0.
Inductive expand: nat ->(Ensemble fm)->Prop :=
| Def_of_expand0 : expand 0 X0
| Def_of_expandS1 n X a: expand n X -> enumR n a ->
Cons (Add _ X a) -> expand (S n) (Add _ X a)
| Def_of_expandS2 n X a: expand n X -> enumR n a ->
((Add _ X a) ⊢ ⊥) -> expand (S n) (Add _ X ¬a).
Definition Y: Ensemble fm :=
(fun a => exists n, forall X, expand n X -> In _ X a).
Lemma Y_MCons: MCons Y.
Lemma Y_includes_X : Included _ X0 Y.
これらの集合族は包含関係を順序とした全順序となります。添え字が小さいほど小さい集合です。Yがω回繰り返した結果の集合で、X0の保存拡大である極大無矛盾（のひとつ）です。
□ 4-5 完全性の依存関係
使われている公理です:
Print Assumptions completeness.
Axioms:
PropVar.t : Type
PropVar.id_r : forall x : PV, PropVar.g (PropVar.f x) = x
PropVar.g : nat -> PV
PropVar.f : PV -> nat
classic : forall P : Prop, P \/ ~ P
Extensionality_Ensembles : forall (U : Type) (A B : Ensemble U), Same_set U A B -> A = B
最初の4つは原子命題記号が満たすべき性質です。今回は原子命題記号の型を特定しませんでしたが、Arith.Nat で fもgも恒等関数にとればこれらのAxiomは証明できるので無視します。なので使っているAxiomは二つで、排中律とEnsembleの外延性公理です。両方とも結構有名なAxiomですが、両方追加してCICが矛盾するかは知りませんが、多分大丈夫でしょう、と思いたい。
5. ソースコード
Gistで公開しました。何かに利用する際はコメントくれるとモチベが上がります
https://gist.github.com/41semicolon/36a2f9277cb423506db453da487fd033