序 章

数学基礎論の考え方

1 数学の意味と形式
どんな学問においても，その入り口の基本用語を日常の言葉で説明したり，
またそれを正しく理解したりすることは大変なことだ．日常語の曖昧さや多義性によって生じる誤解はいうまでもなく，数学基礎論のような根元的な学問においては，言語が本質的にもつ機能の多面性や多層性が誤謬の原因になる．端的にいうと，言語には意味と形式という 2 つの機能があって，話し手と聞き手がお互いにどちらのチャンネルで話しているかをその都度了解していないと対話が成立しない．当たり前のことではあるが，こと数学に関して
は，こうした通念の整理がなおざりにされていて，教育にも支障をきたしているように見える．
例えば，「定数」という基本用語がある．かつて中学校・高等学校の数学の教科書や参考書類を調べたところ，次のような判読し難い説明をしているものがたくさん見つかった∗1 ．
いろいろな値をとって変化する文字を変数という．
これに対して，変化しない一定の数を定数という．
∗1

十数年前のこと．このような記述は近年減少したようだ．

序章 数学基礎論の考え方

2

変数の方は「値が変化する文字」ということで理解できるにしても，「変化しない数」という表現においては，変化したりしなかったりする主体は何なのかと考えてしまう．付言しておくと，「関数 f (x) が定数である」というような表現においてならば「定数」を「一定の数」と解することも可能であるが，ここでは数式に現れる「変数」と「定数」を比較して説明しているのである．
英語で考えれば，少し見通しがよくなるかもしれない．上の場合の「定数」
は単にコンスタント（constant）
であり，コンスタント・ナンバーではない．ついでに「変数（variable）」「関数（function）」「級数（series）」なども英語と比較すると，語尾に「数」が単に語呂合わせでついているように見える∗2 ．
次の 2 つの文を比較してほしい．

(1a) 6 は，偶数である．
(1b) 6 は，定数である．
偶数も定数も数学用語ではあるが，上の 2 文は異なるチャンネルのメッセー
ジと解さなければならない．わかりにくければ，次のような例はどうだろう．

(2a) 6 は，9 に 2/3 を掛けて得られる．
(2b) 6 は，9 を 180◦ 回転して得られる．
文 (1a) と文 (2a) は，記号「6」が意味する数 6 についての主張であり，文 (1b)と文 (2b) は，記号「6」そのものについての主張である．前者は数学的真理をあつかう狭義の “数学” であるのに対し，後者は数学の形式を議論する超数学またはメタ数学とよばれる．
従来の数学，つまり広義の “数学” では，しばしば数学とメタ数学が混在していて，それらを分別しにくいときがある．例えば，「x2 + 2x + 2 は正である」はほぼ 100%数学的主張ととれるが，「x2 + 2x + 2 は 2 次式である」の診断は難しい．文字列としての式「x2 + 2x + 2」の性質を述べているのだろ
マ

∗2

テ

ー

マ

タ

「数学
（mathematics）」はギリシャ語源的には「勉強して学ぶべきこと（mathemata）」
マ テ ー テ ー ス」は聖書では「弟子」と訳される．
の意味である．ちなみに「学ぶ者（mathetes）

2 射影幾何の双対原理

3うか，x2 + 2x + 2 が意味する関数やグラフの性質を述べているのだろうか？
文脈にもよるかもしれないが，多くの場合は両方の主張を同時に表していて，それでも大概は問題ない．むしろ，しばしば問題を生じるのは，意味世界における概念の多層構造が対話の立ち位置を混乱させることかもしれない．例えば，先程の二例においても，最初の「x2 + 2x + 2」は関数を表すものではなく，（任意の）x に対する x2 + 2x + 2 の値を表す．数学基礎論では，x2 + 2x + 2が表す関数は λx. x2 + 2x + 2 と記すことで，混乱を減じている．
歴史を振り返ると，数学とメタ数学が意識的に分離され，メタ数学が独立に議論されるようになるのは，幾何学の公理の再検討が始まる 19 世紀のことである．また同じ頃，代数の記号的方法を論理に応用する試みから誕生したのが記号論理学である．それを用いてメタ数学の数学化が図られた結果，20世紀前半に数学の一分野としての数学基礎論が確立する．以来，証明論，モデル理論，集合論，計算論などさまざまな技術専門分野が派生し，20 世紀後
半にはそれらを総称してロジック（logic）とよぶようになった．現在では数学基礎論がロジックの一分野としてあつかわれることも多い．
まずはメタ数学における最初の画期的な発見である射影幾何の双対原理についておさらいしておこう．

2 射影幾何の双対原理
話を簡単にするため，2 次元平面上で点と直線のみをあつかう射影幾何を考える．射影幾何は，射影によって変わらない図形の性質を調べる幾何であり，
ユークリッド幾何から長さや角度のような計量的な概念を除いたものになっている．ここでは，とりあえず「点」
「直線」
「
（点）
が
（直線）
の上にある」「（直線）が（点）を通る」という用語だけを用いる幾何学としておこう．
このような簡単な幾何でも，次のような結構深みのある命題が表現できる．

