逆数学のソースを表示

'''逆数学'''（ぎゃくすうがく）とは、[[数学]]の[[定理]]の[[証明 (数学)|証明]]に必要な[[公理]]を決定しようとする[[数理論理学]]のプログラムである。簡単に言えば、通常の数学が公理から定理を導くのとは逆に、「定理から公理を証明する」手法を用いることが特徴である。「[[選択公理]]と[[ツォルンの補題]]は[[ツェルメロ＝フレンケルの公理系|ZF]]上で同値である」、というような[[集合論]]の古典的定理は、逆数学プログラムの予兆となるものだった。しかし、実際の逆数学では主に、集合論の公理ではなく、通常の数学の定理を研究するのを目的とする。

逆数学は大抵の場合、[[2階算術]]について実行され、定理が[[構成的解析]]と[[証明論]]に動機付けられた[[2階算術]]の部分体系のうち、どれに対応するのかを研究する。
2階算術を使うことで、[[再帰理論]]からの多くの技術も利用できる。実際、逆数学の結果の多くは、[[計算可能解析学|計算可能性解析学]]の結果を反映している。

逆数学は、{{harvs|txt|authorlink=Harvey Friedman|first=Harvey|last= Friedman|year1=1975|year2=1976}}によってはじめて言及された。基本文献は{{harv|Simpson|2009}}を参照。

== 一般的な原理 ==
逆数学は、フレームとなる言語と基本的な公理からはじめる。例えば、“すべての[[実数]]の有界な列は[[上限 (数学)|上限]]をもつ”という定理の研究には、実数と実数の列を定義する公理が必要となる。

基本体系において証明できない定理からはじめて、定理を証明するのに必要な(基本体系よりも強い)公理を決定することを目標とする。定理<math>T \, </math>とそれを証明可能な場合の体系<math>S \, </math>との関係を示す2つの証明がある。1つ目は、<math>S \, </math>から<math>T \, </math>が証明可能であることの証明である。このとき普通の数学の定理は体系<math>S \, </math>で成り立つ。2つ目は*逆方向*、
すなわち<math>T \, </math>が<math>S \, </math>と同値であることであることの基本体系における証明である。
逆方向の証明ができれば、<math>S \, </math>より弱い体系<math>S^\prime \, </math>であって<math>T \, </math>を証明できるようなものは存在しないことが分かる。

=== 2階算術の使用 ===
逆数学は[[2階算術]]の部分体系において研究されることが多い。その場合、数学的対象を[[自然数]]と自然数の集合によって形式化しなければならない。例えば、自然数のペアを1つの自然数として表現することができ、自然数のペアによって有理数を表現する。有理数の集合（これは結局、自然数の集合として表現される）によって有理数の列を表現し、有理数の列のうちコーシー列であるようなものによって実数を表現することができる。逆数学の研究においては、弱い部分体系であって数学的対象を形式化できる程度には強い体系を基本体系として用いる。<!--
逆数学では公理系は'''内包公理'''と呼ばれる[[公理図式]]によって定義される。この図式は、複雑な論理式によって定義された任意の自然数に関する集合で与えられる。論理式の複雑さは[[算術的階層]]や[[解析的階層]]によって比較される。
-->

逆数学が集合論ではなく2階算術を用いるのは、弱い部分体系であって数学的対象を形式化できる程度には強い体系を2階算術では自然に定義することができるからである。<!--
2階算術において[[ポストの定理]]は、論理式の複雑さとそれが定義する集合の計算可能性の間に対応があることを意味している。
-->

2階算術を使う場合、数学の定理を制限しなければならない。例えば、2階算術では一般のベクトル空間は表現できない。そのため"すべてのベクトル空間は基底をもつ"という一般的な原理は表現できないが、"すべての可算なベクトル空間は基底をもつ"という原理は表現することができる。同様に、代数の定理の対象は可算な群や環や体についてのものになる。また、[[距離空間]]を対象とする解析や位相の定理は、実数を有理数のコーシー列によって表現したのと同様の手法により、可分な距離空間について考察することができる。<!--
"すべてのベクトル空間は基底をもつ"というような原理が成り立つには、[[選択公理]]を意味する多くの原理が2階算術の弱い部分体系で証明可能でなければならない。
-->
なお、定理を可算なものに制限した場合、本来の定理とその強さが全く異なる場合がある。例えば、"すべての体は代数的閉体をもつ"はZF集合論では証明できないが、"すべての可算な体は代数的閉体をもつ"と制限すれば、非常に弱い形式体系である<math>\mbox{RCA}_0 \, </math>でも証明することができる。

