日々の流転

λ. 「アイルランドにおける貧民の子女が、その両親ならびに国家にとっての重荷となることを防止し、かつ社会に対して有用ならしめんとする方法についての私案」を読んだ。「リーマンの、リーマンによる、リーマン(あるいはその予備軍)のための教養講座」を読んだ。

λ. 東方風神録を注文

「東方風神録」の店頭委託は9/21発売ということなので早速注文。ついでに、「うみねこのなく頃に」も一緒に注文してみた。

λ. 集合論を知らない子ども達

あまりも当たり前過ぎて21世紀に入ってから言葉にだしたことはあまりないのですが、当然のことながら、数学というのは、集合論を理解して初めて「出来る」と言うのです。 数学が出来る、という状態は「集合論が出来る」という状態の延長線上にあるべきで、集合論を理解していないということは数学を理解していない、つまり数学を理解していないのとほぼ同じだと思います。

最近は圏論とか呼ばれる、いわゆる抽象数学を用いる分野が増えてきていますが、それでも依然として、数学というのは集合論を使って構成されるもので、数学というものは全て集合論の延長上にあると思っています。 その意識がないと、たとえ公理や定理を書いていても、矛盾してしまったり、モデルがうまく作れなかったりしたときに「なぜだろう?」ということがピンとこないことになります。

まだ大学に入って無くて、圏論のような抽象数学を楽しんでいる若い人たちには、ぜひ集合論を勉強してみることを勧めます。 最近は素晴らしい時代になったもので、ごく初歩的な入門はその辺の教科書でもすることができます。 しかし本格的に集合論を遊びたくなったら、JechやKunenを使うのがお勧めです。 今の集合論は複雑になりすぎていて、初心者が全ての理論を知ろうとすると膨大な時間と労力がかかります。 しかし、最終的にはそれは全て知らなければならないことですし、知っておくべきことです。

最近は、全くの文化系の女の子が、わずか数ヶ月の研修で「ソフトウェア検証」と称して定理を書くような商売もあるらしいのですが、そんなときにもぜひ集合論を勉強してもらいたいと思います。集合論が解らないと、そもそも数学の構造やモデルの仕組みがわからないということなので、何が問題なのかわからないことの方が多くなると思います。

どれだけ数学が進化しても、その仕組みを理解していることは絶対に必要です。

筆算ができない人が電卓を使い続けたときに答えが正しいのか間違っているのかわからないのと同様、集合論ができない人が書いた公理系は、一見無矛盾なように見えたとしても、それは奇跡のようなバランス、自転車で言えば補助輪がついた状態で奇跡的に動いているに過ぎず、なにか未知の問題が発生したときに素早く公理系の内部でおきていることに直感を巡らせ、適切な処置・対応をするためには集合論の理解は不可欠と言って良いでしょう。

さらにいえば、集合論よりさらに下のレイヤーである、一階述語論理を理解しているとさらに理想的です。

昔、数学の本といえば集合論の本を意味しました。しかし、今の若い学生達は、下のような図をみても何を意味するか瞬時にわからないのではないでしょうか。

<URL:http://ja.wikipedia.org/wiki/%E3%83%99%E3%83%B3%E5%9B%B3>

数学的対象は全て集合の組み合わせでできています。 数学を構成する要素は全て集合論と一階述語論理なので、集合論を理解しないと数学の原理を理解していないことになります。 最低でも、ZFCで自然数と整数を作れる程度の理解はしておいて欲しいと思います。 集合論、一階述語論理の2つは、現在でもあらゆる数学の基礎になっているので、最低限おさえておきたいところです。

最後に参考文献をまとめておきます。 ただ読むだけでもとても面白い本ばかりです。

• Thomas J. Jech, Set Theory
• Kenneth Kunen, Set Theory: An Introduction to Independence Proofs
• Akihiro Kanamori, The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings
• Keith J. Devlin, Constructibility

元ネタ

• マシン語を知らない子ども達 - Keep Crazy;shi3zの日記
• アルゴリズムを知らない子ども達 - val it: α → α = fun

λ. 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を追加すれば良いし、集合論と型理論の違いについてはこのような埋め込みを考えれば良いとしても、一階述語論理と高階述語論理の違いが問題になることはないのか、その辺りはまだよく分からない。