今回の数学エッセーでは, 前回の正則性公理のパラドックスに引き続き, 自然数のパラドックスを紹介します. 形式的体系として, ZFC を考えます.
ZFC の言語を L とし, L に現れない定記号 b を L に追加した言語を L_b とします. そこで, ZFC の公理シェーマを全て言語 L_b に関して考えることにより, ZFC を拡張した形式的体系を T_b とします. T_b に於ける具体的自然数の超数学的定義は, 前回と同様です.
N を ZFC に於ける有限順序数 (自然数) の全体とします.
x を ZFC の自由変数, 又は b とする時,
B(x) を論理式 x ∈ N とします.
次の公理シェーマ S_b を考えます: n が具体的自然数の時, 論理式 n ∈ b は公理である.
さて, ここで, 次の定理が成り立ちます:
定理: T_b に明示的公理 B(b) と公理シェーマ S_b を追加した形式的体系 T_b^* は, ZFC の保存拡大である.
証明: A を T_b^* から証明可能な ZFC の論理式とすると, T_b の公理 C_1(b), ・・・, C_m(b) と具体的自然数 n と LK の証明図 P を有限時間内に構成し, P の end sequent が, 次の形になるようにできる:
C_1(b), ・・・, C_m(b), B(b), φ∈b ∧・・・∧ n∈b → A
ここで, ZFC の自由変数 v で, P に現れないものを取り, P にあらわれる b を全て v で置き換えたものを P' とすると, P' は LK の証明図で, その end sequent は
C_1(v), ・・・, C_m(v), B(v), φ∈v ∧・・・∧ n∈v → A
の形である. よって, sequent
(∀v)C_1(v), ・・・, (∀v)C_m(v), B(v), φ∈v ∧・・・∧ n∈v → A
は LK-provable. よって, sequent
(∀v)C_1(v), ・・・, (∀v)C_m(v), (∃v)(B(v)∧φ∈v ∧・・・∧ n∈v) → A
は LK-provable. 然るに, 論理式 (∃v)(B(v)∧φ∈v ∧・・・∧ n∈v) は ZFC から証明可能だから,
ZFC の有限個の公理 D_1, ・・・, D_p が存在して, sequent
D_1, ・・・, D_p → (∃v)(B(v)∧φ∈v ∧・・・∧ n∈v)
は LK-provable となる. よって, cut より,
(∀v)C_1(v), ・・・, (∀v)C_m(v), D_1, ・・・, D_p → A
は LK-provable である. そこで, (∀v)C_1(v), ・・・, (∀v)C_m(v) がそれぞれ ZFC の定理であることに注意すると, A が ZFC から証明可能であることがわかる.
文責: Dr. Kazuyoshi Katogi
