00. 概要
Coq上で一階述語論理、特にペアノ算術を含む算術理論を符号化し、その不完全性を構成的に証明した成果物がcoq-community/goedel （以下goedel）にあります。それを読み解くことを本稿の目的とします。
いくつか前提を共有します。
著者の解説記事がある : 著者であるO'Conor 氏による解説記事がWeb上から読めます。TPHOLs2005で論文にしたものをWeb記事で読めるようにしたものです。全体像と一階述語論理の符号化におけるハマリポイントなどを丁寧に説明してくれています。まずはこれを読むのがよむのがよいかとおもいます。一方、コードベースで変更が相次いでいるので記述がコードと整合しない箇所もいくつかあります。
hydra/battles に移行中？ :
goedel は依存関係のあるプロジェクトで、一階述語論理の符号化には coq-community/hydra-battles を、算術的な定理に関してはcoq-community/pocklington を利用していました。そして、数年前と比べると goedel のコードの多くが coq-community/hydra-battles にポートされているように見えます。なので現時点でのコードリーディングの多くは hydra-battles/theories/ordinals/Ackermann/ を読むことに充てられることになると思います。
環境構築 :Coq全般に言えるのですが、コードを読むだけでなく動かして確認するためには環境設定が必要です。OPAM経由でOCaml,Coqをインストールし、OPAMレポジトリにCoq用のレポジトリを追加して、coq-community/goedelなどを依存関係ごとインストールするわけですが、coq-community/hydra-battles のビルドにものすごい計算リソースが必要になります。全コアCPU100%を数時間くらい？なので環境構築には時間がある時を選びましょう。
ポイント
-
Coqは表現力が高いのでrefelexitive type である述語論理の符号化には選択肢が多くあります。
coq-community/goedelでは比較的シンプルな実装で、HOASだったりde Bruijn indexは使っていません -
述語論理の符号化は特定の算術に依存しない一般的なものです。任意の非論理記号を加えた理論でも多くの定理がそのまま利用できるよう配慮されています。
-
Coqに追加の公理を入れないので、メタ言語が直観主義論理です。なので不完全性定理を含め、メタセオリカルな言明の表現には否定翻訳を必要とする場合があります。
-
原始再帰性の符号化には、denotational semanticsを使っています。つまり原始再帰性の形式とその具体的な手続きとを分けており、算術階層関連の言明の証明時に見通しが立てやすくなっています。
01. 統語論
まず対象言語/object language を定める。「+,×,0,S」を採用する言語をLNT、「+,×,0,S,≤」を非論理記号として採用する言語をLNNと呼ぶ。後述するようにこれらは算術PA, NNに対応する言語となる:
(* 対象言語は関数記号と関係記号とそれぞれのアリティからなる *)
Record Language : Type := language {
Relations : Set;
Functions : Set;
arity : Relations + Functions -> nat}.
(* 言語LNNでは4つの関数記号と1つの関係記号からなる *)
Inductive LNTFunction : Set :=
| Plus : LNTFunction
| Times : LNTFunction
| Succ : LNTFunction
| Zero : LNTFunction.
Inductive LNNRelation : Set :=
LT : LNNRelation.
(* 中略 *)
Definition LNT : Language :=
language Empty_set LNTFunction LNTArity.
Definition LNN : Language :=
language LNNRelation LNTFunction LNNArity.
対象言語が定まれば一階算術の統語論を符号化できる。論理記号として「=,→,¬,∀」及びnatでパラメータ化した可算無限個の変数記号を採用すると、帰納的に項 Term や 式 Formula を定義できる:
(*項の帰納的定義, なお L:Language *)
Inductive Term : Set :=
| var : nat -> Term
| apply : forall f : Functions L, Terms (arity L (inr _ f)) -> Term
with Terms : nat -> Set :=
| Tnil : Terms 0
| Tcons : forall n : nat, Term -> Terms n -> Terms (S n).
(*式の帰納的定義*)
Inductive Formula : Set :=
| equal : Term -> Term -> Formula
| atomic : forall r : Relations L, Terms (arity L (inl _ r)) -> Formula
| impH : Formula -> Formula -> Formula
| notH : Formula -> Formula
| forallH : nat -> Formula -> Formula.
LNT,LNN のような decidableな言語では、項や式もdecidableである(term_dec, terms_dec, formula_dec)。一階論理では深さによる帰納法を使うため、それに対応した帰納原理もまた構成する:
Definition Formula_depth_rec
(P : Formula->Set)
(rec : forall a, (forall b, lt_depth b a -> P b) -> P a)
(a : Formula)
: P a := (*後略*)
02. 証明型
証明はヒルベルト流を採用する。証明長は有限なので、前提を list Formulaで符号してよく、証明型 Prf を帰納的に定義できる:
Definition Formulas := list Formula.
Inductive Prf : Formulas -> Formula -> Set :=
| AXM : forall A : Formula, Prf (A :: nil) A
| MP :
forall (Axm1 Axm2 : Formulas) (A B : Formula),
Prf Axm1 (impH A B) -> Prf Axm2 A -> Prf (Axm1 ++ Axm2) B
| GEN :
forall (Axm : Formulas) (A : Formula) (v : nat),
~ In v (freeVarListFormula L Axm) -> Prf Axm A -> Prf Axm (forallH v A)
| IMP1 : forall A B : Formula, Prf nil (impH A (impH B A))
| IMP2 :... (*後略*)
一旦証明が定義できると、算術での証明可能性や算術のConsistencyを定義できる。算術（一般に理論）における証明可能性において、理論を構成する論理式は無限個かもしれないので list ではなく Ensemble で符号化する必要がある:
Definition System := Ensemble Formula.
Definition SysPrf (T : System) (f : Formula) :=
exists Axm : Formulas,
(exists prf : Prf Axm f,
(forall g : Formula, In g Axm -> mem _ T g)).
Definition Inconsistent (T : System) :=
forall f : Formula, SysPrf T f.
Definition Consistent (T : System) :=
exists f : Formula, ~ SysPrf T f.
Definition wConsistent (T : System) :=
forall (f : Formula) (v : nat),
(forall x : nat, In x (freeVarFormula LNN f) -> v = x) ->
SysPrf T (existH v (notH f)) ->
exists n : nat, ~ SysPrf T (substituteFormula LNN f v (natToTerm n)).
03. 算術
不完全性定理が定義される算術理論として NN を構成する。NNは算術に関する9つの文からなる。この9つの文には対応する9つの公理図式が存在するが、それらはほぼ自明に証明できる:
Definition NN1 := forallH 0 (notH (equal (Succ (var 0)) Zero)).
(*後略*)
Definition NN :=
Ensembles.Add _
(Ensembles.Add _
(Ensembles.Add _
(Ensembles.Add _
(Ensembles.Add _ (Ensembles.Add _ (Ensembles.Add _ (Ensembles.Add _ (Singleton _ NN1) NN2) NN3) NN4) NN5)
NN6) NN7) NN8) NN9.
Lemma nn1 : forall a : Term, SysPrf NN (notH (equal (Succ a) Zero)). (*後略*)
同様にPAも構成する。PAは数学的帰納法に対応する公理図式を含んでおり、可算無限個の公理からなる点がNNと違うけれど、構成的に定義できる点では同じ:
(* 公理図式は Formula -> Prop と符号化できるので *)
Definition InductionSchema (f : Formula) : Prop :=
exists g : Formula, (exists v : nat, f = PA7 g v).
(* PA もまた Ensemble Formula として符号化できる *)
Definition PA :=
Ensembles.Add _
(Ensembles.Add _ (Ensembles.Add _ (Ensembles.Add _ (Ensembles.Add _ (Ensembles.Add _ InductionSchema PA1) PA2) PA3) PA4)
PA5) PA6.
04. ゲーデル数化
Cantor の pairing function を使うとnat*nat から nat への単射が構成できる:
Definition sumToN (n : nat) :=
nat_rec (fun _ => nat) 0 (fun x y : nat => S x + y) n.
Definition cPair (a b : nat) := a + sumToN (a + b).
よって対象言語の各記号を適当なルールでnatに符号化したとき:
Definition codeLNTFunction (f : LNTFunction) : nat :=
match f with
| Plus => 0
| Times => 1
| Succ => 2
| Zero => 3
end.
項・論理式・証明からnatへの単射も自然に構成できる:
Fixpoint codeTerm (t : Term) : nat :=
match t with
| fol.var n => cPair 0 n
| fol.apply f ts => cPair (S (codeF f)) (codeTerms _ ts)
end
with codeTerms (n : nat) (ts : Terms n) {struct ts} : nat :=
match ts with
| Tnil => 0
| Tcons n t ss => S (cPair (codeTerm t) (codeTerms n ss))
end.
Fixpoint codeFormula (f : Formula) : nat :=
match f with
| fol.equal t1 t2 => cPair 0 (cPair (codeTerm t1) (codeTerm t2))
| fol.impH f1 f2 => cPair 1 (cPair (codeFormula f1) (codeFormula f2))
| fol.notH f1 => cPair 2 (codeFormula f1)
| fol.forallH n f1 => cPair 3 (cPair n (codeFormula f1))
| fol.atomic R ts => cPair (4+(codeR R)) (codeTerms _ ts)
end.
Fixpoint codePrf (Z : Formulas) (f : Formula) (prf : Prf Z f) {struct prf} :
nat :=
match prf with
| AXM A => cPair 0 (codeFormula A)
| MP Axm1 Axm2 A B rec1 rec2 =>
cPair 1
(cPair
(cPair (cPair 1 (cPair (codeFormula A) (codeFormula B)))
(codePrf _ _ rec1)) (cPair (codeFormula A) (codePrf _ _ rec2)))
| GEN Axm A v _ rec =>
cPair 2 (cPair v (cPair (codeFormula A) (codePrf _ _ rec)))
| IMP1 A B => cPair 3 (cPair (codeFormula A) (codeFormula B))
(*中略*)
| EQ4 r => cPair 12 (codeR r)
| EQ5 f => cPair 13 (codeF f)
end.
そしてnatをnatToTermを使い、対象言語上の数項と同一視する。
以上により、メタレベルの存在物――特に証明――を対象言語で扱う第一段階が完了した。第二段階はメタレベルでの集合や関係――例えば定理全体――を対象言語で表現することだ。それには算術階層や 表現可能性といった概念を経由する必要がある。
05. 原始再帰性
原始再帰性もまた、統語論と意味論の両面で構成する。まずは統語的な原始再帰性を帰納的に定義する:
Inductive PrimRec : nat -> Set :=
| succFunc : PrimRec 1
| zeroFunc : PrimRec 0
| projFunc : forall n m : nat, m < n -> PrimRec n
| composeFunc :
forall (n m : nat) (g : PrimRecs n m) (h : PrimRec m),
PrimRec n
| primRecFunc :
forall (n : nat) (g : PrimRec n) (h : PrimRec (S (S n))),
PrimRec (S n)
with PrimRecs : nat -> nat -> Set :=
| PRnil : forall n : nat, PrimRecs n 0
| PRcons : forall n m : nat, PrimRec n -> PrimRecs n m ->
PrimRecs n (S m).
続いて具体的な関数実装を結びつける。例えば射影関数の実装:
(* 射影関数の実装 *)
Fixpoint evalProjFunc (n : nat) : forall m : nat, m < n -> naryFunc n :=
match n = return (forall m : nat, m < n -> naryFunc n) with
| O => fun (m : nat) (l : m < 0) => False_rec _ (lt_n_O _ l)
| S n' =>
fun (m : nat) (l : m < S n') =>
match eq_nat_dec m n' with
| left _ => fun a : nat => evalConstFunc _ a
| right l1 =>
fun _ =>
evalProjFunc n' m
match le_lt_or_eq _ _ (lt_n_Sm_le _ _ l) with
| or_introl l2 => l2
| or_intror l2 => False_ind _ (l1 l2)
end
end
end.
(* 意味論=統語論と実装を結びつける *)
Fixpoint evalPrimRec (n : nat) (f : PrimRec n) {struct f} :
naryFunc n :=
match f in (PrimRec n) return (naryFunc n) with
| succFunc => S
| zeroFunc => 0
| projFunc n m pf => evalProjFunc n m pf
| composeFunc n m l f =>
evalComposeFunc n m (evalPrimRecs _ _ l) (evalPrimRec _ f)
| primRecFunc n g h =>
evalPrimRecFunc n (evalPrimRec _ g) (evalPrimRec _ h)
end
with evalPrimRecs (n m : nat) (fs : PrimRecs n m) {struct fs} :
Vector.t (naryFunc n) m :=
match fs in (PrimRecs n m) return (Vector.t (naryFunc n) m) with
| PRnil a => Vector.nil (naryFunc a)
| PRcons a b g gs =>
Vector.cons _ (evalPrimRec _ g) _ (evalPrimRecs _ _ gs)
end.
すると、Coqでの――つまりメタレベルでの――関数や関係の原子再帰性を記述できる。extEqual はCoqでいうところの functional extensionality と同じことであるが、Axiom-freeにやるという全体方針を踏襲して、自前で実装している:
(* 関数に関しPRという性質を定める *)
Definition isPR (n : nat) (f : naryFunc n) : Set :=
{p : PrimRec n | extEqual n (evalPrimRec _ p) f}.
(* 関係に関しても特徴関数経由で同様に定義可能 *)
Definition isPRrel (n : nat) (R : naryRel n) : Set :=
isPR n (charFunction n R).
特に nat_rec が原子再帰的であることが示せる
Lemma indIsPR :
forall f : nat -> nat -> nat,
isPR 2 f -> forall g : nat, isPR 1
(fun a: nat => nat_rec (fun n: nat => nat) g (fun x y: nat => f x y) a).
これにより、Cantorのpairing function が原始再帰的であることがいえ、芋づる式に各種ゲーデル数化が原子再帰的であることが直ちに従う。
06. 表現可能性
原始再帰性はメタレベルの関数・関係に対する性質である。しかし対象言語すなわち算術に対応物がある。以下のように原始再帰関数と論理式を対応付けたとき:
Fixpoint primRecFormula (n: nat) (f: PrimRec n) {struct f}: Formula :=
match f with
| succFunc => succFormula
| zeroFunc => zeroFormula
| projFunc n m _ => projFormula m
| composeFunc n m g h =>
composeSigmaFormula n n m (primRecsFormula n m g) (primRecFormula m h)
| primRecFunc n g h =>
primRecSigmaFormula n (primRecFormula n g) (primRecFormula (S (S n)) h)
end
with primRecsFormula (n m : nat) (fs : PrimRecs n m) {struct fs} :
Vector.t (Formula * naryFunc n) m :=
match fs in (PrimRecs n m) return (Vector.t (Formula * naryFunc n) m) with
| PRnil n => Vector.nil _
| PRcons n m f fs' =>
Vector.cons (Formula * naryFunc n) (primRecFormula n f, evalPrimRec n f) m
(primRecsFormula n m fs')
end.
これらの開論理式は、その対応物をrepresentする。すなわち、その論理式に数項n, m, ... を代入して得られる文と、対応する関数に 数n,m,... を適用した数c が 証明可能性⊢ における同値となる:
Fixpoint RepresentableHelp (n : nat) : naryFunc n -> Formula -> Prop :=
match n return (naryFunc n -> Formula -> Prop) with
| O =>
fun (f : naryFunc 0) (A : Formula) =>
SysPrf T (iffH A (equal (var 0) (natToTerm f)))
| S m =>
fun (f : naryFunc (S m)) (A : Formula) =>
forall a : nat,
RepresentableHelp m (f a) (substituteFormula LNN A (S m) (natToTerm a))
end.
Definition Representable (n : nat) (f : naryFunc n)
(A : Formula) : Prop :=
(forall v : nat, In v (freeVarFormula LNN A) -> v <= n) /\
RepresentableHelp n f A.
Lemma primRecRepresentable :
forall (n : nat) (f : naryFunc n) (p : isPR n f),
Representable n f (primRecFormula n (proj1_sig p)).
representableならば、expressibleである。つまり、要素性と証明可能性が一致するように、メタな集合の対応物である開論理式を作ることができる
Fixpoint ExpressibleHelp (n : nat) : naryRel n -> Formula -> Prop :=
match n return (naryRel n -> Formula -> Prop) with
| O =>
fun (R : naryRel 0) (A : Formula) =>
match R with
| true => SysPrf T A
| false => SysPrf T (notH A)
end
| S m =>
fun (R : naryRel (S m)) (A : Formula) =>
forall a : nat,
ExpressibleHelp m (R a) (substituteFormula LNN A (S m) (natToTerm a))
end.
Definition Expressible (n : nat) (R : naryRel n) (A : Formula) : Prop :=
(forall v : nat, In v (freeVarFormula LNN A) -> v <= n /\ v <> 0) /\
ExpressibleHelp n R A.
08. 証明述語の構成
対象言語上に証明述語 codeSysPrf(x,y) を構成したい。つまりaをゲーデル数とする論理式fの証明列のゲーデル数がb であるときにのみ、codeSysPrf(a̅,b̅) が証明できるような開論理式codeSysPrf(x,y)を構成したい。「aをゲーデル数とする論理式fの証明列のゲーデル数がb である」が原始再帰的であることから、それは実際に可能で、具体的に構成することができる:
Definition codeSysPrf : Formula := (*略*)
(* 注: Uは x∈U ⇒ U ⊢ f([x]) なる集合。よって g に関する部分は「証明列の各項が証明可能ならば」と読めばよい。*)
Lemma codeSysPrfCorrect1 :
forall (f : fol.Formula L) (A : list (fol.Formula L)) (p : Prf L A f),
(forall g : fol.Formula L, In g A -> mem _ U g) ->
SysPrf T
(substituteFormula LNN
(substituteFormula LNN codeSysPrf 0
(natToTerm (codeFormula L codeF codeR f))) 1
(natToTerm (codePrf L codeF codeR A f p))).
(*略*)
Lemma codeSysPrfCorrect2 :
forall (f : fol.Formula L) (A : fol.Formulas L),
(exists g : fol.Formula L, In g A /\ ~ mem _ U g) ->
forall p : Prf L A f,
SysPrf T
(notH
(substituteFormula LNN
(substituteFormula LNN codeSysPrf 0
(natToTerm (codeFormula L codeF codeR f))) 1
(natToTerm (codePrf L codeF codeR A f p)))).
Lemma codeSysPrfCorrect3 :
forall (f : fol.Formula L) (n : nat),
(forall (A : list (fol.Formula L)) (p : Prf L A f),
n <> codePrf L codeF codeR A f p) ->
SysPrf T
(notH
(substituteFormula LNN
(substituteFormula LNN codeSysPrf 0
(natToTerm (codeFormula L codeF codeR f))) 1
(natToTerm n))).
証明述語からΣ1論理式である可証性述語を作れる。
Definition codeSysPf : Formula := existH 1 codeSysPrf.
09. 対角化定理とゲーデル文の構成
NNにおける不動点定理を 可証性述語codeSysPf の否定に対して適用することでゲーデル文G（私は証明できない）を構成する:
Lemma FixPointLNN :
forall (A : Formula) (v : nat),
{B : Formula |
SysPrf NN
(iffH B (substituteFormula LNN A v (natToTermLNN (codeFormula B)))) /\
(forall x : nat,
In x (freeVarFormula LNN B) <->
In x (list_remove _ eq_nat_dec v (freeVarFormula LNN A)))}
(* 後略 *)
Definition G := let (a,_) := FixPointLNN (notH codeSysPf) 0 in a.
ゲーデル文が構成できれば不完全性定理はほぼ自明。
10. 第一不完全性定理
ゲーデルはω無矛盾な体系に証明も反証もできない文があることを示した:
Theorem Goedel'sIncompleteness1st :
wConsistent T ->
exists f : Formula,
~ SysPrf T f /\
~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f)).
前提条件を無矛盾性に緩めた第一不完全性定理はロッサーによって示された。証明述語を少し技術的に複雑にし（つまり関係「aがRの証明のゲーデル数であればb<aなるbが存在してbは￢Rの証明のゲーデル数である」とし）、不動点定理を使ってロッサー文を作ることで不完全性を示せる。goedelでは定理が決定可能集合であることを前提としており、その要因を著者はCoqが直観主義論理であることに帰着させているけれど、それが正しいかどうかは不明。一般には理論の決定性は不要のはず:
Theorem Rosser'sIncompleteness :
(forall x : Formula, mem _ T x \/ ~ mem _ T x) ->
exists f : Formula,
(forall v : nat, ~ In v (freeVarFormula LNN f)) /\
(SysPrf T f \/ SysPrf T (notH f) -> Inconsistent LNN T).
11. 読んでみた感想
- 論文でも触れてたけれど, 項や原始再帰性の定義である相互再帰的な定義方法である必要はないように思う
- 十分一般的な枠組みで議論しているので多くの定理・証明が長く読みずらい。
- 自分でも実装してみたい。一般的ではなく、PA-に特化した形でやればそれほど多くの行数にならないと思う。
- Axiom-freeで、つまり構成的に証明ができることに感心した。