kazz の数学旅行記

数学の話題を中心に, 日々の知的活動の旅路を紹介します.

数理論理学入門〜定義による関数記号の導入の問題〜

やっと, できました.

 

数理論理学入門

 

数理論理学入門のテキストです.

(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