ZFC を Coq で符号化したコード coq-contribs/zfc を読みときます。

1. 概要

公理的集合論のひとつであるZFCをCoqで符号化した成果物が Coq の公式contribレポジトリに入っているのでそれを読みときます。

やっていることはZFCのモデル構築です。具体的には Inductive に集合型 Ens を定義して、Ensに対する各種操作・性質を構成して ZFCの各種公理を証明します。公理を証明というと変な感じですが、公理を仕様だとみなして仕様を満たしていることを確認しているわけです。さて、ZFCのモデルを構成できるならば ZFCが無矛盾ということになるのではないか？と疑問がでてきますが、ここで言えるのは「CIC/Coq が無矛盾ならZFCのモデルが存在する」ということなので、ZFCの無矛盾性をCICの無矛盾性に還元しただけです。そしてCICも不完全性定理が適用できる体系なのでCICの無矛盾性はCIC自身では証明できません。

また、Coqを使っているので構成的なZFと思われますが、そうではありません。Impredicativeなソートつまり Prop を使っているので非構成的な普通のZFCです。そのため構成的なZFCでは述べづらい冪集合を作れたりするので表現力は増しています。

コードはいくつかのファイルに分散されていますが、それらを単一のファイルにまとめたzfc.v があるのでそれを読んでもよいです。

2. 集合型 Ens

Coq で集合といえば A->Prop で符号化する Ensembles ライブラリです。しかし zfc では別の方法で符号化します。定義は以下:

Inductive Ens := sup (A:Type) (f: A->Ens).

短いですが読みとくのは少し骨がおれます。ただひとつ構成子 sup を持ち sup A f : Ens と型がつきます。AはTypeなので bool型でもnat型でもなんであっても構いません。f はAからEns への任意の関数です。例えば Aがboolなら f true, f false という二つの Ens が得られます。これらが（後で定義しますが）集合 sup A f の要素となります。説明のため以下では、Aを台, f を要素関数と呼称します（多分 sup は台/support の略称）。Ens から台と要素関数を射影する関数 pi1, pi2 も容易に構成できます。

さて、上記のような符号化(reflexive encoding) では、具体的なEnsを挙げるのが難しいです。台が False型(もしくはその同型) の時には自明な一つのEnsが得られるのでこれに Vide と名前をつけます（空集合のフランス語）:

Inductive F : Set :=.
Definition Vide := sup F (fun x:F => match x with end).

一つでもEnsが構成できれば、あとは定義に従っていくつもEnsを作っていけます。

3. Ensに関する操作と性質

Ens はZFCでの集合を企図しているので関連する操作や性質を定義していきます。自然に定義するとそれがZFCの公理を満たすことにつながります

3.1 「=, ∈, ⊆」

集合の等値性EQ:Ens->Ens->Prop、集合の要素関係 IN: Ens->Ens->Prop 、集合の包含関係 INC: Ens->Ens->Ens は自然に定義できるでしょう。等値性は外延的に定めます:

(*注: EXType は @Logic.ex と同じ。つまり
EXType _ (fun y : B => eq1 x (g y)) は exists y, eq1 x (g y) と同じ *)
Definition EQ : Ens -> Ens -> Prop.
simple induction 1; intros A f eq1.
simple induction 1; intros B g eq2.
apply and.
exact (forall x : A, EXType _ (fun y : B => eq1 x (g y))).
exact (forall y : B, EXType _ (fun x : A => eq1 x (g y))).
Defined.

Definition IN (E1 E2 : Ens) : Prop :=
  match E2 with sup A f => EXType _ (fun y : A => EQ E1 (f y)) end.

Definition INC : Ens -> Ens -> Prop.
intros E1 E2. exact (forall E : Ens, IN E E1 -> IN E E2). Defined.

こうして定めた EQ が同値関係であること(EQ_refl, EQ_tran, EQ_sym), INCが半順序関係であること (INC_refl, INC_tran INC_EQ) は容易に証明できます。

3-2. ペア・シングルトン・分出

EnsからEnsを作るような操作としてペアやシングルトンや分出(特定の性質を満たす要素だけからなる集合)があります。これらもEnsの定義から自然に定義できます。

ペア関数 Paire: Ens->Ens->Ens は、台として bool を取ればよさそうです。シングルトン関数 Sing : Ens -> Ens は自身とのペアとすればよさそうです（unit型を台としてもよさそうですが実装はペアを使っています）。