4

序章 数学基礎論の考え方

パッポスの定理 2 つの直線 l, l の上に，それぞれ 3 つの点 A, B, Cと A , B  , C  がある．このとき，（A と B  を通る直線）と（A と B を通る直線）の交点，（B と C  を通る直線）と（B  と C を通る直線）の交点，（A と C  を通る直線）と（A と C を通る直線）の交点
は，一直線上にある（図 1）．
C

l

B

A

A

B
図1

C

l

パッポスの定理

読みやすさのために多少表現を工夫してあるが，基本用語を論理的につなぐだけで定理が表現されていることに注意されたい．
いま，射影幾何の任意の命題 σ をとってきて，文中の「点」と「直線」の2 語を入れ替え，それにしたがって「（点）が（直線）の上にある」と「（直線）が（点）を通る」という述語も入れ替えると，別の意味をもつ命題 σ ができる．

 を σ の双対（dual）とよぶ．このとき，次のことがいえる．
この命題 σ射影幾何の双対原理（ジェルゴンヌ - ポンスレ） 命題 σ が射影幾何の定理であれば，その双対 σ も定理になる．
例えば，パッポスの定理 σ に対する双対 σ は次のようになる．

第

1章

等式理論

本章では，等式の形をした公理によって定められる数学的理論の特徴について考察する．具体的には，そのような理論のモデル全体がもつ性質（例えば，直積に関して閉じている）
を調べる．ここでの主要な結果は，1.3 節で証明するバーコフの完全性定理と等式クラス定理であるが，それらは第 2 章，第 3 章で論理記号を含んだ公理系に拡張される（とくに，定理 2.3.9 と定理 3.4.8）．論理式のさま
ざまな形態によって理論が分類され，そうした分類とモデルの性質の関係を明らかにしていくことが第 1 部全般の主題である．
また 1.4 節では，重要な等式理論であるブール代数に関する基本的事実（双対定理，積和標準形など）について述べる．1.5 節では，等式理論のもう 1 つの応用としてエルブラン - ゲーデルの一般再帰的関数を導入する．そして，これが計算可能関数に一致することを示す．

1.1 等式の形式体系
1.2 代数構造と準同型
1.3 自由代数とバーコフの完全性定理
1.4 ブール代数
1.5 計算可能関数と一般再帰的関数

14

第 1 章 等式理論

1.1 等式の形式体系
本節では，群の等式理論を題材として，数学の証明がどのようになされているかを観察し，その形式化について考える．序章で述べたように，群論の公理の定め方にはいろいろあるが，ここでは議論を簡単にするために，以下のような等式の公理を採用する．
定義 1.1.1

群の理論（単に群論（group theory）とよぶ）Gp は次の 3 つの公理からなる．

⎧
G1 :
⎪
⎨
G2 :
⎪
⎩
G3 :

(x • y) • z = x • (y • z) （結合律）e•x = x

（左単位元）

x−1 • x = e（左逆元）

上の 3 つの等式に現れる x, y, z は変数，e は定数であり，−1 は 1 変数関数
記号である．
いま，G を空でない集合とし，∗ を G 上の 2 変数関数，∼ を G 上の 1 変数関数，e を G の元とする．そして，公理の記述に現れる • , −1 , e を G 上でそれぞれ ∗, ∼ , e と解釈し，変数に G の任意の元を代入して等号の両辺が同じ値になるとき，構造 G = (G, ∗, ∼ , e) を群論 Gp のモデル（model）
，ある
いは単に群
（group）とよぶ．
一般に，公理的体系は公理となる命題の集合で規定されるので，命題（論理式）の集合を理論（theory）とよぶ．構造 M が理論 T のすべての命題 σ を成り立たせるときに M |= T ∗1 と記して，M は T のモデルであるという．とくに，T = {σ} のときは M |= σ と書き，σ が M において真（true）であることを表す．さらに，命題 δ が理論 T のすべてのモデルで成り立つとき，δ は

T の帰結（consequence）である，あるいは T で成り立つ（hold, valid）といい，
T |= δ と書く．
∗1

記号 |= は，ダブル・ターンスタイル（double turnstile）とよばれる．

1.1 等式の形式体系

15

群論 Gp において成り立つ命題の例として，次の定理を見てみよう．
定理 1.1.2

Gp |= x • x−1 = e （右逆元）

証明 G = (G, ∗, ∼ , e) を任意の群とする．G の任意の元 a を選んで，a ∗a∼ = e を示せばよい．
まず，a ∗ a = a ならば a = e を示そう．a ∗ a = a の両辺に左から a∼ をかけ，a∼ ∗ (a ∗ a) = a∼ ∗ a を得る．この左辺は，a∼ ∗ (a ∗ a) = (a∼ ∗ a) ∗ a（G1 より）=e∗a（G3 より）=a（G2 より）となり，また右辺 a∼ ∗ a は G3 より e に等しいから，a = e を得る．
そして，

