【第25回 数学カフェ】公理的集合論入門一日目
朝5時起床。今日は金曜日。晴れ。
朝食後、散歩、筋トレ、朝刊を読むというルーチンワークをこなした。
で、今日は午後13時から、【第25回 数学カフェ】公理的集合論入門一日目に参加してきた。
講師は愛媛大学大学院理工学研究科特任講師、藤田博司先生です。
後日、二日目も含めて、改めてレポートするつもりですが、とりあえず一日目のダイジェストレポート。
公理的集合論の動きは、ラッセルのパラドックスから始まった。
公理的集合論を定義するために、まずは純粋集合（pure set）の定義から始める。
pure setとは文字（x,y,z）を見たら集合と思うことにし、
・空集合はpure set
・集合xの全ての要素がpure setならxもpure set
・pure setの要素もpure set、pure setの部分集合もpure set
・集合xの全ての要素がpure setならxもpure set
・pure setの要素もpure set、pure setの部分集合もpure set
と定め、公理論的集合論をpure setの世界の理論 + 血統書付き！を加えたものである。
ここでクワイン集合などの集合は除く必要があるため、公理論的集合論では言語をfixしなければならない。
つまり形式言語にしておく必要がある。
まずは記号を変数、述語記号、論理記号、量化記号と定め、４つの条項からなる構文を定める。
そして公理として以下を定義することにより、血統書付きの公理的集合論（ZFC）を展開できる。
①外延性
②分離公理
③対の公理
④和集合の公理（この時点で積集合、差集合も導ける。）
⑤冪集合の公理（この時点でクラフトスキーの順序対により直積集合が定義できる。よって関数も定義可。）
⑥無限集合の公理（この時点で自然数が定義できる。）
⑦置換公理図式（この時点でωより大きい集合が定義できる。）
⑧基礎の公理（この時点で無限に下がっていく集合が取れてしまうことを禁止できる。クワイン集合はここではじかれる。）
⑨選択公理
③対の公理
④和集合の公理（この時点で積集合、差集合も導ける。）
⑤冪集合の公理（この時点でクラフトスキーの順序対により直積集合が定義できる。よって関数も定義可。）
⑥無限集合の公理（この時点で自然数が定義できる。）
⑦置換公理図式（この時点でωより大きい集合が定義できる。）
⑧基礎の公理（この時点で無限に下がっていく集合が取れてしまうことを禁止できる。クワイン集合はここではじかれる。）
⑨選択公理
この後、ZFCを使用して独立性証明のための準備である証明不可能ということの定義を紹介。
ここで公理とターゲットの命題の否定を満たす「構造」（モデル？）をなんとかして作るのが独立性証明の方法論らしい。
藤田先生の説明は分かりやすく、記号・構文などに構文木を用いたりと、かなりコンパイラ（というより自動証明計算理論かな）の処理との共通項が多い。
藤田先生が論理式を書く時、まるで論理式をプログラミングしているのではないかと感じたのが印象的でした。
とりあえず一日目はここまで。明日が楽しみ。
22時までには寝る。