== 2階算術の5つの基本的部分体系(Big Five) ==
2階算術の部分体系 <math>\mbox{RCA}_0 \, </math>、<math>\mbox{WKL}_0 \, </math>、<math>\mbox{ACA}_0 \, </math>、<math>\mbox{ATR}_0 \, </math>、<math>\Pi^1_1\mbox{-CA}_0 \, </math>は, '''Big Five'''と呼ばれ、
逆数学において頻繁に扱われるものである。

次は"big five"の特徴である。{{harvtxt|Simpson|2009|loc=p.42}}参照。
{|class="wikitable"
!部分体系
!名称の由来
!証明論的順序数
!対応する哲学的原理
!備考
|-
|<math>\mbox{RCA}_0 \, </math>
|Recursive comprehension axiom(再帰的内包公理)
|<math>\omega^\omega \, </math>
|構成的数学 (Bishop)
|逆数学の基本体系
|-
|<math>\mbox{WKL}_0 \, </math>
|Weak König's lemma(弱ケーニッヒの補題)
|<math>\omega^\omega \, </math>
|有限還元 (Hilbert)
|[[原始再帰的算術|PRA]]上で<math>\Pi^0_2 \, </math>文を、<math>\mbox{RCA}_0 \, </math>上で<math>\Pi^1_1 \, </math>文を保存する。
|-
|<math>\mbox{ACA}_0 \, </math>
|Arithmetical comprehension axiom(算術的内包公理)
|[[Epsilon_zero|<math>\epsilon_0 \, </math>]]([[イプシロン数]])
|可述主義 (Weyl, Feferman)
|ペアノ算術上で算術的文を保存する。
|-
|<math>\mbox{ATR}_0 \, </math>
|Arithmetical transfinite recursion(算術的超限再帰)
|[[Feferman–Schütte ordinal|<math>\Gamma_0 \, </math>]]
|可述的還元主義 (Friedman, Simpson)
|フィッファーマン体系IR上で<math>\Pi^1_1 \, </math>文を保存する。
|-
|<math>\Pi^1_1\mbox{-CA}_0 \, </math>
|<math>\Pi^1_1 \, </math> comprehension axiom (<math>\Pi^1_1 \, </math>内包公理)
|[[Psi0(Omega omega)| <math>\Psi_0 \, </math>(<math>\Omega_\omega \, </math>)]]
|非可述主義
|
|}

なお, Big Fiveの名前についている <math>{}_0 \, </math>は帰納法の図式が制限されていることを意味する。例えば、<math>\mbox{ACA}_0 \, </math>は算術的論理式についての帰納法しか持たない。帰納法を制限した体系は、一般の2階算術の論理式についての帰納法をもつ体系に比べ、大幅に小さい証明論的順序数を持つ。

=== 再帰的内包公理 RCA<sub>0</sub> ===
<math>\mbox{RCA}_0 \, </math>は、「[[ロビンソン算術]]の公理」＋「<math>\Sigma^0_1 \, </math>論理式に対する帰納法の公理」＋「<math>\Delta^0_1 \, </math>論理式に対する内包公理」からなる部分体系である。

<math>\mbox{RCA}_0 \, </math>は逆数学で最も多用される体系である。<math>\mbox{RCA}_0 \, </math>は"再帰的内包公理"と呼ばれ、"再帰的"とは"計算可能"を意味している。この名称は<math>\mbox{RCA}_0 \, </math>が"計算可能性数学"に類似しているからである。<math>\mbox{RCA}_0 \, </math>で存在が証明可能な自然数の集合は計算可能である、よって計算不可能な集合の存在は<math>\mbox{RCA}_0 \, </math>で証明できない。