(a ∗ a∼ ) ∗ (a ∗ a∼ ) = a ∗ (a∼ ∗ (a ∗ a∼ ))∼∼（G1 より）= a ∗ ((a ∗ a) ∗ a )（G1 より）= a ∗ (e ∗ a∼ )（G3 より）∼（G2 より）=a∗a .
よって，上で示したことより，a ∗ a∼ = e.
［問題 1］ Gp |= x • e = x（右単位元）を示せ．

を x • x−1 = e（右逆元）に置き換えたものを Gp と［問題 2］ Gp の公理 G3（左逆元）する．このとき，Gp においては G3 が成り立たないこと，すなわち Gp |= x−1 • x = eを示せ．

上の定理 1.1.2 の証明は数学でふつうに行われている議論であって，何ら問題がないように見える．だが，改めて考えてみれば，任意の群 G をもってきて，さらに任意の元 a を選んで議論するというのは，読み手の数学能力に頼った不確実な論法のようでもある．Gp |= x • x−1 = e という主張は，読み手が

16

第 1 章 等式理論

想像しうる群のみに関して，あるいは現在までに知られている群の実例の範囲において右逆元があれば，それによって真であるといえるのだろうか？
しかし，任意の群 G とその任意の元 a を定めてしまえば，あとは単純な式変形になっている．その変形は，Gp の公理を出発点にして，等号に関する規則だけを使って得られるもので，その道筋は以下に述べるように完璧に舗装（形式化）できる．そうであれば，実はその道に何を選んで通すかは問題でない．入り口を通るもの，つまり公理を満たす構造であれば，何であっても必ず出口において定理を満たすからである．
それでは，議論の舗装に必要な等式の形式体系を導入しよう．まず，対象となる理論の言語を規定しておかなければならないが，一般的な定義は次節にまわして，ここでは群論の • , −1 , e のような数学記号の集合と考えておけ
ばよい．これらの記号と変数を，括弧を用いながら，適当に組み合わせてできる記号列が項（term）である．項 s • t をしばしば st と略する．そして，項s, t に対し，記号列 s = t を等式（equation）とよぶ．与えた理論 T のもとで，正しい等式だけを導く仕組み（演繹体系）を以下の 2 つの定義で定める．
定義 1.1.3

T を等式の集合とする．T の等式理論（equational theory（）これも T で表す）は，次の公理と規則からなる．

(1) T に属する等式は公理である．
(2) t = t の形の等式は公理である．
(3) 以下の 4 つの図式は（上式が成り立つとき，下式が成り立つことを表す）規則である．ただし，s, t, si , ti , u (1 ≤ i ≤ n) は項，x は変数，

f は T に含まれる関数記号である．
s = t (sym),s = t t = u (trans),t=s
s=us(x) = t(x)s1 = t1 . . . sn = tn(sub),(comp).
s(u) = t(u)f(s1 , . . . , sn ) = f(t1 , . . . , tn )ここで，公理 (2) は等号の反射律であり，規則 (sym) は対称律，規則 (trans)

第

2章

1階論理

本章では，1 階論理（述語論理）についての基本的事項を学ぶ．第 1 章では等式だけをあつかう形式体系の性質を調べたが，1 階論理ではいろいろな関係記号や論理記号（例．∧, ∀）を使った表現が可能となり，普通の数学の議論が（例．<）
ほぼ不自由なくこの論理の上で展開できる．

1 階論理の形式化にはさまざまな種類があるが，ここでは第 1 章の等式理論の形式化に類似したゲンツェン - テイトの体系 GT をあつかう．そして，これに対して完全性定理（論理的に真なる文はすべて証明可能であること）
をヘンキンの方法で証明する．この証明法からは，コンパクト性定理やレーベンハイム - スコーレムの定理も直に得られる．また，完全性定理を応用して，理論の翻訳について述べる．最後に，1 階論理の拡張である多領域論理や 2 階論理について付録で説明する．

2.1 言語と構造
2.2 ゲンツェン - テイトの形式体系 GT
2.3 ゲーデルの完全性定理
2.4 言語の拡張と理論の翻訳
付録

多領域論理と 2 階論理

62

第 2 章 1 階論理［問題 1］ 等号公理 x1 = y1 , . . . , xn = yn , R(x1 , . . . , xn ), ¬R(y1 , . . . , yn ) で R が等式になる場合を認めれば，それと定義 2.2.2(2) の等号公理 (i) から等号公理 (ii) と(iii) が導けることを示せ．

補題 2.2.4

任意の論理式 ϕ について， ¬ϕ, ϕ．

証明 ϕ の構成に関する帰納法によって示す．ϕ が原子論理式のときは，公理である．ϕ ≡ ψ ∨ θ のとき，¬ϕ ≡ ¬ψ ∧ ¬θ であり，

