型の理論に入門しそこねた・・・

９月３日に
マルレク・サブゼミ「型の理論入門」
https://type-theory.peatix.com/

に行ったことは行ったんだけど、
会場が理科室みたいなかんじで、椅子に背もたれがなくて
（理科室みたいな椅子）、なんかつらかったのと、

話を聞いてても、ときめかなかったので、
丸山先生には申し訳ないけど、
ありがとうと感謝して、後半のゼミを断捨離してきた
（つまり、ぶっちした）ので、

前半だけ、メモメモ

---

カントール没後１００年

●カントールの集合論
カントール
・順序数
　無限の順序数ω、
　ω　　　１，２，３・・・
　ｗ＋１　１，２，３・・・ω
　ｗ＋ｗ
　　：　
　ｗのｗ乗
→でも、加算回で、特定のページにたどり着く
ε０（いぷしろんぜろ）→べき乗についてのＦＩＸ　ＰＯＩＮＴ
　カントール　のーまる　フォーム

　ゲンツェン
　　数論の無矛盾性証明：ペアノ数論の無矛盾性を証明
　　→ソビエトの収容所で亡くなる

・無限集合の要素の個数
　数えることとは切り離して、個数が存在する
　無限集合の場合：１対１が対応つく場合
　無限の場合：部分は全体と同じ数の要素を持つ
　　　→ユークリッド幾何学
　自然数と有理数全体とは一対一に対応する
　→ゲーデル：１つの自然数に対応付けられる
　対角線論法

・カントールが証明できなかったこと：連続体仮設
　加算無限集合の濃度をℵ₀（あれふぜろ）とよぶ
　連続体仮設
　一般連続体仮設
　→ヒルベルトの２３の問題の１番目

・矛盾
　カントールの集合概念
　Fregeの定式化(Comprehension Axiom)
　ある述語φについてφ（ｘ）が成り立つすべての要素Ｘを集めた集合Ｙ
→ラッセルの逆理
　自己参照的な定義、非述語的な定義が問題

・集合論の矛盾
　ラッセルの型の理論
　ＰがなりたたないことをすべてのＸについて成り立つならば（対偶）
　　Ｐが成り立つあるＸが存在する？？
　→　直観主義、構成主義
　→　ヒルベルト・プログラムと「有限の立場」
　有限の立場で数学の証明

証明
・ゲーテルの不完全性定理

　照明も半焼もできない命題が存在する
　体系の無矛盾性はその体系の中で証明できない
・計算とは何か、証明とは何か？
　　ゲーデルの機能関数論
　　チャーチのラムダ・カリキュラス
　　チューリングのチューリングマシン
　→同値
　チャーチチューリングのテーゼ：複雑性理論の第一世代
　　→証明できない
　証明可能性と計算可能性の同一性の認識→コンピューターはまだ存在しない


非カントール
　ゲーデル：連続体仮説と
　コーエン　連続体仮説と集合論の独立性

カテゴリー論
　集合論をＳＥＴで集合のカテゴリーＰをとってくる
　変異集合

新しい型の理論
　カーリーハスケル（カリーハワードのカリーと、ハスケル
は同一人物）
　カリーハワード対応 Lisp λ計算する
　型付きラムダ計算
　ハワードによる発展：論理式はラムダ計算の型とみなすことができる
　　ｐが命題Ｐの証明であることをｐ：Ｐ
　　ｐは型Ｐの要素である　ｐ：Ｐ
　→ＰＡＴ Propositions as Types Proof as Terms
　→Coq

従来型

Martin-Lofの型の論理
Dependent Type
　
Dependent Type と Polymorphism
Infuctive Type（帰納的型）

Martin-Lof→ML,Haskell
Curry-Howard　Coq,Agda

Univalent Foundation
　voevodsky
　新しい型の理論ＨｏＴＴ
　　a:A
１．集合論：Ａは集合、aは要素
２．構成論：Ａは問題、aは解決
３．ＰＡＴ：Ａは命題、aは証明
４．HoTT　：Ａは空間、aは点

Univalent Axiom
　統価原理
　ライプニッツの原理
　
UniMath

---

ちなみに、私は「ドラゴンボール見るから」という理由で
ゼミをぶっちちたことがあります。