Hilbertの第2問題
概要
Hilbertの第2問題（Hilbert's second problem）とは、Hilbert が 1900 年に挙げた問題の一つで、算術の公理、すなわち実数の公理系から有限回の論理的な推論で矛盾が導かれないことを直接に証明せよという問題である。Hilbert はこれを、形式化した証明を有限の方法で調べる計画へ発展させた。第 2 不完全性定理により、十分に強い無矛盾な理論の無矛盾性は、適当な条件のもとでその理論の中で形式化できる方法では証明できない。有限の方法は $\mathsf{PA}$ の中で形式化できると広く認められているので期待された形の証明は得られないと考えられているが、Gentzen は $\varepsilon_0$ までの超限帰納法で $\mathsf{PA}$ の無矛盾性を証明した。
前提知識: 無矛盾性, Peano算術, 実数, Gödelの不完全性定理
Hilbert の第 2 問題（Hilbert's second problem）は、Hilbert が 1900 年の講演「数学の問題」で挙げた 23 の問題の 2 番目で、算術の公理が矛盾しないこと、すなわち公理から出発して有限回の論理的な推論をいくら重ねても矛盾した結論に至らないことを証明せよ、という問題である。ここで「算術の公理」とは自然数の公理ではなく、計算の規則に連続性の公理を加えた実数の公理系を指す（Hil02 pp. 447–448）。
幾何学の公理の無矛盾性は、数の体の中にモデルを作ることで算術の無矛盾性に帰着できる。しかし算術そのものには、頼れる先がもうない。Hilbert はそこで、別の理論に帰着しない直接の証明を求めた。1920 年代に Hilbert はこの問いを、形式化した証明を有限の記号列として調べ、有限の方法だけで矛盾が出ないことを示す計画（Hilbert のプログラム）へ発展させた（Rat06 pp. 45–46）。
Gödel が 1931 年に示した第 2 不完全性定理（Gödelの不完全性定理）により、十分に強い無矛盾な理論は、適当な条件のもとで、その中で形式化できる方法では自分の無矛盾性を証明できない。有限の方法は $\mathsf{PA}$ の中で形式化できると広く認められているので、Hilbert が期待した形の証明は得られないと考えられている（Zac23 §4）。一方で Gentzen は 1936 年に、方法を $\varepsilon_0$ までの超限帰納法に広げて $\mathsf{PA}$ の無矛盾性を証明し、ここから理論の強さを順序数で測る研究が始まった（Rat06 pp. 46–47）。
この記事では問題の内容と現在の位置づけを述べ、次の 3 つを証明する。Hilbert の完全性公理が実数を特徴づけること、無矛盾性から計算で確かめられる全称文の正しさが従うこと、量化記号のない弱い算術の無矛盾性が直接の計算で示せることである。第 2 不完全性定理と Gentzen の証明はそれぞれの記事に譲り、ここでは証明しない。
| 結果 | 内容 |
|---|---|
| thm-h2-completeness | Archimedes 的な順序体のうち拡大できないものは実数体 |
| thm-h2-real | $\mathsf Q$ を含む無矛盾な理論は、計算で確かめられる性質についての全称文を誤らない |
| thm-h2-open | 開いた算術の無矛盾性 |
| cor-h2-sub | 第 2 不完全性定理の帰結：部分理論では無矛盾性を証明できない |
問題の内容
Hilbert は、ある科学の基礎を調べるには基本概念の間の関係を記述する公理系を立て、公理は同時に基本概念の定義になる、と述べた。そして公理についての問いのうち最も重要なものとして、公理が矛盾しないこと、すなわち公理に基づく有限回の論理的な推論が矛盾した結果に至らないことの証明を挙げた（Hil02 p. 447）。続く内容は次のとおりである（同 pp. 447–449）。
- 幾何学では、適当な数の体を作って公理の関係を数の関係に対応させれば、幾何学の無矛盾性は算術の無矛盾性に帰着する。
- 算術の公理の無矛盾性には直接の方法が必要である。算術の公理は計算の規則に連続性の公理を加えたものにほかならず、Hilbert は連続性の公理を Archimedes の公理と、数の系はこれ以上拡張できないという新しい公理（完全性公理）に置き換えていた。
- 無理数の理論の既知の推論を注意深く調べて修正すれば、直接の証明が見つかるはずだと Hilbert は確信を述べた。
- 概念に矛盾する属性を与えれば、その概念は数学的に存在しない。属性が有限回の推論で矛盾に至らないことが証明されれば、その概念の数学的な存在が証明されたことになる。実数の公理の無矛盾性の証明は、実数の全体の系すなわち連続体の数学的な存在の証明でもある。
4 の「無矛盾なら存在する」という見方は、一階の理論については Gödelの完全性定理 によって定理になった。無矛盾な一階の理論はモデルをもつ（無矛盾性 の定理「無矛盾性とモデルの存在」）。ただし Hilbert の完全性公理は「すべての拡大」について語る公理で、一階の公理ではない。
Hilbert が考えていた実数の公理系の範囲がはっきりしたのは、1920 年代に論理を本格的に扱うようになってからである（Rat06 p. 45）。数学の大きな部分は二階算術の中で形式化できるので（Hilbert–Bernays、同 p. 56）、問題の対象は後に $\mathsf{PA}$ や二階算術のような形式的な理論の無矛盾性として読まれるようになった。
完全性公理と実数
Hilbert の算術の公理を現代の言葉で述べ、それが実数体をちょうど定めることを確かめる。順序体 $F$ が Archimedes 的であるとは、どの $x\in F$ にも $x< n$ となる自然数 $n$ があることをいう。順序体 $E$ が $F$ を部分体として含み、$E$ の順序が $F$ の順序を延長しているとき、$E$ を $F$ の順序体の拡大という。
Archimedes 的な順序体 $F$ が完全性公理を満たすとは、Archimedes 的な順序体の拡大 $E\supset F$ で $E\ne F$ となるものが存在しないことをいう。
Archimedes 的な順序体 $F$ から $\mathbb R$ への、順序を保つ体の準同型 $\psi$ が存在する。$\psi$ は単射で、$F$ に含まれる $\mathbb Q$ の上で恒等写像である。
$x\in F$ に $\psi(x):=\sup\{q\in\mathbb Q\mid q< x\}$ を対応させる。Archimedes 性から、$F$ の中で $\mathbb Q$ は稠密である。これにより $\psi$ が順序を保つ体の準同型であることが確かめられる。
詳しい証明を開く
$F$ の中の $\mathbb Q$ は $1$ から作る（自然数を $1$ の和とすることは 実数 の節「Archimedes性」と同じである）。集合 $\{q\in\mathbb Q\mid q< x\}$ は Archimedes 性により空でなく上に有界なので、$\psi(x)\in\mathbb R$ が定まる。$F$ の $x< y$ について、Archimedes 性から $1/N< y-x$ となる $N$ をとると、$Nx< m\le Nx+1< Ny$ となる整数 $m$ があるので $x< m/N< y$ である（実数 の定理「有理数の稠密性」と同じ議論）。よって有理数は $F$ で稠密であり、$x< y$ なら $\psi(x)< \psi(y)$（間に有理数を 2 つとる）で、$\psi$ は単射である。$q\in\mathbb Q$ なら $\psi(q)=q$ である。
和：有理数 $q< x$、$r< y$ について $q+r< x+y$ なので $\psi(x)+\psi(y)\le\psi(x+y)$ である。有理数 $s< x+y$ については $s-y< x$ で、稠密性から $s-y< q< x$ となる有理数 $q$ をとると $s-q< y$ なので、$s\le\psi(x)+\psi(y)$ である。よって等号が成り立つ。
積：$x,y>0$ なら、正の有理数 $q< x$、$r< y$ について $qr< xy$ で、有理数 $s$ が $0< s< xy$ なら $s/y< q< x$ となる有理数 $q>0$ をとると $s/q< y$ である。上と同様に $\psi(xy)=\psi(x)\psi(y)$ を得る。一般の符号は $\psi(-x)=-\psi(x)$ に帰着する。$\square$
Archimedes 的な順序体 $F$ について、次は同値である。
- $F$ は完全性公理を満たす。
- $F$ は上限性質をもつ。すなわち $F$ は実数体である。
とくに、完全性公理を満たす順序体は 実数 体 $\mathbb R$ と順序体として同型である。
2 ⇒ 1：実数 の定理「実数体の一意性」により $F=\mathbb R$ としてよい。$E\supset\mathbb R$ を Archimedes 的な順序体の拡大とし、$\psi\colon E\to\mathbb R$ を lem-h2-embed の写像とする。$r\in\mathbb R$ について、$r$ より小さい有理数と $\psi(r)$ より小さい有理数は一致するので（$\psi$ は順序を保ち $\mathbb Q$ を動かさない）、$\psi(r)=r$ である。$x\in E$ について $r:=\psi(x)$ とおくと $\psi(x)=\psi(r)$ で、$\psi$ は単射だから $x=r\in\mathbb R$ である。よって $E=\mathbb R$ である。
1 ⇒ 2：$\psi\colon F\to\mathbb R$ を lem-h2-embed の写像とする。$\psi$ が全射でないとすると、$\mathbb R$ は $\psi(F)$ の真の拡大である。$\mathbb R\setminus\psi(F)$ を $F$ に付け加えて $\psi(F)$ の元を $F$ の元と同一視した集合に、$\mathbb R$ の演算と順序を移すと、$F$ の真の Archimedes 的な順序体の拡大が得られ、1 に反する。よって $\psi$ は順序体の同型で、$F$ は上限性質をもつ。$\square$
実数体の存在は集合論の中で切断や Cauchy 列から示せるので（実数 の節「構成と完備性」）、Hilbert の公理系は集合論の中にモデルをもつ。しかしこれは無矛盾性を集合論の無矛盾性に帰着しているだけで、Hilbert の求めた直接の証明ではない。
完全性公理を一階の公理に弱めると事情は変わる。実閉体 の一階の理論は量化記号消去をもつ（Tarski–Seidenbergの定理）。したがって $(\mathbb R,0,1,+,\cdot,<)$ の中で一階の論理式で定義できる $\mathbb R$ の部分集合は、$\mathbb R$ の中で多項式の有限個の符号条件で書ける集合であり、有限個の点と区間の和である。$\mathbb N$ はこの形でない。よってこの構造では自然数を定義できず、第 2 不完全性定理の障害はこの理論にそのままの形では及ばない。Hilbert の問いの難しさは、実数の演算よりも、実数の部分集合全体についての公理（完全性公理や連続性の公理）にある。
相対的な無矛盾性と直接の証明
理論 $T$ が無矛盾であるとは、$T\vdash A$ と $T\vdash\lnot A$ が同時に成り立つ文 $A$ が存在しないことをいう（無矛盾性）。モデルをもつ理論は無矛盾である（同記事の定理「モデルをもてば無矛盾」）。幾何学の公理（Hilbertの公理系）は実数の座標平面の中で解釈できるので、幾何学に矛盾があればそれは実数の算術の矛盾になる（Zac23 §1.1）。これが rem-h2-statement の 1 の相対無矛盾性である。
$\mathsf{PA}$ の公理はすべて $(\mathbb N,0,S,+,\cdot)$ で真なので $\mathsf{PA}$ は無矛盾である（無矛盾性 の例「Peano 算術」）。この議論は無限集合 $\mathbb N$ の全体と、量化記号を含む文の真理の概念を使う。形式的な証明の体系 $\mathsf{PA}$ が疑わしいと考える立場からは、$\mathsf{PA}$ より強い前提に頼っていることになる。
これに対して Hilbert のプログラムは、次のように考える。数学の証明を形式的な体系の中の記号列にすれば、証明そのものは有限の組合せ的な対象である。そこで、記号列を操作する有限の方法だけを使って、$0=1$ に至る記号列が存在しないことを示せばよい（Zac23 §1.3）。
有限の方法の範囲は Hilbert 自身の言葉では厳密に定められておらず、後の分析では Tait が原始再帰算術と同一視している（Rat06 p. 47）。Hilbert のプログラムは、「実在的」な命題が「理想的」な手段で証明できるなら有限の手段でも証明できることを示す還元の計画でもあった（同 p. 46）。無矛盾性がなぜこの還元を与えるのかを示すのが次の節である。
無矛盾性が保証すること
Gödelの不完全性定理 の記事の記号を使う。$L_A=\{0,S,+,\cdot,<\}$ を算術の言語、$\mathsf Q$ を Robinson算術、$\underline n$ を自然数 $n$ の数項とする。理論 $T$ が $\mathsf Q$ の公理をすべて導出するとき、$T$ は $\mathsf Q$ を含むという。論理式 $\rho(x)$ が関係 $R\subset\mathbb N$ を $\mathsf Q$ で表現するとは、$R(n)$ なら $\mathsf Q\vdash\rho(\underline n)$、$R(n)$ でないなら $\mathsf Q\vdash\lnot\rho(\underline n)$ となることをいう。計算可能な関係はすべて $\mathsf Q$ で表現できる（同記事の注意「この記事では証明しない事実」の 1。ここでは証明しない）。
$T$ を $\mathsf Q$ を含む無矛盾な $L_A$ の理論とし、$\rho(x)$ を関係 $R\subset\mathbb N$ を $\mathsf Q$ で表現する論理式とする。$T\vdash\forall x\,\rho(x)$ なら、すべての $n\in\mathbb N$ で $R(n)$ が成り立つ。
ある $n$ で $R(n)$ が成り立たないとする。表現の定義により $\mathsf Q\vdash\lnot\rho(\underline n)$ であり、$T$ は $\mathsf Q$ を含むので $T\vdash\lnot\rho(\underline n)$ である。一方 $T\vdash\forall x\,\rho(x)$ から $T\vdash\rho(\underline n)$ である。これは $T$ の無矛盾性に反する。$\square$
$T$ が $\mathfrak N=(\mathbb N,0,S,+,\cdot,<)$ で真であることも、$T$ の公理が決定可能であることも仮定していない。言語の違う理論でも、$L_A$ の式を翻訳して $\mathsf Q$ の公理の翻訳を導出できるなら、翻訳した式について同じ議論が通る。したがって無限の集合についての強い公理をもつ集合論でも、無矛盾でさえあれば結論が成り立つ。
$R(n)$ を「$2n+4$ は 2 つの素数の和である」とする。$R$ は計算可能なので、$\mathsf Q$ で表現する論理式 $\rho$ がある。Goldbach 予想 $\forall x\,\rho(x)$ が $\mathsf Q$ を含む無矛盾な理論 $T$ で証明されたとすると、thm-h2-real により予想は実際に正しい。$T$ が実解析や集合論の強い手段を使っていてもよい。この意味で、計算で確かめられる性質についての全称文にとって、無矛盾性は正しさの保証になる。Goldbach の予想のほか、多くの有名な問題が算術の言語の文として形式化できる（Rat06 p. 46）。
thm-h2-real は各 $n$ についての外からの主張である。Hilbert のプログラムが目指したのは、これを有限の推論の理論の中の主張にすることだった。ある有限の推論の理論が $T$ の無矛盾性を証明できれば、$T$ で証明された実在的な命題はその理論自身で証明できることになる（Zac23 §5）。Hilbert の無矛盾性の証明はこの意味で、理想的な数学を実在的な数学へ還元する手段だった。
直接の証明が届く例：開いた算術
Hilbert の学派では、von Neumann が帰納法の公理を含まない $\varepsilon$ 計算の体系の無矛盾性を 1925 年に証明した（1927 年刊。Zac23 §1.3）。ここでは直接の無矛盾性の証明がどのようなものかを、もっと簡単な、量化記号のない算術で見る。次の体系はこの記事で説明のために置くものである。
項を、変数と $0$ から $S,+,\cdot$ で作る。開いた論理式を、$s=t$ の形の式から $\lnot,\to$ で作る（量化記号を含まない）。次の公理と規則で開いた論理式を導出する体系を、この記事では開いた算術 $\mathsf{Op}$ とよぶ。ここで $A[x:=t]$ は変数 $x$ に項 $t$ を代入した式である。
- 公理 (P)：命題論理の恒真式の、原子式に開いた論理式を代入した形の式。
- 公理 (E)：$t=t$ と $s=t\to(A[x:=s]\to A[x:=t])$。
- 公理 (Q)：$Sx=Sy\to x=y$、$\lnot(0=Sx)$、$x+0=x$、$x+Sy=S(x+y)$、$x\cdot0=0$、$x\cdot Sy=x\cdot y+x$。
- 三段論法：$A$ と $A\to B$ から $B$。
- 代入：$A$ から $A[x:=t]$。
- 帰納法：$A[x:=0]$ と $A\to A[x:=Sx]$ から $A$。
変数を含まない項（閉項）の値 $\operatorname{val}(t)\in\mathbb N$ は、$S,+,\cdot$ を計算すれば有限の手順で求まる。変数を含まない開いた論理式の真偽も、$s=t$ を値の比較で判定して $\lnot,\to$ の真理値表で決まる。開いた論理式 $A$ の変数すべてに数項を代入した式を $A$ の数値例という。
$\mathsf{Op}$ で導出される式の数値例はすべて真である。とくに $0=S0$ は導出できず、どの式 $A$ についても $A$ と $\lnot A$ の両方が導出されることはない。
導出の長さについての帰納法で示す。公理の数値例は値の計算で真と分かる。三段論法と代入は数値例の取り替えで済み、帰納法の規則は、数値例を $0$ から $m$ まで順に $m$ 回たどれば処理できる。
詳しい証明を開く
まず補題：閉項 $s$ の値が $n$ なら、$A[x:=s]$ の真偽は $A[x:=\underline n]$ の真偽と一致する。真偽は閉項の値だけで決まるからである。
公理 (P)：数値例の原子式に真偽を入れると恒真式の値は真である。公理 (E)：$\operatorname{val}$ は項に値を与えるので $t=t$ は真である。$s=t\to(\cdots)$ の数値例では、$s,t$ の値が異なれば前件が偽で全体は真、等しければ補題から $A[x:=s]$ と $A[x:=t]$ の真偽は一致する。公理 (Q)：$\operatorname{val}$ の定義と $\mathbb N$ の計算そのものである。
三段論法：$B$ の数値例を与える代入 $\sigma$ を、$A$ にしか現れない変数へ $\underline0$ を割り当てて延長する。帰納法の仮定により $\sigma(A)$ と $\sigma(A\to B)$ が真なので $\sigma(B)$ は真である。代入：$A[x:=t]$ の数値例 $\sigma(A[x:=t])$ は、補題により、$x$ に $\operatorname{val}(\sigma t)$ の数項を割り当てた $A$ の数値例と同じ真偽をもつ。
帰納法の規則：$A$ の数値例を $\sigma$ とする。$x$ が $A$ に現れないなら $A$ は前提 $A[x:=0]$ と同じ式である。現れるとき $\sigma(x)=\underline m$ とする。$k\le m$ について、$\sigma$ の $x$ の値を $\underline k$ に替えた代入を $\sigma_k$ とする。$\sigma_0(A)$ は $A[x:=0]$ の数値例なので真である。$\sigma_k(A)\to\sigma_k(A[x:=Sx])$ は帰納法の仮定により真で、補題により $\sigma_k(A[x:=Sx])$ は $\sigma_{k+1}(A)$ と同じ真偽をもつ。これを $m$ 回たどると $\sigma_m(A)=\sigma(A)$ は真である。
結論：$0=S0$ は偽なので導出できない。$A$ と $\lnot A$ がともに導出されると、数値例の 1 つで同じ閉じた式とその否定がともに真になり、矛盾する。$\square$
証明が使うのは導出の長さについての帰納法と、閉項の有限の計算だけである。式の真偽は有限の手順で決まるので、$\mathbb N$ の全体についての真理の概念はいらない。
量化記号が入るとこの方法は止まる。$\forall x\,A$ の真偽は有限の計算で決まらず、帰納法の公理は「すべての数値例で真」を別の式の前提に使う形になる。$\mathsf{PA}$ についてこの困難が本質的であることが次の節の内容である。
第 2 不完全性定理の影響
$T$ を決定可能な公理系とし、$\mathrm{Con}_T$ を $T$ の無矛盾性を表す文とする（定義は Gödelの不完全性定理 の節「第2不完全性定理」）。同記事の定理「第2不完全性定理」は、$T$ が $\mathsf Q$ を含み無矛盾で、証明可能性の論理式が導出可能性条件 (D2)・(D3) を満たせば $T\not\vdash\mathrm{Con}_T$ であることを述べる。$\mathsf{PA}$ や集合論の標準的な論理式がこの条件を満たすことは、同記事の注意で述べられているとおりである（この記事では証明しない）。
$T$ を上の条件を満たす理論とする。$F$ を、定理がすべて $T$ の定理になる $L_A$ の理論とする。このとき $F\not\vdash\mathrm{Con}_T$ である。
$F\vdash\mathrm{Con}_T$ なら $T\vdash\mathrm{Con}_T$ となり、第 2 不完全性定理に反する。$\square$
$T=\mathsf{PA}$ とする。有限の方法で行われる推論が $\mathsf{PA}$ の中で形式化できるなら、cor-h2-sub により $\mathsf{PA}$ の無矛盾性の有限の証明はない。実数の公理を形式化した理論（たとえば二階算術）は $\mathsf{PA}$ の強さを含むので、同じ障害に当たる。
「有限の方法は形式化できる」は定理ではなく、有限の方法の範囲についての判断である。Gödel は 1931 年の論文で、形式化できない有限の方法の可能性を残していた。しかし 1934 年ごろ以降、Gödel の結果の前に有限的と認められていた方法はすべて $\mathsf{PA}$ の中で形式化できることが、ほぼ一般に受け入れられている（Zac23 §4）。
この結論の読み方には議論がある（Zac23 §4）。Smoryński は第 1 不完全性定理の段階で Hilbert の保存性の要求が崩れると論じ、Detlefsen は実在的な部分に誤りを生まないことだけを求める読み方でこれに反論した。また $\mathrm{Con}_T$ の書き方によっては $T$ の中で証明できる文も作れる（Gödelの不完全性定理 の節「反例：条件を外すと成り立たない」）が、そのような文は導出可能性条件を満たさない証明可能性の述語による。
問題のその後：Gentzen の証明と順序数解析
無矛盾性の証明の手段を有限の方法より広げれば、第 2 不完全性定理と矛盾せずに証明ができる。Gentzen は有限の方法に $\varepsilon_0$ までの超限帰納法を加えて $\mathsf{PA}$ の無矛盾性を証明した。これは、$\mathsf F$ を有限的に正当化される推論を体現する理論、$\text{EC-TI}(\varepsilon_0)$ を初等的に計算可能な述語についての $\varepsilon_0$ までの超限帰納法として、$\mathsf F+\text{EC-TI}(\varepsilon_0)\vdash\mathrm{Con}(\mathsf{PA})$ の形に述べられる（Rat06 式 (1)、p. 47）。無限の導出を使う形の証明と、$\varepsilon_0$ が改良できないことは Gentzenの無矛盾性証明 で証明する。
Gentzen 以後の研究は、理論ごとに無矛盾性の証明に必要な順序数を決める順序数解析へ進み、2006 年の概説は二階算術の強い部分体系までの進展を述べている（Rat06 p. 46）。別の方向では、逆数学 が通常の数学の定理に必要な公理の強さを調べ、たとえば Hahn–Banach の定理が証明できる $\mathsf{WKL}_0$ は原始再帰算術に対して $\Pi^0_2$ 文で保存的である（Zac23 §5）。これらは Hilbert の計画を部分的に実現するものと見られている。
| 理論 | 無矛盾性の証明について | 所在 |
|---|---|---|
| 開いた算術 $\mathsf{Op}$ | 閉項の計算と導出の長さの帰納法 | thm-h2-open |
| $\mathsf{PA}$ | モデル $\mathbb N$ の存在 | ex-h2-model |
| $\mathsf{PA}$ | $\varepsilon_0$ までの超限帰納法 | Gentzenの無矛盾性証明 |
| $\mathsf{PA}$ | $\mathsf{PA}$ の中で形式化できる方法では証明できない | cor-h2-sub |
| 実数の一階の理論（実閉体） | 自然数を定義できず、第 2 不完全性定理の対象外 | rem-h2-rcf |
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| thm-h2-real の「$T$ は無矛盾」 | $L_A$ のすべての文の集合 | 結論の「すべての $n$ で $R(n)$」 |
| thm-h2-real の「$T$ は $\mathsf Q$ を含む」 | $T=\{\forall x\,(x=0)\}$、$\rho(x)$ は $x=0$ | 同じ |
| thm-h2-real の「$\rho$ は $R$ を $\mathsf Q$ で表現する」 | $T=\mathsf{PA}+\lnot\mathrm{Con}_{\mathsf{PA}}$、$\rho(x)$ は $\lnot\mathrm{Con}_{\mathsf{PA}}$、$R=\emptyset$ | 同じ |
| def-h2-completeness の拡大を Archimedes 的なものに限ること | $\mathbb R\subset\mathbb R(t)$ | thm-h2-completeness の 2 ⇒ 1 |
どの行でも、外した条件以外の仮定は満たされ、結論だけが崩れる。
確かめを開く
1 行目：すべての文の集合は $\mathsf Q$ を含み、$\forall x\,\rho(x)$ も導出する。$\rho$ を $x=0$ とすると $\rho$ は $R=\{0\}$ を $\mathsf Q$ で表現するが、$R(1)$ は成り立たない。
2 行目：1 元の構造がモデルなので $T$ は無矛盾である。$\rho$ は $R=\{0\}$ を表現し、$T\vdash\forall x\,\rho(x)$ だが $R(1)$ は成り立たない。$T$ は $\mathsf Q$ の公理 $\forall x\,\lnot(0=Sx)$ を導出しないので $\mathsf Q$ を含まない。
3 行目：$\mathsf{PA}$ が無矛盾なら、第 2 不完全性定理により $\mathsf{PA}\not\vdash\mathrm{Con}_{\mathsf{PA}}$ なので $T$ は無矛盾であり、$\mathsf Q$ を含む。$\rho(x)$ を $x$ を含まない文 $\lnot\mathrm{Con}_{\mathsf{PA}}$ とすると $T\vdash\forall x\,\rho(x)$ である。$R=\emptyset$ は計算可能な関係で、$R(0)$ は成り立たないので結論が崩れる。$\rho$ は $R$ を表現していない。表現しているなら $\mathsf Q\vdash\lnot\rho(\underline0)$、すなわち $\mathsf Q\vdash\lnot\lnot\mathrm{Con}_{\mathsf{PA}}$ となって $\mathsf{PA}\vdash\mathrm{Con}_{\mathsf{PA}}$ に反するからである。
4 行目：$\mathbb R(t)$ に $t$ をすべての実数より大きくする順序を入れると（実数 の例「非Archimedes順序体」）、$\mathbb R$ の真の順序体の拡大である。拡大の制限を外すと、どの順序体 $F$ も $F(t)$ に同じように拡大できるので、条件「拡大できない」を満たす順序体は存在しない。Archimedes の公理は、完全性公理を意味のあるものにするために必要である。
関連項目
- 前提: 無矛盾性, Peano算術, 実数, Gödelの不完全性定理
- 比較: Hilbertの第5問題, Hilbertの第10問題, Hilbertの第12問題
- 道具: Robinson算術, Hilbertの公理系, 実閉体
- 発展: Gentzenの無矛盾性証明, 証明論, 逆数学
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