<math>\mbox{RCA}_0 \, </math>はBig Fiveで最弱だが、古典的数学の対象を形式化できる。また、以下の定理が証明可能である。
*自然数全体、整数全体、有理数全体の成す集合の基本性質(例えば、有理数全体が[[順序体]]を成すこと)。
*実数全体の成す集合の基本性質(実数全体が[[アルキメデスの性質|アルキメデス]]順序体であること、長さが0に近付く任意の[[包含閉区間列]]の交叉が1点のみからなること、実数は非可算であること)。
*[[完備距離空間|完備]][[可分空間|可分]][[距離空間]]における[[ベールの範疇定理]]。
*実連続関数における[[中間値の定理]]。
*可分バナッハ空間における連続[[線形演算子]]の列に関する[[バナッハ–シュタインハウスの定理]]。
*弱い[[ゲーデルの完全性定理]]。
*可算な体での[[代数的閉体]]の存在(一意性は除く)。
*可算な順序体の[[実閉体]]の存在と一意性。

<math>\mbox{RCA}_0 \, </math>の1階部分は、<math>\mbox{I}\Sigma_1 \, </math>（ペアノ算術の帰納法を<math>\Sigma_1 \, </math>論理式に制限した体系）と一致する。

=== 弱ケーニッヒの補題 WKL<sub>0</sub> ===
<math>\mbox{WKL}_0 \, </math>は、<math>\mbox{RCA}_0 \, </math>に弱ケーニッヒの補題（すべての無限二分木は無限路をもつ）を付け加えた体系である。

弱ケーニッヒの補題は[[選択公理]]に近く、実際<math>\text{RCA}_0 \, </math>において、<math>\Pi^1_1 \, </math>選択公理と<math>\text{WKL}_0 \, </math>が同値であることを示せる。また、<math>\Sigma^0_1 \, </math>分離原理とも同値になる。

<math>\mbox{WKL}_0 \, </math>は、<math>\mbox{RCA}_0 \, </math>よりも証明能力が高く、<math>\mbox{WKL}_0 \, </math>では非計算可能集合の存在を示せる。

<math>\mbox{RCA}_0 \, </math>と<math>\mbox{WKL}_0 \, </math>の1階部分は同じ、つまり算術的な定理については証明能力は同じである。しかし、<math>\mbox{WKL}_0 \, </math>で証明可能で、<math>\mbox{RCA}_0 \, </math>では証明不可能な古典的数学の定理もある。これらの結果は2階部分の証明能力の違いを示している。

<math>\mbox{RCA}_0 \, </math>上で、<math>\mbox{WKL}_0 \, </math>と以下の定理が同値であることが示せる。

*実数からなる単位閉区間に対する（開区間による任意の被覆が有限部分被覆を持つという意味での）[[ハイネ＝ボレルの定理]]。
*完備全有界可分距離空間に対する（開球体列による被覆についての）ハイネ＝ボレルの定理。
*単位閉区間（もしくは任意のコンパクト可分距離空間）上の連続実函数が有界であること（もしくは有界かつその境界値を実現する点が存在すること）。
*単位閉区間上の連続実函数が有理係数多項式で一様に近似できること。
*単位閉区間上の連続実函数が一様連続であること。
*単位閉区間上の連続実函数が[[リーマン積分]]可能であること。
*単位閉区間の有限個のコピーの直積上の連続函数に対する[[ブラウワーの不動点定理]]。
*可分バナッハ空間の部分空間上の有界線型形式が全体空間上の有界線型形式に拡張できるという形での可分[[ハーン＝バナッハの定理]]。
*[[ジョルダンの閉曲線定理]]
*可算言語に対するゲーデルの完全性定理。
*任意の可算[[可換環]]が[[素イデアル]]を持つこと。
*任意の可算形式的実体を順序体にできること。
*可算体に対する代数閉包の一意性。

=== 算術的内包公理 ACA<sub>0</sub> ===
<math>\mbox{ACA}_0 \, </math>は、<math>\mbox{RCA}_0 \, </math>に算術的内包公理を付け加えた体系である。<math>\mbox{ACA}_0 \, </math>は、任意の算術的論理式を満たす自然数の集合の存在を示す。実際、算術的内包公理を得るために、<math>\mbox{RCA}_0 \, </math>にΣ<sub>1</sub>論理式の内包公理を追加したものである。

<math>\mbox{ACA}_0 \, </math>の1階部分はペアノ算術と同じである。つまり<math>\mbox{ACA}_0 \, </math>は算術的な定理についてはにペアノ算術と証明能力は同じである。また、両者は無矛盾性については等価である。

<math>\mbox{ACA}_0 \, </math>は、可述的数学のほとんどを展開することができ、古典的数学の基本的な定理の多くを証明することができる。

