A(x) を x を変数とする論理式とする時,
τ_x(A(x)) の形で, A(x) を満たす x が存在する時は,
そのような xのうちの一つ, A(x) を満たす x が存在しない時は,
ある一つの対象を表します.
ブルバキは, なぜ, こんな τ なる記号を導入したのか.
これは,
A(x_1, ... x_n, y) を形式的体系 T の論理式で,
∀x_1 ・・・ ∀x_n ∃_1 y A(x_1, ... x_n, y)
が T から証明可能な時, 我々はよく,
T に現れない関数記号 f を T に追加し, T の公理に 論理式
∀x_1 ・・・ ∀x_n A(x_1, ... x_n, f(x_1, ... x_n))
を追加することで, 新しい形式的体系 T' を作り,
T' が T の 保存拡大になっていることを確認し,
T' の中で議論をするということを行います.
しかし, 形式的体系のいかんによっては,
T' が T の保存拡大にならない場合もあり,
この『定義による関数記号の導入』の一般論を,
任意の形式的体系 T に関して定式化することは非常に煩雑です.
また, ブルバキの数学原論編纂の目的そのものが, この種の議論
・・・定義による関数記号の導入・・・
のような煩雑さをなるべく回避して,
working mathematician にとっての数学の理論的な基礎に
『厳密さを犠牲にせずに』
速やかにたどり着けるようにしたい, ということだったと推察されます.
そこで, 超限論的選択関数 τ を形式的体系の中に
最初から組み込んでおけば,
∀x_1 ・・・ ∀x_n ∃_1 y A(x_1, ... x_n, y)
が 形式的体系 T から証明可能であれば,
f(x, ..., x_n) を
τ_y (A(x_1, ... , x_n, y))
の省略記号だと約束しさえすれば,
T においては
∀x_1 ・・・ ∀x_n A(x_1, ... x_n, f(x_1, ... x_n))
がトリビアルナ形で定理にっている,
ということが保証されるのです.
つまり, 形式的体系 T の言語, 記号, 公理などを拡張していかなくても,
『定義による関数記号の導入』
という点では,
T の中で系統的に理論展開が可能になるのです.
これこそが, ブルバキが超限論的選択関数を
その数学原論の中において導入した,
大きな理由ではないかと, 私は考えております.
文責: Dr. Kazuyoshi Katogi