¬ψ, ψ
¬θ, θ
(増)
(増)
¬ψ, ψ, θ¬θ, ψ, θ(∨)(∨)¬ψ, ψ ∨ θ¬θ, ψ ∨ θ(∧) .
¬ψ ∧ ¬θ, ψ ∨ θ
ϕ が他の形の論理式の場合も同様に示されるので，残りは演習問題とする．
この補題 2.2.4 により，例 4 において，ϕ, ψ は原子論理式に限らず一般の論理式でもよいことがわかる．

2.3 ゲーデルの完全性定理
この節では，前節で導入した形式体系 GT に対して完全性定理を証明し，そのいくつかの応用について述べる．
定理 2.3.1（演繹定理（deduction theorem）） 言語 L における理論

T ，文 ϕ，シークエント Γ に対して，
T ∪ {ϕ}  Γ =⇒ T  ¬ϕ, Γ.
証明 T ∪ {ϕ}  Γ の証明木 P に現れるすべてのシークエントに論理式¬ϕ をつけ加えた木を P  とする．P の最上点以外の頂点における推論規則の関係はこの書き換えのあとでも同種の推論規則になる（注．¬ϕ は文なので規則（∀）の条件が保たれる）
が，P  の最上点のラベルはそのまま公理になるとは

68

第 2 章 1 階論理定理 2.3.9（ゲーデルの完全性定理（completeness theorem））

T  ϕ ⇐⇒ T |= ϕ.
証明“ T  ϕ ならば T |= ϕ ” は簡単にわかる．実際，シークエント

ϕ1 , . . . , ϕn の真偽を ϕ1 ∨ · · · ∨ ϕn の真偽と考えれば，T の公理，排中律，
等号公理は T の任意のモデルで真である．また，各推論規則において前提が真であれば結論も真になることは明らかだから，証明木に現れるシークエン
トはすべて真であり，とくに根の ϕ は T の任意のモデルで真である．
逆を示すために，T  ϕ でないと仮定する．ϕ が自由変数 x0 , . . . , xn を含
むときは，ϕ の代わりに ∀x0 · · · ∀xn ϕ を考え，ϕ は文であると仮定してよい．すると，補題 2.3.3 より，T ∪ {¬ϕ} は無矛盾である．したがって，補題

2.3.6 によって，T ∪ {¬ϕ} はモデルをもつので，T |= ϕ でないことになり，完全性定理が証明された．
定理 2.3.10（コンパクト性定理（compactness theorem）） 理論 T がモデルをもつための必要十分条件は，T の任意の有限部分集合がモデルをもつことである．
証明

必要性は明らかなので，十分性を示す．T の任意の有限部分集合がモデルをもつとすれば，任意の有限部分集合が無矛盾であるから，T 自身からも矛盾は導かれない．よって，完全性定理により，T はモデルをもつ．
［問題 2］ T1 ∪ T2 が矛盾していれば，ある文 σ が存在して，T1  σ かつ T2  ¬σとなることを示せ．
［問題 3］ 次を示せ．

(1) 群に（演算を保存するような）順序が入るための必要十分条件は，すべての有限生成部分群に対し順序が入ることである．

(2) アーベル群に順序が入るための必要十分条件は，ねじれがないことである

第3章

モデルの理論

第 1 章では，構造のクラスが等式理論で公理化されるための必要十分条件を与えた（バーコフの等式クラス定理）．本章では，1 階論理におけるいろいろな形の公理系（例．ホーン理論）とそのモデルのクラスの特徴を調べていく．そして，その分析の道具として，モデルの理論で用いられる基本概念（初等的部分構造，初等鎖，モデル完全，約積，超積など）を導入する．
最後に，モデルの理論の重要な応用である超準解析について述べる．超積ないし超ベキを使って，無限大や無限小を含んだ実数の超準世界が構成されると，そこでは本来の極限操作が有限的な計算に置き換わる．この超準的手法は，弱い体系でも限定的に利用でき，第 8 章の議論に用いられる．

3.1 初等的部分構造
3.2 ∀ 理論と ∀∃ 理論
3.3 ホーン理論と約積
3.4 超積3.5 超準解析入門

第3章

104

モデルの理論3.5 超準解析入門
前節で導入した超ベキを用いて，自然数，実数，関数空間などのさまざまな構造に対し，それらを初等的部分構造として真に含む大きな構造（超準モデ
ル）を作ることができる．とくに，実数の超準モデルは，標準モデルからみての無限大や無限小を要素として含んでおり，ライプニッツ流の無限小解析に初めて合理的なモデルを与えたものとして重要な意義をもつ．超準的手法は数学のさまざまな分野に応用されるようになっているが，とくに解析学への応用は超準解析とよばれ，大きな研究領域になっている．
この節を通して，自然数 ω (= N) 上の非単項超フィルター U を 1 つ固定する．
構造 A の超ベキ Aω /U を ∗ A で表す．前節で示したように，A から ∗ A へは自然な埋め込み d(a) = ∗ a があり，A とその像 d(A) を同一視すれば，A は ∗ A の初等的部分構造とみなせる．N = (N, +, • , 0, 1, <) や R = (R, +, • , 0, 1, <) な
ど我々が数学的な経験の中で自然に理解している構造を標準モデル（standard