算術的集合を含まない<math>\mbox{WKL}_0 \, </math>のモデルが存在するので、<math>\mbox{ACA}_0 \, </math>は<math>\mbox{WKL}_0 \, </math>よりも強いことが示される。実際、[[低基底定理]]を使った[[低集合]]を含むような<math>\mbox{WKL}_0 \, </math>のモデルは構成不可能。

<math>\mbox{RCA}_0 \, </math>上で次と<math>\mbox{ACA}_0 \, </math>は同値。
*実数全体の集合の点列コンパクト性（有界で単調増加な任意の実数列は極限を持つ）。
*[[ボルツァーノ＝ワイエルシュトラスの定理]]。
*[[アスコリの定理]]: 単位閉区間上の任意の有界で同程度連続な実関数列は一様収束する部分列を持つ。
*任意の可算可換環は[[極大イデアル]]を持つ。
*有理数体（もしくは任意の可算体）上の任意の可算ベクトル空間は基底を持つ。
*任意の可算体は[[超越基底]]を持つ。
*（任意の有限分岐木に対する、弱でない）ケーニヒの補題。
*ラムゼーの定理の一形態などを例とする組合せ論の諸定理。

=== 算術的超限再帰 ATR<sub>0</sub> ===
<math>\mbox{ATR}_0 \, </math>は、<math>\mbox{ACA}_0 \, </math>に算術的超限再帰を追加した体系である。

<math>\mbox{ATR}_0 \, </math>は<math>\mbox{ACA}_0 \, </math>上で、Σ<sup>1</sup><sub style="margin-left:-0.6em">1</sub>分離原理と同値である。

<math>\mbox{ATR}_0 \, </math>は、<math>\mbox{ACA}_0 \, </math>の無矛盾性を証明可能なので[[ゲーデルの不完全性定理]]より、<math>\mbox{ACA}_0 \, </math>より強い。

<math>\mbox{RCA}_0 \, </math>で次が<math>\mbox{ATR}_0 \, </math>と同値。
*任意の二つの可算整列順序は比較可能（一方が他方または他方の始片に同型）である。
*可算被約アーベル群に対する[[ウルムの定理]]。
* 完備可分距離空間の任意の非可算閉部分集合が完全閉集合を含むことを述べた[[完全集合性|完全集合定理]]。
*[[ルージンの分離定理]]（essentially <math>\Sigma^1_1 \, </math>分離）。
*[[ベール空間]]における[[開集合]]の[[決定性]]。

=== Π{{su|p=1|b=1}}内包公理 Π{{su|p=1|b=1}}-CA<sub>0</sub> ===
<math>\Pi^1_1\text{-CA}_0 \, </math>は、<math>\mbox{RCA}_0 \, </math>に<math>\Pi^1_1 \, </math>論理式に関する内包公理を追加した体系である。<math>\Pi^1_1\text{-CA}_0 \, </math>は非可述的な体系である。

<math>\Pi^1_1\text{-CA}_0 \, </math>と<math>\text{ATR}_0 \, </math>の関係は、<math>\text{ACA}_0 \, </math>と<math>\text{WKL}_0 \, </math>の関係に似ている。

<math>\Pi^1_1\text{-CA}_0 \, </math>は、記述的集合論における強い非可述的論法によって証明される定理と同値になる。この同値性はこれらの非可述的論法が取り除けないことを示している。

<math>\mbox{RCA}_0 \, </math>で、<math>\Pi^1_1\mbox{-CA}_0 \, </math>と次の定理が同値であることが証明できる。
*[[カントール＝ベンディクソンの定理]]（実数から成る任意の閉集合は完全集合と可算集合の和集合として書ける）。
*任意の可算アーベル群は可除群と被約群の直和として書ける。

== Big Five以外の体系 ==
逆数学においては、Big Five以外の体系も研究されている。それらはAfter Fiveとも呼ばれる。

*再帰的内包公理よりも弱い体系が定義できる。<math>\mbox{RCA}^\ast_0 \, </math>は、[[初等関数算術]]EFA(指数関数を含む算術の基本公理 + <math>\Delta^0_0 \, </math>帰納法)に<math>\Delta^0_1 \, </math>内包公理を付け加えた体系である。<math>\mbox{RCA}^\ast_0 \, </math>上で、<math>\mbox{RCA}_0 \, </math>は、可算な体の上で多項式が高々有限の根しかもたないことや、有限アーベル群の分類定理などと同値である。
<math>\mbox{RCA}_0^\ast \, </math>は<math>\mbox{EFA} \, </math>と同じ証明論的順序数
<math>\omega^3 \, </math>をもち、<math>\mbox{EFA} \, </math>上<math>\Pi^0_2 \, </math>文について保存的な拡大になっている。