分出 Comp: Ens->(Ens->Prop)->Ensに関してです。性質 P:Ens->Propが与えられているとします。E := sup A f なるEnsを考えます。fun x:A => P (f x) なる性質は「Pを満たすEの要素」であるときに成立するため、台として sig (fun x=>P (f x))) をとり、要素関数として、その第一射影に f を適用しましょう:

Definition Comp : Ens -> (Ens -> Prop) -> Ens.
simple induction 1; intros A f fr P.
apply (sup (sig A (fun x => P (f x)))).
simple induction 1; intros x p; exact (f x).
Defined.

3-3. 和・積・冪

和 Union: Ens->Ens についてです。sup A f なる E に対して fun x:A => pi1 (f x) はEの各要素についてそれぞれ台を与えます。同様に fun x:A => pi2 (f x) はEの各要素についてそれぞれ要素関数を与えます。よって台として sigT (fun x:A => pi1 (f x)) を採用し、その第一射影に f をかけてEの要素 f aを得て、その要素関数に第二射影にかけることで (f a) の要素が得られることから、和集合が定義できそうです:

(* 注: depprod は @sigT と同じ意味 *)
Definition Union : forall E : Ens, Ens.
simple induction 1; intros A f r.
apply (sup (depprod A (fun x : A => pi1 (f x)))).
simple induction 1; intros a b.
exact (pi2 (f a) b).
Defined.

冪 Power: Ens -> Ens を考えます。入力となる集合Eに対し、任意のEの部分集合E' には、Eの台Aのある集まり P: A->Prop が存在して E' が f による P の像となります。したがって、台を A->Prop: Type とし、以下のような操作で冪を定義することができそうです:

(* 注: dep_i は existT と同じ意味 *)
Definition Power (E : Ens) : Ens := match E with sup A f =>
 sup _ (fun P : A -> Prop =>
   sup _ (fun c : depprod A (fun a : A => P a) =>
      match c with dep_i a p => f a end))
 end.

3-4. 順序対, 直積

順序対Couple: Ens->Ens->Ens, 直積 Prod: Ens->Ens->Ens は自然に構成できます:

Definition Couple (E E' : Ens) := Paire (Sing E) (Paire Vide (Sing E')).
(* 注: pair_t は pair と同じ意味 *)
Definition Prod (E E' : Ens) : Ens := match E, E' with
  | sup A f, sup A' f' =>
      sup _ (fun c : prod_t A A' =>
         match c with pair_t a a' => Couple (f a) (f' a') end)
  end.

3-5. 順序数

「xは順序数である」という性質 Ord: Ens->Prop もInductiveに定義できます:

Definition Succ (E : Ens) := Union (Paire E (Sing E)).
Inductive Ord : Ens -> Prop :=
  | Oo : Ord Vide
  | So : forall E : Ens, Ord E -> Ord (Succ E)
  | Lo : forall E : Ens, (forall e : Ens, IN e E -> Ord e) -> Ord (Union E)
  | Eo : forall E E' : Ens, Ord E -> EQ E E' -> Ord E'.

特に nat型で指数付けされたEns（0がVideで1増やすごとにSuccを掛けていく) であるNat: nat->Ens を定義すると任意のn で Nat n は順序数になります。Natを要素関数とする Ens を Omega と定義すると Omega も順序数であることが証明できます。

4. 公理の符号化と証明

公理的集合論の各種公理は、上述のようなEnsやPaireなどの定義を使うと証明できます。Coqでどのように符号化されるのかを見ていきましょう。

まず読みやすさのため、以下のNotationを導入します。このNotationはコードにはなく、私が付け加えたものです:

Require Import Setoid.

Notation "∅" := Vide.
Notation "a ≅ b" := (EQ a b)  (at level 30).
Notation "a ∈ b" := (IN a b)  (at level 30).
Notation "a ⊆ b" := (INC a b)  (at level 30).
Notation "{ a , b }" := (Paire a b) (at level 20).
Notation "[ a | P ]" := (Comp a P) (at level 20).

まず、外延性公理ですがコードコメントには easy としか書かれておらず証明がなかったので私のほうで証明してみます:

(* 外延性公理 *) Theorem EQ_spec:
  forall x y, (forall z, z ∈ x <-> z ∈ y) <-> x ≅ y.
Proof. split;intros H. - apply INC_EQ; unfold INC; intros z Hz.
now rewrite <-H. now rewrite H. - split; intros.
eapply IN_sound_right; eauto. eapply IN_sound_right; eauto.
auto with zfc. Qed.

空集合の公理・対の公理・分出公理・和集合の公理・冪集合の公理・無限公理に関しては証明があるので確認します。無限公理に関しては必要な部品がそろっているものの直接の証明がなかったので私のほうで作っておきました:

(* 空集合の公理 *) Check  Vide_est_vide:
  forall x, x ∈ ∅ -> F.
(* 対の公理 *) Check Paire_IN:
  forall a b x, x ∈ {a, b} -> x ≅ a \/ x ≅ b.
(* 分出公理 *) Check Comp_INC:
   forall x P, [x | P] ⊆ x.
(* 和集合の公理 *) Check Union_IN :
    forall x y, y ∈ Union x -> EXType _ (fun z => z ∈ x /\ y ∈ z).
(* 冪集合の公理 *) Theorem Power_spec :
    forall x y,  y ⊆ x <-> y ∈ (Power x).
  Proof. split. apply INC_IN_Power. apply IN_Power_INC. Qed.
(* 無限公理 *) Theorem Omega_spec:
    ∅ ∈ Omega /\ (forall x, x ∈ Omega -> Succ x ∈ Omega).
Proof. split. unfold IN, Omega. apply EXTypei with 0. auto with zfc.
intros. destruct (IN_Omega_EXType _ H) as [n Hn].
enough (Nat (S n) ≅ Succ x). eapply IN_sound_left.
eassumption. auto with zfc.
assert (Nat (S n) ≅ Succ (Nat n)). auto with zfc.
eapply EQ_tran; eauto. unfold Succ. apply Union_sound.
assert ({Nat n, Sing x} ≅  {x,Sing x}). auto with zfc.
eapply EQ_tran. apply Paire_sound_left. eassumption.
auto with zfc. Qed.

さて、置換公理ですが状況が少し込み入っています。まずCoqの(Type systemでの)選択公理/choice を仮定すると集まりの公理/collection が証明できます。さらに排中律を仮定すると置換公理が証明できます。つまり、CIC + ClassicalChoice + Cassical のように CICに公理を追加することで、集まりの公理と選択公理が証明できます:

  (* 集まりの公理 *) Check Choice_Collection: 
  choice ->
  forall P : Ens -> Ens -> Prop,
  (forall x x' y, x ≅ x' -> P x y -> P x' y) ->
  (forall x, EXType _ (P x)) ->
  forall E, EXType _ (fun E2 => forall x, x ∈ E -> EXType Ens (fun y => y ∈ E2 /\ P x y)).

  (* 置換公理 *) Check classical_Collection_Replacement :
  (forall P : Prop, P \/ (P -> False)) -> 
  collection -> 
  forall P : Ens -> Ens -> Prop,
  functional P ->
  (forall x y y' : Ens, y ≅ y' -> P x y -> P x y') ->
  (forall x x' y : Ens, x ≅ x' -> P x y -> P x' y) ->
  forall X, EXType _ (fun Y => forall y,
     (y ∈ Y -> EXType _ (fun x => x ∈ X /\ P x y)) /\
     (EXType _ (fun x => x ∈ X /\ P x y) -> y ∈ Y)).

5. 歴史的経緯

あまり詳しくないので参考程度にして下さい

ZFとは別に構成的なZF集合論CZFが研究されてきました。CZFでは排中律や選択公理といった非構成的なものを排除します。その結果公理の形も少し変わり例えば分出公理はpredicativeなものへと弱められたりします。CZFは構成的なのでLofの型理論で符号化できます――つまりCoqでCZFを符号化できます――。しかし、本稿のコード coq-contrib/zfc は impredicative な道具立てを積極的に使うことで CZF ではなく ZF を直接符号化しています。副作用としては code extraction ができなくなっていますが、利点として冪集合を明確に定義することができるなど表現力が高まっています。

6. おまけ

ラッセルのパラドックスが起きないか心配になるかもしれません。別の言い方をするとEnsは集合だけでなくProperClassにもなっているのではないか？という疑問はあるかもしれません。以下の定理はEnsがProperClassでないことの証明です:

Check Russell:  forall x, (forall y, y ∈ x) -> False.

Coq で ZFC