model）といい，∗ N や ∗ R などをそれらの超準モデル（nonstandard model）という．
標準モデルとそれに対応する超準モデルは，初等的命題の真偽に関して差はないが，基本的な性質でも初等的に表現できないものがあることに注意しておきたい．この節で我々があつかうのは，実数の超準モデル ∗ R であるが，そのアルキメデス性は初等的に表現できない．ここで，順序体 A が，アルキメデス的（Archimedian）であるとは，任意の正の元 a, b ∈ |A| に対し，十分
n個




大きな自然数 n ∈ N が存在して，b < a + a + · · · + a となることである．
定理 3.5.1∗

R は，非アルキメデス順序体である．

証明 R は順序体であり，“順序体である” ことは初等的に記述できる性
質であるから，∗ R も順序体である．次に，非アルキメデス性をいうために，

3.5 超準解析入門

105

s = 1, 2, 3, . . . ∈ |Rω | とし，N = [s] ∈ |∗ R| とおく．このとき，任意の自

∗

n個



∗



然数 n ∈ N に対して，N > 1 + 1 + · · · + ∗ 1 となる．なぜなら，{i | a(i) >n} ∈ U だからである．
定義 3.5.2|∗ R| の元 a が無限大（inﬁnite）であるとは，∀b ∈ R b < |a| とであるという．|∗ R| のなることをいう．また，無限大でない元は有限（ﬁnite）
元 a が無限小（inﬁnitesimal）
であるとは，∀b (> 0) ∈ R |a| < b となることをいう（図 3）．
−∞R0（マイナス）無限大

0

+∞

無限大

∗

R
拡大
標準実数

0

標準実数

無限小 無限小図 3 実数の超準モデル ∗ R

例4

N = [1, 2, 3, . . .] は無限大であり，1/N = [1/1, 1/2, 1/3, . . .] は無限小である．
［問題 10］ (1)

無限小全体が + と • の演算で閉じていることを示せ．

(2) a が無限大であることと，1/a が無限小であることは同値であることを示せ．

定義 3.5.3

a, b ∈ |∗ R| に対し，a≈b⇐⇒

a − b は無限小．

≈ は同値関係であり，さらに + と • の演算を保存していることも容易にわ
かる．

第

4章

1階算術と不完全性定理

本章では，まず，ペアノ算術とその部分体系のさまざまな性質，とくに表現可能性と証明可能性を調べる．これらの考察を総合して導かれる結果が，「どんな算術の体系にも証明も反証もできない文が存在する」というゲーデルの第一不完全性定理である．そして，さらに精密な分析により「どんな算術の体系も自らの無矛盾性を証明できない」という第二不完全性定理を得る．
「どんな算術の体系」といっても，2 つの定理で要求される仮定が若干異なる．第一定理の証明においてメタ的に使用される原始再帰的関数の役割が，第二定理の証明では体系内の形式的対象としてあつかわれ，その議論に Σ1 帰納法を用いる．これら 2 つの証明の質の差を理解することで，数学基礎論という学問の奥行きの深さを掴んでほしい．他方，演算が足し算だけに制限された体系（プレスバーガー算術）においては，このような不完全現象は生じない．プレスバーガー算術の完全性と決定可能性の証明には，量化記号消去を用いる．

4.1 ペアノ算術と部分体系
4.2 算術の最弱体系 R
4.3 体系 IΣ1 と原始再帰的関数
4.4 第一不完全性定理
4.5 第二不完全性定理
4.6 プレスバーガー算術と量化記号消去

第4章

112

1 階算術と不完全性定理

4.1 ペアノ算術と部分体系
本節では，ペアノ算術 PA とその代表的な部分体系 PA− , IΣn , Q などを定義し，その基本的な性質を調べる．
まず，言語 LOR を順序環の記号集合 {+, • , 0, 1, <} とする．ペアノ算術は
この言語における理論として，次のように定義される．
定義 4.1.1

ペアノ算術（Peano arithmetic, PA と略す）は，次の公理からなる LOR の理論である．

A1.

∀x ¬(x + 1 = 0).

A2.

∀x ∀y (x + 1 = y + 1 → x = y).

A3.

∀x (x + 0 = x).

A4.

∀x ∀y (x + (y + 1) = (x + y) + 1).

A5.

∀x (x • 0 = 0).

A6.

∀x ∀y (x • (y + 1) = x • y + x).

A7.

∀x ¬(x < 0).

A8.

∀x ∀y (x < y + 1 ↔ x < y ∨ x = y).

A9.

ϕ(0) ∧ ∀x (ϕ(x) → ϕ(x + 1)) → ∀x ϕ(x), ただし ϕ(x) は任意の LOR論理式で，x 以外にも自由変数を含んでいてよい．