*<math>\mbox{WWKL}_0 \, </math>は、<math>\mbox{RCA}_0 \, </math>に弱弱ケーニッヒの補題「無限路を持たない無限2進木のある部分木は、長さ<math>n \, </math>の葉がどれだけ存在するかを一様に推定できる」（無限路を持たない二分木の長さ n の枝の本数と <math>2^n</math> の比は <math>n\to\infty</math> でゼロに収束する）を追加した公理系である。<math>\mbox{WWKL}_0 \, </math>は、<math>\mbox{RCA}_0 \, </math>上で「任意のコンパクト距離空間における任意のボレル測度は可算加法的である」等の測度論の定理と同値になる。<math>\mbox{WWKL}_0 \, </math>のモデル理論は、[[アルゴリズム的ランダム列]]の理論と関連する。実際、<math>\mbox{RCA}_0 \, </math>の<math>\omega \, </math>-モデル<math>M \, </math>に対し, <math>M \, </math>が<math>\mbox{WWKL}_0 \, </math>のモデルであることと, <math>M \, </math>に含まれる任意の集合<math>X \, </math>について、<math>X \, </math>に対し相対的に1-randomなある<math>Y \, </math>が存在して<math>Y \, </math>が<math>M \, </math>に含まれることは同値である。
*DNR("diagonally non-recursive"の略)は、<math>\mbox{RCA}_0 \, </math>に「任意の集合に対し[[対角的非再帰]]な関数が存在する」を追加した公理系である。<math>\mbox{DNR} \, </math>とはつまり「任意の集合<math>A \, </math>に対して、ある全域的関数<math>f \, </math>が存在して、fは<math>A \, </math>から計算可能などんな部分関数とも等しくない」が成り立つということである。<math>\mbox{DNR} \, </math>は、<math>\mbox{WWKL}_0 \, </math>よりも真に弱い。(Lempp ''et al.'', 2004).
*「超算術的な集合全体からなる構造の上で成り立つ」「極小<math>\omega \, </math>モデルは超算術的な集合全体である」という性質を満たす公理系は[[Theory of hyperarithmetic analysis]]と呼ばれる。
[[Theory of hyperarithmetic analysis]]の例として、<math>\mbox{weak-}\Sigma^1_1\mbox{-AC}_0 \, </math>、<math>\Delta^1_1\mbox{-CA}_0 \, </math>、<math>\Pi^1_1\mbox{-SEP}_0 \, </math>、<math>\Sigma^1_1\mbox{-AC}_0 \, </math>は[[Theory of hyperarithmetic analysis]]があり、それぞれ<math>\mbox{ACA}_0 \, </math>に弱<math>\Sigma^1_1 \, </math>選択公理、<math>\Delta^1_1 \, </math>内包公理、<math>\Pi^1_1 \, </math>分離公理、<math>\Sigma^1_1 \, </math>選択公理を追加した公理系である。

== &omega;-モデルと&beta;-モデル==
「<math>\omega \, </math>-モデル」の<math>\omega \, </math>は非負整数全体の集合を意味する。

その1階部分が1階ペアノ算術の標準モデルになっているような、2階算術の部分体系のモデルを<math>\omega \, </math>-モデルと呼ぶ。ただし、2階部分は非標準であっても良い。すなわち、<math>\omega \, </math>-モデルは<math>S \subseteq \mathcal{P}(\omega) \, </math>（<math>\mathcal{P}(\omega) \, </math>は<math>\omega \, </math>の部分集合全体のクラス）によって与えられる。数変数は <math>\omega \, </math>の元として解釈され、定数記号<math>0, 1 \, </math>や関数記号<math>+, \times \, </math>は標準的に解釈される。一方、集合変数は <math>S \, </math>の元として解釈される。<math>S = \mathcal{P}(\omega) \, </math>とする<math>\omega \, </math>-モデルを2階算術の標準モデルと呼ぶ。しかし、標準モデル以外にも<math>\omega \, </math>-モデルは存在する。たとえば、<math>\mbox{RCA}_0 \, </math>は<math>S \, </math>として計算可能な<math>\omega \, </math>の部分集合全体をとった<math>\omega \, </math>-モデルをもつ。

