数理科学と日本古代史のブログ

Hilbertのε定理に関する論文を張っておきます

Hilbert's "Verunglueckter Beweis," the first epsilon theorem, and consistency proofs

Michael Rathjenによる構成的集合論の論文：

Generalized Inductive Definitions in Constructive Set Theory

と、Laura Crossilla による論文：

Constructive notions of set Part I Sets in Martin-Loef type theory

へのリンクを張っておきます。

　構成主義数学の形式化に関する論文の紹介です。

CZF and Second Order Arithmetic

　表題の CZF とは Constructive Zermelo Fraenkel で、標準数学のデファクト・スタンダードとなっている公理的集合論 ZF の構成主義バージョンの一つです。
　外延性公理は備えているものの、冪集合の公理を持たないので、ある意味不便です。この集合論が Bishop の構成主義数学の精神に適っているかは微妙ですが、いろいろな整合性が成り立つ、研究対象としては面白い体系のようです。

地球の大陸移動の過去と未来に関するサイトの紹介です。
未来については大きく分けて２説あるようで、大西洋がこのまま拡大して太平洋が無くなるとする説と、大西洋が再び閉じるという説です。このサイトは後者の説に立っています。

PALEOMAP Project

　だいぶ間が空いてしまいましたが（というかほとんどサボっているだけですが）、どうもキチンと内容が完結してから書き込もうとするから面倒くさくなって書き込めなくなるのだと気付きまして、これからは、単なる思い付きを書くことにします。今まで以上に読んでる人には意味がわからなくなるでしょうが、ご勘弁を。

　さて、今回は、数学の基礎付けにおける「形式化の原理」と私がよんでいる原理を、数学の基礎付けの一番最初の部分である論理式の sequent からなる証明文の推論規則を“導出”する際に適用する場合の、すでに書いたことがある内容に関する、ちょっとした“気付き”の話です。

　熱力学の基本原理は「熱力学の第１法則」と「熱力学の第２法則」です。私は、この大きな枠組みについて異を唱えるものではありません。

　毎回覗いてくれていた方、どうもおまたせしました。久しぶりに新しい連載ネタが見つかったので再開します。

　今回はちょっと表題について面白い話題を一つ。
　Banach-Tarskiの背理というのは、いろいろな言い方がありますが、「豆粒大の球を有限個の部分に分割して組み合わせなおすと、あーら不思議！太陽の大きさの球ができる」という定理なのですが、一見、体積を考えるとそんなことはあり得ないように見えることからパラドクス（背理）と呼ばれています。
　しかしもちろん、これはパラドクスでも何でもなく、れっきとした定理で、有限個に分割された各パーツはそもそも「体積が定義できない」ので、パラドクスではないのです。
　ただし、このBansch-Tarskiの定理の証明には選択公理が用いられており（証明はたとえばこちらやこちらを参照のこと）、しかも非可算無限個の対象に対する選択公理を用いていることから、「選択公理を用いると不自然な定理が証明される」という代表例によく引っ張り出されます。

　ところが、最近、Banach-Tarskiにある意味大変“近い”結果が、選択公理なしに証明できたというのです！

　だいぶ間が開いてしまいましたが、直前の書き込み以降、その定義において一箇所だけ修正しようと思った箇所があります。
　再帰的集合論については、私のWebサイト「数学の基礎」の第５節で解説していますが、そこでは既に修正を反映しています。
　それは、和集合の公理をやめて、それより強い推移性公理を置く、というものです。

　今までに、“形式化の原理”、すなわち特定の記号列、あるいは記号列に関する特定の状態に名前を付け、それが持つ構文論的な性質を列挙し、しかる後にその名前を付けたモノを理論内部の記号として改めて追加すると共に、それが持っていた構文論的な性質を推論規則あるいは公理の形に翻訳する、という方法で理論拡大していく手法を具体的に説明してきました。
　独断的な名前ですが、こうして得られた理論を「根拠のある理論」と呼ぶことにしましょう（もちろん、これは“根拠がある”という概念に対する考え方の一つに過ぎず、それ以外の考え方は誤りだ！などと主張するものではありませんので念のため）。
　このとき、今までの議論により、以下の結果が得られたことになります。

　前々回の「可算選択公理の根拠(2-35)」の解説を若干追加し、誤りを訂正しました。

　前回解説した再帰的集合論の公理を論理式で表現してみましょう。

　さて、高階の集合論において、T がある n≧1 に対する τ_n項であることを set(T) と書いて T は集合であると言い、τ項と集合を総称して τ'項とよび、ある n と m＞n に対して τ_n(a) かつ τ_m(b) かつ a∈_mb が成り立つことを a∈b と略記することにします。
　また、X∈A が成り立つとき、X は A の元である、X は A に属すといい、A に属す τ'項 は必ず B に属すとき A⊂B と書いて A は B に包含されると言い、A⊂B と B⊂A が共に成り立つとき A〜B と書いて A と B は元が共通であると言うことにします。
　ただしここで出てきた set や τ' や ∈ や ⊂ や 〜 は、理論内部の記号ではなく、メタ記号です。このとき次の性質が成り立ちます。

　前回は、与えられた理論 τ 上の高階の集合論 τ**^…* を用いると、初等的な数学はほとんど展開できることを説明しました。
　実用上はこれで十分かもしれませんが、いちいち途中で理論を拡大しながら議論するというのはかなり煩わしいことです。
　そこで、このような理論拡大が固定した理論の中で自由に行えるようにできたら便利です。

　一般に、２つの存在述語記号 σ , τ に対し、

(1) (σ∨τ)(T) ≡ σ(T) ∨ τ(T)

と定義すると、σ∨τ は１変項述語記号のように扱えるので、(σ∨τ)理論というものを考えることができます。これを理論 σ と理論 τ の和理論とよぶことにします。