A1, A2 は次の数 x + 1 の性質を規定する最も基本的な公理であり，いわゆ
る「ペアノの公理」にもある．A3, A4 は足し算，A5, A6 は掛け算，A7, A8
は不等号をそれぞれ帰納的に定める公理であり，どれも「ペアノの公理」にはを表す公理図式（axiom scheme）
規定されていない．A9 は帰納法（induction）
であり，論理式 ϕ(x) ごとに規定される公理をまとめて書いたものである．「ペアノの公理」では，帰納法を集合の言葉で表現していたが，公理図式を用いることで集合論を前提としなくなったところがこの形式化の重要なポイントである．

4.5 第二不完全性定理

T σ

=⇒

137



T  ¬ψ σとなるような論理式 ψ(x) はない．
証明 そのような ψ(x) があったとすると，¬ψ(x) に対する不動点 σ をとり，ゲーデル - ロッサーの不完全性定理の証明と同様に矛盾が導かれる．
補題 4.4.16

T で証明可能な文のゲーデル数の集合 {σ | T  σ, σ は文である} は再帰的でない．
証明 T の定理の集合が再帰的であれば，前節の結果より R で表現可能になり，すなわち上の補題 4.4.15 の ψ(x) が存在することになる．
定理 4.4.17（チャーチの述語論理決定不可能性（undecidability ofpredicate calculus）） 言語 LOR（または LAR ）において，述語論理の公理だけから証明できる文のゲーデル数の集合 {σ |  σ, σ は文である} は再帰的でない．
証明 Q< は有限理論であるから，その公理をすべて ∧ でつないで，1 つの文にしたものを ξ とおく．演繹定理から Q<  σ ⇐⇒  ξ → σ であるから，{σ |  σ} が再帰的であれば，{σ |  ξ → σ} = {σ | Q<  σ} も再帰的になり，上の補題 4.4.16 に反する．

4.5 第二不完全性定理
ゲーデルの第一不完全性定理は，算術の公理系 T に対して証明も反証もできない文の存在を示したものだが，第二不完全性定理は「T が無矛盾である」という意味をもつ具体的な文が T で証明できないことを主張する．大雑把にいえば，第二定理は，第一定理の証明を体系 T 内で形式化することによって得られるのだが，それには異次元の緻密さが要求される．端的には，第一定第5章

1階算術の超準モデル

本章の目的は 2 つある．第 1 の目的は，1 階算術の超準（非標準）モデル，とくに可算超準モデルの性質を調べることである．なかでも，自己埋め込み性（自己同型の始切片の存在）に関する H. フリードマンらの結果は算術の超準モデルの際立った特徴付けであり，この定理は第 8 章で 2 階算術に拡張される．
第 2 の目的は，証明に使われる超準モデルの構成法についての一般的理解にある．排除タイプ定理や再帰的飽和モデルや往復論法などは，算術に限らず，幅広
い応用がある．最後の節では，自らの充足関係を内在するような麗質モデルについて調べる．

5.1 超準モデルと過剰原理
5.2 排除タイプ定理と終拡大
5.3 再帰的飽和モデルと自己埋め込み定理
5.4 麗質モデルと充足関係
付録 A 往復論法
付録 B

麗質モデルの応用

第6章

実閉体の完全性と決定可能性

自然数の理論は必ず不完全になることをゲーデルが示したあと，タルスキが発見した対照的な事実は，実数や複素数の理論には完全な公理系が存在することであった．その証明の鍵となったのは，第 5 章で用いた量化記号消去の手法である．のちにさまざまな改良が加えられたが，それでも実数の理論に対して，式変形による量化記号消去を直接示すことは容易でない．ここでは，アルティンとシュライアーによって創始された実閉体理論の結果を用いて，量化記号が消去可能であるという事実を間接的（モデル理論的）に導こう．
最初に 6.1 節で実係数の多項式についての基本的事実を復習し，6.2 節で実閉体理論の要となるアルティン - シュライアーの定理を証明する．これを用いて，

6.3 節で量化記号消去を示し，さらに実閉体理論の完全性と決定可能性を導く．
6.4 節では複素数体の理論を代数閉体の理論としてあつかって完全性と決定可能性を示し，さらにその応用について述べる．付録 A では，実閉体理論の完全性を応用した，ヒルベルトの第 17 問題の解法について説明する．付録 B では，実閉体理論の発展となる順序極小理論について簡単に述べる．

6.1 実係数の 1 変数多項式
6.2 実閉順序体
6.3 実閉順序体の量化記号消去
6.4 複素数と零点定理
付録 A

ヒルベルトの第 17 問題
付録 B 順序極小理論

第7章

実数論と逆数学

2 階算術は，自然数と，自然数からなる諸集合を対象とした形式理論であるが，実数や実数列，そして実数上の連続関数などもそのような集合としてあつかう
ことができる．そこで，数学の各定理を証明するのに，2 階算術のどのような集合存在公理が必要かを調べる研究プログラムが誕生し，逆数学とよばれるようになった．
まず，7.1 節で逆数学の土台となる体系 RCA0 を導入し，7.2 節ではその上で展開される実数論をみる．例えば，区間縮小法の原理が成り立ち，実数の非可算性もいえる．しかし，点列コンパクト性などにはさらに強い公理が必要で，それらは 7.3 節で説明する．7.4 節では，ラムジーの定理のバリエーションにはさらに細かい分類が必要であることの一端をみる．7.5 節では，無限ゲームの決定性には通常の公理よりはるかに強い仮定が必要になることをみる．