<math>\omega \, </math>-モデルであって、<math>\Sigma^1_1 \, </math>文について、標準モデルと真偽が一致するものを<math>\beta \, </math>-モデルと呼ぶ。<math>\mbox{ACA}_0 \, </math>において全ての<math>\beta \, </math>-モデルが<math>\mbox{ATR}_0 \, </math>のモデルであることが示せる。また、<math>\mbox{ACA}_0 \, </math>において、「任意の集合<math>X \, </math>について<math>X \, </math>を含む<math>\beta \, </math>モデルが存在する」は <math>\Pi^1_1\mbox{-CA}_0 \, </math>と同値である。

一般に、<math>\omega \, </math>-モデルであって、<math>\Sigma^1_n \, </math>文について、標準モデルと真偽が一致するものは<math>\beta_n \, </math>-モデルと呼ばれる。

また、Non-<math>\omega \, </math>-モデル（1階部分が標準ではないモデル）も、ある公理系が保存的拡大であることの証明にしばしば登場する。

== 参考文献 ==
*{{Cite book|和書
|author=田中一之|authorlink=田中一之
|others=倉田令二朗 監修
|date=1997-08
|title=逆数学と2階算術
|series=数学基礎論シリーズ 4
|publisher=河合文化教育研究所
|isbn=978-4-87999-970-2
|ref={{Harvid|田中|1997}}
}}
*{{Citation
|author = Ambos-Spies, K.
|coauthors = Kjos-Hanssen, B.; Lempp, S.; Slaman, T.A.
|year = 2004
|title = Comparing DNR and WWKL
|journal = Journal of Symbolic Logic
|volume = 69
|issue = 4
|doi = 10.2178/jsl/1102022212
|pages = 1089
|postscript = .
}}
*{{Citation | last1=Friedman | first1=Harvey | title=Proceedings of the International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1 | publisher=Canad. Math. Congress, Montreal, Que. | id={{MathSciNet | id = 0429508}} | year=1975 | chapter=Some systems of second order arithmetic and their use | pages=235–242}}
*{{Citation | last1=Friedman | first1=Harvey | title=Meeting of the Association for Symbolic Logic | url=http://www.jstor.org/stable/2272259?seq=7 | publisher=Association for Symbolic Logic | year=1976 | journal=The Journal of Symbolic Logic | issn=0022-4812 | volume=41 | issue=2 | chapter=Systems of second order arithmetic with restricted induction,  I, II  | pages=557–559}}
*{{Citation | last1=Simpson | first1=Stephen G. | title=Subsystems of second order arithmetic | url=http://www.math.psu.edu/simpson/sosoa/ | publisher=[[Cambridge University Press]] | edition=2nd | series=Perspectives in Logic | isbn=978-0-521-88439-6 | id={{MathSciNet | id = 2517689}} | year=2009}}
*{{Citation
|last=Stillwell
|first=John
|date=2019-09-24
|title=Reverse Mathematics: Proofs from the Inside Out
|publisher=Princeton University Press
|location=Princeton, NJ
|edition=Paperback
|isbn=978-0-691-19641-1
}}
**{{Cite book|和書
|author=ジョン・スティルウェル
|others=田中一之 監訳・解説
|translator=川辺治之
|date=2019-02
|title=逆数学　定理から公理を「証明」する
|publisher=森北出版
|isbn=978-4-627-05451-6
|ref={{Harvid|スティルウェル|2019}}
}}
*{{Citation | doi=10.2307/421140 | last1=Solomon | first1=Reed | title=Ordered groups: a case study in reverse mathematics | url=http://www.jstor.org/stable/421140 | id={{MathSciNet | id = 1681895}} | year=1999 | journal=The Bulletin of Symbolic Logic | issn=1079-8986 | volume=5 | issue=1 | pages=45–58}}

== 外部リンク ==
*[http://www.math.ohio-state.edu/~friedman/ Harvey Friedman's home page]
*[http://www.math.psu.edu/simpson/ Stephen G. Simpson's home page]

[[Category:数理論理学]]
[[Category:再帰理論]]
[[Category:証明論]]
[[Category:数学に関する記事]]
{{デフォルトソート:きやくすうかく}}