この pdf(公理的集合論研究書) で, atom からなる集合を持つ BGE (別名 NBG) が atom からなる集合を持つ ZFC の保存拡大であることの有限の立場での証明 (より精密には, recursive な証明) を与えています.
ただし, この pdf の中では, atom を個体と呼んでいます.
ここで, 『recursive な証明』とは, 下記の意味となります: BGE から証明可能な ZFC の任意の論理式 A と BGE に於ける任意の証明図 Γ = A_1, ・・・, A_n で A_n が A に等しくなるようなものに対し, ZFC に於ける証明図 Γ' = B_1, ・・・, B_m で B_m が A に等しくなるようなものを対応させることができる. この対応付け: Γ → Γ' は次の意味で recursive である: Γ のゲーデル数 p = G(Γ) に Γ' のゲーデル数 q = G(Γ') を対応させる関数 f : n → m = f(n) は recursive である.
上記の pdf では, Γ を Γ' に計算可能な形で変形できるということのみを証明し, 上記 recursive function f を explicit に与えてはいないが, 読者は上記 pdf に於ける証明を丁寧に検証すれば, 上記 f が recursive となることを容易に確認できるであろう.
ここ 1ヶ月くらい, この保存拡大の超数学的定理の執筆を行なっていました. 僕がこの証明を与えたのは, もう 15年くらい前ですが, 当時は大学院での僕の専門とは外れる分野で, 趣味としてやっていた勉強でした. 従って, LaTeX での清書を行っていなかったのです.
しかし, 最近, この保存拡大の超数学的定理に関する文献が通常の方法ではなかなか手に入らないことを知り, この結果に興味を持たれるであろう数学愛好者のために, この pdf を執筆したものです.
証明には, 内部モデルの方法, 強制法 (ジェネリック拡大), シークエント計算や証明図の分析を使います.
2023/10/8 追記: 最後から 2 ページ目のところのミスプリを修正しました. が, 保存拡大の本論には影響しない部分です.
2023/10/11 追記. モストウスキーの同型 \varphi : M_0 \to M_1 について, 誤植を訂正しました.
x ∈ M_0 かつ cl x の時, \varphi (x) = { \varphi (y) | y ∈ x} ではなく, \varphi (x) = { \varphi (y) | y ∈ x \cap M_0} となります.
2023/10/17 追記: 形式的体系についての準備のセクションの一番最初で, A が記号列で x が対象変数, X が類変数で, x, X が A に現れない時, (∃x)A と (∃X)A が図形として区別できなくなっていた問題を解消しました. (∀x)A, (∀X)A についても同様です.
文責: Dr. Kazuyoshi Katogi