7.1 逆数学と基本体系 RCA0
7.2 RCA0 上の実数論
7.3 実数の完備性とコンパクト性
7.4 ケーニヒの補題とラムジーの定理
7.5 無限ゲームの決定性
付録 A

差階層
（エフェクティブ版）

付録 B ヒルベルトのプログラム

226

第7章

実数論と逆数学

7.1 逆数学と基本体系 RCA0
2 階算術という枠組みにおいて，数学的性質や定理を証明するのにどの程度の集合存在公理が必要かを調べる研究は「逆数学」とよばれる．証明に必要な存在公理によって数学の多様な命題が織りなす世界に等高線を入れてみると，数学史の流れや，異なる理論間の感覚的な類似性がうまく捉えられるというのがこの研究の売り物である．例えば，中間値の定理より実数の公理（例．
ヴァイエルシュトラスの上限に関する公理）の方が強い存在公理を必要とすることが証明される．解析学の教科書で，中間値の定理が実数の公理より前に説明されることはありえないと思うが，歴史の流れは逆であり，歴史はより高度な集合論を求める方向に進んだとも解釈できよう．別の例として，実数列に関するボルツァーノ - ヴァイエルシュトラスの定理と，関数列に関するア
スコリ - アルツェラの補題が同値になるという結果がある．一般的に後者は前者より遙かに高度な主張と思われているが，前者の定理をヴァイエルシュトラスが明確に述べたのは，後者の定理が発見されるのとほぼ同時期であった．
さて，1 階論理の枠組みでの自然数の理論を「1 階算術」という．その代表「2 階算術」は，当初 2 階は，第 4, 5 章であつかったペアノ算術 PA である．
論理上の自然数論であったが，2 階論理自体の形式化が難しいため，今日では自然数と，自然数からなる諸集合を対象とした（2 領域の）1 階理論として定式化されている．2 階算術のフル体系 Z2 は，1 階論理の公理，推論規則に加えて，自然数の順序や和積演算に関する諸公理と，定義し得るどんな自然数の集まりも “集合” としてあつかえることを保証する集合存在公理（内包公理）からなり，その集合存在公理に種々の制限をつけることにより部分体系が得られる．以下の議論においてとくに重要な部分体系は（証明能力の）弱い方
から順に，RCA0 , WKL0 , ACA0 , ATR0 , Π11 -CA0 の 5 つで，これらをビッグ5（pp.227–228 参照）という．例えば，RCA0 は Recursive Comprehension
Axiom（再帰的内包公理）の頭文字をとったもので，この体系では再帰的集合

7.1 逆数学と基本体系 RCA0227の存在のみが保証されている．また，添え字の 0 は帰納法の制限を表すが，これについては p.231（定義 7.1.2 の下）で後述する．

1970 年代半ば，H. フリードマンは Z2 の各部分体系でどれだけの数学が展開できるかを調べ，次のような現象がしばしば観察されることに気づいた∗1 ．

フリードマン：逆数学現象
数学の定理の多くは RCA0 で証明できるか，そうでなければ上にあげた他の 4 つの体系のどれかと論理的に同値であることが RCA0において証明できる．

その後もこのパターンに当てはまる多くの定理がシンプソンを中心とする研究グループによって発見された．しかし，この現象に当てはまらない例も少なからず知られており，最近の研究ではむしろ例外の方に関心が移っているともいえる．ここで，5 つの公理系とそこで証明できる定理の特徴をまとめておく．正確な定義は後で与える．

逆数学ビッグ 5

1．RCA0自然数の基本演算に関する公理とある種の帰納法，そして再帰的内包公理とよばれる集合存在公理からなる．粗っぽくいえば，RCA0
で展開される数学は計算機があつかえる範囲の数学であり，計算可能解
析学（computable analysis）
とか再帰的代数学（recursive algebra）などの形式化にあたる．例えば，RCA0 で中間値の定理が証明できる．なぜなら，2 分法というアルゴリズムで，任意の n > 0 に対し，誤差 ± n1 以内の近似有理解を有限ステップで求めることができるからである．

2．WKL0∗1

RCA0 に「無限個の頂点をもつ 2 分木は無限長の道（path）を1974 年にカナダ・バンクーバーで開催された国際数学者会議（ICM）における彼の有名な基調講演 “Some systems of second-order arithmetic and their use” での報告
は，厳密にいえば，この現象とは若干異なる．とくに，帰納法の制限を考えていない．

第8章

2階算術と超準的方法

