やっと, できました.
数理論理学入門のテキストです.
(12/1, 17:00 頃, ケアレスミスを修正しました.)
(12/7. 保存拡大に関する, 追加の記述を多少付け足しました.)
このテキストでは, 数学の基礎付けとしての等号述語論理を定式化し,
定義による関数記号の導入が, いかなる場合に, 元の形式的体系の
保存拡大になっているかを論じています.
このことにより, N. Borubaki が, 数学原論の集合論の部門を整備する際に,
なぜ, 超限論的選択関数を導入したのか, その理由に迫ります.
そもそも, 定義による関数記号の導入とは, 等号を持つ理論 T,
T の変数 x_1, ・・・, x_n, y , T の formula A (x_1, ・・・, x_n, y )
に対し, T 内で論理式
(∀x_1) ・・・ (∀ x_n) (∃! y) A (x_1, ・・・, x_n, y )
が証明可能な時, T の言語 L に現れない n 変数の関数記号 f を L に付け足した言語を
L' とし, T' として, 言語が L', 明示的公理が T の明示的公理の全体と次の形の
明示的公理を持つものを考えたものです:
(∀x_1) ・・・ (∀ x_n) (∀ y)(y = f (x_1, ・・・, x_n) ⇄ A (x_1, ・・・, x_n, y ))
このとき, T' の公理シェーマに, どういう条件を付け足せば, T' が T の保存拡大になっているか?
この問題を定式化して, 答えの一つを与えたのが, 上記のテキストです.
しかし, 一般に, working mathematichians にとって, 上記のテキストで論じられているような, 定義による関数記号の拡大の一般論を勉強するのは, 非常に煩わしい限りです.
そこで, N. Borubaki の数学原論の数理論理学の部分では, この煩わしさを回避するため,
超限論的選択関数を導入し, 等号を持った理論の研究では, 初めから, 同一の理論 T
についてのみの研究で済むような定式化を成功させています.
これは, N. Borubaki が数学原論の数理論理学の部分を整備する際に, working mathematicians にとって, 数学の基礎としての数理論理学の知識に, 速やかに到達できるような配慮をしたのではないかと, 私は考えています.
文責: Dr. Kazuyoshi Katogi
