日々の流転

λ. Sets in types, types in sets

Sets in types, types in sets by Benjamin Werner, in Proceedings of TACS'97

We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible cardinals in the set theory. The main result is that both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent. Both encodings are quite elementary: type theory is interpreted in set theory through a generalization of Coquand 's simple proof-irrelevance interpretation. Set theory is encoded in type theory using a variant of Aczel's encoding; we have formally checked this last part using the Coq proof assistant.

ytbさんの 2008-06-14 - あいまいな本日の私 より。

概要

集合論ZFCと型理論CICの間の埋め込みの話。 ZFC_i を ZFC に i 個の到達不能基数を加えたもの、CIC_i を型の宇宙を Type_i までに制限した CIC として、その間の以下の図のような相対無矛盾性の関係があることを示している(矢印の逆向きに埋め込みが可能)。

少し詳しい話

ただし、この論文で扱っている CIC (Calculus of Inductive Construction) は、Coquand らの CC (Calculus of Construction) の変種である Luo の ECC(Extended Calculus of Constructions, c.f. 20060503#p02) に、帰納的データ型を追加したもの。なので、現在のCoqとは違ってPropが非可述的(impredicative)な宇宙になっている。(2018-03-06追記: CoqのPropはimpredicativeか。当時は何を勘違いしてたんだろう……)

また、CICそのものではなくCICに以下のようなものを加えたものを考えている。

排中律

EM := ΠP : Prop. P∨¬P

Type-theoretical Description Axiom on level i:

TTDA_i := ΠA,B : Type_i. ΠP : A → B → Prop. (Πa : A. ∃b : B. (P a b)) → ∃f : A→B. (Πa : A. P a (f a))

Type-theoretical Choice Axiom on level i:

TTCA_i := ΠA : Type_i. ΠR : A→A→Prop. (equiv A R) → ∃f: A→A. Πx,y : A. (R x y) → (f x = f y)

ただし、ここでの存在記号は通常の依存直和(Σ-types)ではなく ∃a : A. P a := ΠX : Prop. (Πa : A. P a → X) → X で定義されるものなので注意。

で、CICからZFCへの埋め込みは、Propに関してはproof-irrelevantな解釈を用い、他に関しては通常の集合論的な解釈をしている。 それによって、ZFC_{i-1} が無矛盾ならば、CIC_i + EM + TTDA_1 + … + TTDA_n + TTCA_1 + … + TTCA_n が無矛盾であることを示している。

一方、ZFCのCICへの埋め込みに関しては、まず集合と等号と要素関係を以下のように帰納的に定義して埋め込みをしている。

Inductive Set : Type_{i+1} :=
  | sup : ΠA : Type_i. (A → Set) → Set.

Fixpoint Eq : Set → Set → Prop :=
  fun (sup A f : Set) (sup B g : Set) ⇒
    (Πa : A. ∃b : B. Eq (f a) (g b)) ∧
    (Πb : B. ∃a : A. Eq (f a) (g b)).

Definition In : Set → Set → Prop :=
  fun (E : Set) (sup A f : Set) ⇒
    ∃a : A. Eq E (f a).

その上で以下のようなことを示している

• Z は CIC_2 + EM にエンコードできる
• ZF は CIC_2 + EM + TTDA_3 にエンコードできる
• ZFC は CIC_3 + EM + TTDA_3 + TTCA_3 にエンコードできる
• ZFC_n は CIC_{n+2} + EM + TTDA_{n+1} にエンコードできる

余談

以前にOCaml-Nagoyaの飲み会に参加したときに、普通の数学をそのままCoq上に持ってくるには集合論をエンコードする必要があるのではないかという話をして、そのときに念頭にあったのはここでやっているようなものだったので、具体的なエンコードとその性質が分かってすっきりした。

ただ、排中律に関してはEMを追加すれば良いし、集合論と型理論の違いについてはこのような埋め込みを考えれば良いとしても、一階述語論理と高階述語論理の違いが問題になることはないのか、その辺りはまだよく分からない。