本章では，2 階算術における 2 種類のメタ数学的論法を紹介する．最初の種類
は「保存的拡大」の応用で，なかでもスマートな証明のハーリントンの定理（定から紹介する．この定理は，算術的（もしくは Π11 ）命題については，弱理 8.1.10）
ケーニヒの補題（あるいは，コンパクト性）を仮定して証明できれば，それなしにも証明できるというものである．この定理の保存命題を ∀X ∃!Y ϕ(X, Y )（ϕ は（定理 8.4.1）
である．また，少算術的論理式）の形に一般化したものが STY 定理
し異なるバリエーションとして，「WKL0 で証明できる Π2 命題は 1 階算術 PRAでも証明できる」というフリードマンの定理（定理 8.2.7）も証明する．
もう 1 つのメタ数学的論法は，WKL0 における超準解析の応用である．WKL0の任意のモデルは可算非 ω モデル（1 階部分が非標準）と初等同値になるので，可算非 ω モデルに対して 2 階部分での超準モデルが構成できれば，ある種の超準解析が可能になる．この超準モデルは「可算非 ω モデルは自分自身に同型な始切片をもつ」という自己埋め込み定理（定理 8.3.1）から導かれる．さらに，この超準的手法と STY 定理をドッキングさせることで，RCA0 における代数学の基
本定理の新しい証明が得られる．

8.1 強制法とハーリントンの定理
8.2 半正則切断とフリードマンの定理
8.3 WKL0 の自己埋め込み定理と超準的手法
8.4 STY 定理∀X ∃!Y ϕ(X, Y ) の保存性

8.5 代数学の基本定理と RCA0 における証明

第8章

284

2 階算術と超準的方法

8.1 強制法とハーリントンの定理
本節では，ハーリントンの定理「WKL0 は RCA0 の Π11 保存的拡大である」
を紹介する．公理的集合論の強制拡大の手法にならって，モデル内の無限木に対する無限道をジェネリック・パスとして加えていくアイデアは，ジョク
シュとソーア（文献 [70]）によって開発されたものだが，ハーリントンはそれを 2 階算術の非 ω モデルにうまく応用した．まず，強制法に馴染みのない方のために，その基本知識を説明しておこう．8.4 節とあわせて読んでいただくと，強制法入門の良い教材になると思う．
強制法の基本的な考え方は，現実世界にないものを世界の混乱を招かないようにして生産投入することである．まず，生成（ジェネレート）するものに対する条件の集合 P が与えられ，条件の間には半順序が定められている．この状況をどう解釈するかは応用によって異なるので，最初は意味を与えずに形式的に進める．
半順序集合 (P, <) を任意に固定し，p, q, r, . . . で P の元を表す．次の条件を満たす集合 G ⊆ P を開集合とよび，これによって (P, <) は位相空間となる．

∀p, q (q < p ∧ p ∈ G → q ∈ G).
いま，[p] = {q ∈ P | q ≤ p}とおくと，任意の開集合 G は p∈G [p] と一致するから，{[p] | p ∈ P} は開基
底を形成する．
任意の空でない開集合と（空でない）
交わりをもつ集合 D ⊆ P を稠密な集合という．D が稠密である条件は，∀p ∈ P [p] ∩ D = ∅,換言すると∀p ∈ P ∃d ∈ D d ≤ pと同値である．
定義 8.1.1

次の条件を満たす集合 F ⊆ P をフィルターとよぶ．

298

第8章

2 階算術と超準的方法できる．にも関わらず，フリードマンの定理によると，WKL0 は，Π2 文に関してヒルベルトの「有限の立場」に相当する形式体系 PRA と同じ定理をもつ．
とくに，無矛盾性は Π1 文で表せるため，両者は無矛盾性に関して同等となり，この事実は「ヒルベルトのプログラム」（第 7 章付録 B）
に関して重要な意義を有している．

第二不完全性定理のモデル論的証明
ここでは，フリードマンの定理を応用した第二不完全性定理のモデル論的証明を紹介しよう．まず，数理論理学に対する逆数学の基本結果を簡単に述べる．2 階算術の中で議論するので，言語 L も構造 A もとくに断らない限り
可算で，形式的にはゲーデル数のようなコード化の手法を用いて N の部分集合としてあつかうことになるが，ここではコード化の議論は省く．
モデルをあつかうためには，構造の上の充足関係 Sat（あるいは |=）が必要になる．これを通常通りタルスキの真理定義条項（定義 2.1.8）の下で論理式の構成による帰納法で定義するなら，ACA0 以上が必要である．そこで，逆数学においては，構造と同時にその上の充足関係もはじめから与えておき，それらがタルスキの真理定義条項を満たすときそのペアをモデルとよぶ．より簡明には，初等ダイヤグラム Th(AA ) を「モデル」と同一視すればよい．
定理 8.2.8

RCA0 において，以下は同値である．

(1) WKL0(2) 言語 L の無矛盾な理論 T はモデルをもつ．
(3) 言語 L の無矛盾な理論 T において，任意の文 ϕ に対して，
T ϕ

⇐⇒

T |= ϕ.

(4) 言語 L の理論 T において，T の任意の有限部分集合がモデルをもつならば，T 全体もモデルをもつ．