講義録

二階算術の部分体系のモデル
(09/02 改訂版)
山崎 武（東北大学理学研究科）
於：聖徳大学 2006.8.31- 9.02 数学基礎論サマースクール 2006
目次
1
2
ω-モデル
1.1 二階算術の言語 L2 .
1.2 L2 -構造 . . . . . . .
1.3 L2 -理論 . . . . . . .
1.4 論理式の階層 . . . .
1.5 ω-モデル上での解釈
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Π11 -CA0 と ACA0
2.1 体系の定義 . . . . . . . . . . .
2.2 ACA0 の ω-モデルの特徴付け (1)
2.3 ACA0 の ω-モデルの特徴付け (2)
2.4 Π11 -CA0 の β-モデルの特徴付け .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2
2
2
3
5
6
.
.
.
.
7
7
8
9
10
3
ω-部分モデル
13
3.1 体系 RCA0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.2 ω-部分モデル . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.3 可算披コード ω-モデル . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
4
ω-モデルの拡大
15
4.1 体系 WKL0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
4.2 WKL0 の ω-モデル . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
4.3 更なる結果 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5
補遺
19
5.1 体系 ATR0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
5.2 逆数学 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
1
1
1.1
ω-モデル
二階算術の言語 L2
全体を通して，自然数全体のなす集合 {0, 1, 2, . . .} を ω であらわす．P (ω) は ω の部
分集合全体のなす集合である．二階算術は ω と P (ω) の 2 種類の対象領域を扱うこと
を目論む形式体系である．このため，二階算術の言語 L2 は，普通の一階述語論理の
言語と異なり 2 種類の変数をもつ．対象領域 ω のための変数を一階の変数または数変
数といい，x, y, l, m, n, · · · など小文字のアルファベットであらわす．P (ω) のための変
数は二階の変数または集合変数といい，X, Y, Z, · · · など大文字のアルファベットであ
らわす．
L2 の項は数項と集合に関する項の 2 つがある．集合に関する項は集合変数だけであ
る．数項は，普通の一階述語論理の言語と同じようにして次の操作により帰納的に定
義される．
(1) 数変数と定数記号 0, 1 は数項である．
(2) もし t1 , t2 が数項ならば，(t1 + t2 ) と (t1 · t2 ) は数項である．
ここで，関数記号 +, · はそれぞれ通常の自然数の和・積に対応するものである．した
がって，自然な解釈において，数項は自然数係数の多変数多項式に対応すると考えて
よい．
t1 と t2 を数項，X を集合変数とするとき，t1 = t2 , t1 < t2 あるいは t1 ∈ X の形
の記号列を L2 の原子論理式という．原子論理式から一階述語論理と同じようにして，
命題論理結合子 ¬, ∧, ∨, →, ↔ と，数変数量化記号 ∀x, ∃x, 及び，集合変数量化記号
∀X, ∃X を適切に組み合わせてできる記号列を L2 の論理式という．以下では L2 の論
理式は単に論理式とよぶことにする．
論理式の中の変数の出現に対する自由・束縛の概念も一階述語論理と同じように定
める．自由変数のない論理式は文とよぶ．
以後，括弧の省略など普通に使われる用例にしたがい，数項や論理式は意味のとり
やすい形で表現し厳密な形で表記しないことにする．例えば，¬((1 + 1) + 1) ∈ X) は
3 6∈ X ，t < s ∨ t = s は t ≤ s，∀x(x ∈ X → x ∈ Y ) は X ⊆ Y という具合にあらわす．
Remark. ここで，L2 の等号記号 = は厳密には 2 つの数項間にのみ用いられるもので
あり，集合変数に関する表記 X = Y は論理式 ∀x(x ∈ X ↔ x ∈ Y ) の略にすぎない
ことに注意する．したがって，項の等式 t1 = t2 は原子論理式だが，集合に関する等式
X = Y は原子論理式ではない．
1.2
L2 -構造
言語 L2 の解釈は次のようになされる．
Definition 1.1 (L2 -構造) 次の 4 条件をみたす 7 つ組
M = (|M |, SM , 0M , 1M , +M , ·M , <M )
2
を L2 -構造または，L2 -モデルという．
(1) 0M , 1M ∈ |M | かつ φ 6= SM ⊆ P (|M |)．
(2) |M | ∩ SM = φ
(3) +M , ·M はともに |M | 上の 2 項演算．
(4) <M は M 上の 2 項関係をあらわす．
|M | は数変数のための領域をあらわし，SM は集合変数のための領域をあらわす．L2
に |M | ∪ SM の各要素に対応する新しい定数記号を加えた言語を L2 (M ) とする．L2 の
場合と同じようにして L2 (M ) の論理式も定めることができる．このとき，L2 の論理式
は L2 (M ) の論理式でもある．L2 (M ) の論理式のことを（M における）L2 のパラメー
タ付き論理式という．パラメータ付き論理式は L2 -構造 M において自然に解釈される．
パラメータ付き文 ϕ が M で真であることを M |= ϕ とあらわす．すると例えば，
M |= ϕ1 ∨ ϕ2 ⇔ (M |= ϕ1 または M |= ϕ2 ),
M |= ∃xϕ(x) ⇔ (M |= ϕ(a) となる a ∈ |M | が存在する),
M |= ∀Xϕ(X) ⇔ (任意の A ∈ SM に対して，
M |= ϕ(A))
等となる．ここで，a, A はそれぞれ a, A に対応する定数記号である．以降は ϕ(a) や
ϕ(A) などは単に ϕ(a), ϕ(A) とかく．
最も代表的な L2 -構造は (ω, P (ω), 0, 1, +, ·, <) である．ここで 0, 1, +, ·, < は自然数
上の通常の演算をあらわす．これを L2 の標準構造とよぶことにする．
L2 -構造 M = (|M |, SM , 0M , 1M , +M , ·M , <M ) から SM をのぞいた
(|M |, 0M , 1M , +M , ·M , <M )
を M の一階部分という1 ．L2 -構造は集合変数のための領域をもつので，1 階部分が
(ω, 0, 1, +, ·, <) であっても，標準構造であるとは限らない．
Definition 1.2 (ω-モデル) 1 階部分が (ω, 0, 1, +, ·, <) である L2 -構造 (ω, S, 0, 1, +, ·, <
) を ω-モデルという．ω-モデル (ω, S, 0, 1, +, ·, <) は二階部分 S によって定まるので，
単に S であらわすこともある．
標準構造 P (ω) において真である文，すなわち P (ω) |= ϕ である文 ϕ は，真な文という．
1.3
L2 -理論
L2 の形式体系（L2 -理論）T は L2 の文の集合によって定めることができる．この集
合もまた T とあらわす．T に属する文を T の公理という．それらから通常の述語論理
の推論規則や公理を用いて導かれる文を T の定理という2 ．ここで，等号 = に関する
1
標準構造の 1 階部分は (1 階) ペアノ算術 PA の標準モデルである．
通常の一階述語論理と異なり我々は２種類の変数を持つ理論を扱うわけだが，実際には一階述語論
理の枠内で取り扱うことができる．つまり，数変数と集合変数のかわりに，数の範囲を特定するための
関係記号 N (x) と集合の範囲を特定するための関係記号 S(x) を導入することで，L2 -理論 T に対応す
る一階述語論理の理論 T0 を考えることができる．
2
3
公理は仮定しておく．文 ϕ が T の定理であるとき，T ` ϕ とかき，T で ϕ が証明でき
るという．また，L2 の形式体系 T1 と T2 に対して，T1 のすべての公理が T2 の定理と
なるとき，T1 は T2 の部分体系という．
L2 の形式体系 T の公理すべてが真である L2 -構造を T のモデルという．
Theorem 1.1 (L2 -理論における完全性定理) T を L2 の形式体系とする．このとき，
任意の L2 の文 ϕ について，
T ` ϕ ⇔ T の任意のモデル M で M |= ϕ
となる．
ここで我々の扱う形式体系は次の L2 -理論 Z2 の部分体系のみである．
Definition 1.3 二階算術 Z2 は次の３種類の公理からなる L2 の形式体系である．
(1) 自然数の順序 < や演算 +, · に関する基本公理 : n+1 6= 0, n+1 = m+1 → n = m,
n + 0 = n, n + (m + 1) = (n + m) + 1, n · 0 = 0, n · (m + 1) = (n · m) + n, ¬(n < 0),
n < m + 1 ↔ (m < n ∨ n = m)
(2) 帰納法公理：(0 ∈ X ∧ ∀n(n ∈ X → n + 1 ∈ X)) → ∀n(n ∈ X)
(3) 集合内包公理3 ：∃X∀n(n ∈ X ↔ ϕ(n)), ただし ϕ(n) は X を自由変数にもたない
論理式である．
ここでは公理を論理式の形であらわしているが，それはその論理式の先頭に全称量化
記号をつけて文にしたものをあらわす．以降，形式体系の公理を具体的にあらわす場
合，同じように全称量化記号を省略し論理式の形であらわすことがある．
Z2 はヒルベルトとベルナイスによって最初に紹介された．彼らはその著書 [7] の補
遺において通常の数学の一部がどのように Z2 で展開されうるかについて概説してい
る．ある意味で，Z2 は数学の展開する体系として十分大きいと考えてよい．
ここで特に注目したいのは (3) の集合内包公理である．以下で扱う L2 -理論は主にこ
の内包公理を制限することによって与えられる．論理式 ϕ(n) に対する内包公理は，直
観的には，ϕ(n) によって定義される集合 X = {n | ϕ(n)} の存在を保証するものであ
る．ϕ(n) は X 以外の自由変数を持つ場合がある．この場合，その自由変数は任意の
パラメータとして扱われている．例えば，ϕ(n) を n 6∈ Y という論理式とすると，内
包公理
∃X∀n(n ∈ X ↔ n ∈
/ Y ).
は，与えられた任意の集合 Y に対して，その補集合 X が存在することを主張して
いる．つまり，変数 Y はパラメータの役割を果たしている．より正確には次である．
ϕ(x, y1 , . . . , yn , Y1 , . . . , Ym ) を x, y1 , . . . , yn , Y1 , . . . , Ym 以外の自由変数をもたない L2 -論
3
集合内包公理は正確には「公理」ではなく公理図式であり，各論理式 ϕ ごとに 1 つ定まる無限個の
公理をあらわしている．以下，このような意味で，本来なら公理図式というべきところを慣例にならい，
ただ公理という．
4
理式とする．このとき，ϕ についての内包公理が L2 -構造 M で真になるのは，任意の
b1 , . . . bn ∈ |M |, A1 , . . . , Am ∈ SM に対し，
{a ∈ |M | : M |= ϕ(a, b1 , . . . , bn , A1 , . . . , Am )} ∈ SM
となるときである．つまり，L2 -構造 M が (3) の集合内包公理をみたすのは，
（パラメー
タを用いて）M 上定義可能なすべての集合が SM に属するときである．
ω-モデル P (ω) は集合内包公理をみたす．また，基本公理と帰納法公理は任意の ωモデルで真であるから，P (ω) は Z2 のモデルである．
(2) は集合に関する帰納法しか認めていないが，集合内包公理により定義可能な集
合はすべてその存在が保証されるので，Z2 から，全帰納法（full-induction）公理：任
意の論理式 ϕ(n) に対して，
ϕ(0) ∧ ∀n(ϕ(n) → ϕ(n + 1) → ∀nϕ(n).
が導かれる．自由変数にも束縛変数にも集合変数のない L2 -論理式は 1 階ペアノ算術
PA の言語 L1 の論理式とみなせる．したがって，基本公理と全帰納法公理により，PA
は Z2 の部分体系であるといえる．実際には L2 の表現力は L1 よりはるかに豊かであ
り，Z2 で PA の無矛盾性も証明できる．
1.4
論理式の階層
Definition 1.4 (1) 集合変数に関する量化記号を含まない論理式を算術的論理式とい
う．算術的論理式は，Π10 -論理式または Σ10 -論理式ともいう．また，算術的論理式全体
の集合を Π10 もしくは Σ10 とあらわす．
(2) 任意の自然数 k ∈ ω に対し，次の形の論理式を Π1k -論理式という：
∀X1 ∃X2 · · · Xk θ
ただし，θ は算術的論理式, X1 , X2 , . . . , Xk は集合変数．また，Π1k -論理式全体の集合
を Π1k とあらわす．
(3) 任意の自然数 k ∈ ω に対し，次の形の論理式を Σ1k -論理式という：
∃X1 ∀X2 · · · Xk θ
ただし，θ は算術的論理式, X1 , X2 , . . . , Xk は集合変数．Σ1k -論理式全体の集合を Σ1k と
あらわす．
ここで (2) と (3) の定義にあらわれる式はともに集合変数に関する量化記号として ∃
と ∀ が交互にあわせて k 回あらわれる形である．パラメータ付き論理式に対しても同
様に定める．
¬∀Xϕ ↔ ∃X¬ϕ，¬∃Xϕ ↔ ∀X¬ϕ, ϕ ↔ ¬¬ϕ より，任意の Π1k -論理式はある Σ1k -論
理式の否定に，また任意の Σ1k -論理式はある Π1k -論理式の否定に論理的に同値である．
また，無意味な量化記号の付け足しにより，任意の k ∈ ω について，
Σ1k ∪ Π1k ⊆ Σ1k+1 ∩ Π1k+1
がわかる．
5
Definition 1.5 (1) 論理式 ϕ と数変数 n，n を含まない数項 t に対して，∀n(n < t → ϕ)
の形の論理式を (∀n < t)ϕ，∃n(n < t ∧ ϕ) の形の論理式を (∃n < t)ϕ とあらわす．
(∀n ≤ t), (∃n ≤ t) も同様に定める．この (∀n < t)，(∃n < t), (∀n ≤ t), (∃n ≤ t) を有
界量化記号という．
(2) 量化記号がすべて有界量化記号の形でしかあらわれない算術的論理式を有界論理
式という．有界論理式は Π00 -論理式または Σ00 -論理式ともいう．有界論理式全体の集合
は単に Π00 もしくは Σ00 とかく．
(3) 任意の k ∈ ω に対し，次の形の算術的論理式を Π0k -論理式という：
∀x1 ∃x2 · · · xk θ
ただし，θ は有界論理式, x1 , x2 , . . . , xk は数変数．また，Π0k -論理式全体の集合は Π0k と
あらわす．
(4) 任意の k ∈ ω に対し，次の形の算術的論理式を Σ0k -論理式という：
∃x1 ∀x2 · · · xk θ
ただし，θ は有界論理式, x1 , x2 , . . . , xk は数変数．また，Σ0k -論理式全体の集合は Σ0k と
あらわす．
ここで (3) と (4) の定義にあらわれる式はともに数変数の量化記号として ∃ と ∀ が交互
にあわせて k 回あらわれる形である．
1.5
ω-モデル上での解釈
Definition 1.6 (ω-モデル上の定義可能性) 4
(1) S を ω-モデルとし，ϕ(x) を自由変数が x のみしかない論理式とする．集合 A ⊆ ω
が
A = {n ∈ ω | S |= ϕ(n)}
となるとき，A は S 上定義可能であるという．とくに P (ω) 上定義可能なときは，た
んに定義可能という．パラメータ付き論理式についても同様に定義する．
(2) k ∈ ω とする．集合 A ⊆ ω は，B1 , . . . , Bm だけをパラメータにもつパラメータ付き
Π1k -論理式を用いて定義可能であるとき，Π1k (B1 , . . . , Bm ) であるという．Σ1k (B1 , . . . , Bm ),
Π0k (B1 , . . . , Bm ), Σ0k (B1 , . . . , Bm ) 等についても同様に定義する．とくに，Π1k (φ)，Σ1k (φ),
. . . らを単に Π1k ，Σ1k , . . . とも書く．
ϕ が算術的文ならば，任意の ω-モデル S に対して，
S |= ϕ ⇔ P (ω) |= ϕ
である．したがって，集合 A ⊆ ω が，算術的論理式 ϕ を用いて，定義可能であるこ
と，すなわち P (ω) 上で定義可能であることと，S 上で定義可能であることは同じで
4
以下のような前節の論理式の階層による標準構造上の解釈は，再帰理論における解析的階層および
算術的階層と対応している．
6
ある．これはパラメータを含む場合もかわらない．例えば，ϕ を A1 , . . . Am ⊆ ω のみ
をパラメータにもつ算術的文であるとき，A1 , . . . Am を要素にもつ任意の ω-モデル S
に対して，
S |= ϕ ⇔ P (ω) |= ϕ
である．ところが，ϕ が Π11 文であるときは，このようなことは必ずしも成り立たな
い．なぜならば，ϕ が算術的論理式 θ(X) を用いて ∀Xθ(X) とあらわせているとする
と，ω-モデル S の解釈では，
S |= ∀Xθ(X) ⇔ 任意の A ∈ S に対して S |= θ(A).
であるからである．このように，算術的でない文に関しては標準構造と ω-モデルで真
偽が異なる場合がある．Π11 文に関しては標準構造と真偽の変わらない ω-モデルを，特
に β-モデルという．
Definition 1.7 ω-モデル S は，任意の (S のパラメータ付きの ) Π11 -文 ϕ に対して，
S |= ϕ ⇔ P (ω) |= ϕ
となるとき β-モデルという．形式体系 T のモデルとなる β-モデルは，T の β-モデル
という．
Π11-CA0 と ACA0
2
2.1
体系の定義
Definition 2.1 (Γ-内包公理) Γ を論理式の集合とする．次の制限された集合内包公
理を Γ-内包公理という：∃X∀n(n ∈ X ↔ ϕ(n))，ただし ϕ(n) は X を自由変数にもた
ない Γ に属する論理式である．
Definition 2.2 k ∈ ω とする．形式体系 Π1k -CA0 は次の３種類の公理からなる5 ．
(1) 基本公理. Definition 1.3 (1) と同じもの．(2) 帰納法公理. (3) Π1k -内包公理.
任意の k ∈ ω について，Π1k ⊂ Π1k+1 であるから Π1k -CA0 ⊆ Π1k+1 -CA0 である．実際，
Π1k+1 -CA0 は Πk1 -CA0 より真に強い，つまり証明できる定理が真に多い．同様に Σ1k -CA0
を定めることができるが，補集合の存在を保証する先述の内包公理 ∃X∀n(n ∈ X ↔
n∈
/ Y ) を用いて，Π1k -CA0 と等しいことが容易にわかる．つまり両者で証明できる定
理は同じである．
∪
Π1∞ = k∈ω Π1k とする．簡単な式変形によって，各論理式は Π1∞ に属するある論理
式と論理的に同値となる．よって， Z2 の集合内包公理は Π1∞ -内包公理におきかえて
もよい．Z2 を Π1∞ -CA0 とあらわすこともある．
5
「Π1k -CA0 」の CA は内包公理 (comprehension axiom) の略であり，下付きの 0 は帰納法の制限を
あらわす．つまり，内包公理の制限から Π1k -CA0 では Π1k -論理式に関する帰納法は証明できるが，全帰
納法は証明できない．
7
Definition 2.3 Π10 -CA0 を特に ACA0 という．
ACA は算術的内包公理 (arithmetical comprehension axiom) の略である．先述した
ように，古典的数学6 の大部分は二階算術 Z2 で展開されることがわかっている．この
ような通常の数学の展開という観点からは，いくつかの重要な例外はあるものの，実
際には Π11 -CA0 ひいては ACA0 でも十分な強さをもつ体系であるといえる．この辺りの
事情は [10], [13] に詳しいので，興味のある方は参照して欲しい．
2.2
ACA0 の ω-モデルの特徴付け (1)
Lemma 2.1 S を ω-モデルとする．このとき，
S 0 = {A ⊆ ω : A は S 上で，パラメータ付きの算術的論理式を用いて定義可能 }
は，S を含む ACA0 の ( 包含関係に関して ) 最小の ω-モデルである．
Proof. まず，S 0 が ACA0 の ω-モデルであることを示す．S 0 が基本公理と帰納法公理
をみたすことは明らかなので，Π10 -内包公理をみたすことを示す．
ϕ(x, Y1 , . . . , Ym ) を x, Y1 , . . . , Ym 以外の自由変数をもたない算術的論理式とし，B1 , . . . ,
Bm ∈ S 0 とする7 ．各 Bi は S 上のあるパラメータ付き算術的論理式 ϕi (x) で定義され
ている8 ．そこで ϕ0 (x) を，ϕ の中のすべての t ∈ Yi の形の部分論理式を ϕi (t) でおきか
えて得られる S 上のパラメータ付き論理式とする．ϕ0 の作り方から ϕ0 (x) は集合変数
に関する量化記号をもたない．したがって，ϕ0 もまた S 上のパラメータ付き算術的論
理式である．よって，S ⊆ S 0 であるから，(Definition1.6 と 1.7 の間の説明より)
{n ∈ ω : S 0 |= ϕ0 (n)} = {n ∈ ω : S |= ϕ0 (n)} ∈ S 0
となる．つまり S 0 |= ∃X∀x(x ∈ X ↔ ϕ0 (x)) である．更に，S 0 |= ∀x(ϕ(x) ↔ ϕ0 (x))
であるから，S 0 |= ∃X∀x(x ∈ X ↔ ϕ(x)) となる．以上により S 0 は Π10 -内包公理をみ
たす．
次に最小性を示す．S 00 を S ⊆ S 00 となる ACA0 の ω-モデルとする．A ∈ S 0 を任意に
とる．このとき，A は，S の要素のみをパラメータにもつあるパラメータ付き算術的
論理式 ϕ(x) で定義されている．S 00 は ACA0 のモデルなので，
A = {n ∈ ω : S |= ϕ(n)} = {n ∈ ω : S 00 |= ϕ(n)} ∈ S 00
となる．以上より，S 0 ⊆ S 00 が示せた．よって，S 0 の最小性がいえる．2
特に S = {φ} について考えることで Lemma 2.1 から次が得られる．
Corollary 2.2 Π10 集合全体 ARITH = {A ⊂ ω | A は Π10 } は，ACA0 の最小の ω-モデ
ルである．
6
数学の分野全体を大雑把にとらえて，集合論的な領域と非集合的な領域に分けたときに，非集合論
的な領域を古典的数学ということにする．それは，幾何や数論，微分方程式，実解析，複素解析，代数，
または，組合わせ論，数理論理学，計算論など多岐の分野にわたるものである．具体的にはこの節で述
べられているものから想像してほしい．
7
我々は ω-モデルについて考えているので数に関するパラメータは気にしなくてよい．
8
実際には S 上で定義されているわけだが，算術的論理式であるので P (ω) 上で定義されていると考
えてよい．
8
2.3
ACA0 の ω-モデルの特徴付け (2)
以上の特徴付けを更に明確にするために，再帰理論 (recursion theory) からいくつか
の結果を利用する．
Definition 2.4 (相対的計算可能性) 9 集合 A ⊆ ω は，B ⊆ ω をオラクルに用いた
チューリング・マシンで計算可能であるとき，B-計算可能，もしくは，B-再帰的 (Brecursive) といい，A ≤T B とあらわす．
Theorem 2.3 (Post) 任意の集合 A, B ⊆ ω に対して，A が，B-計算可能であること
と，Σ01 (B) かつ Π01 (B) であることは同値である．
Theorem 2.4 B ⊆ ω とする．このとき，次をみたす Σ01 (B) 集合 K が存在する：任
意の Σ01 (B) 集合 A に対して，ある e ∈ ω が存在して，
∀n ∈ ω(n ∈ A ⇔ he, ni ∈ K).
ただし，ここで，he, ni = (e + n + 1)(e + n)/2 + e である．各 B に対するこのような
K を，B T とかく10 ．
A, B ⊆ ω に対し，
A ⊕ B = {2n : n ∈ A} ∪ {2n + 1 : n ∈ B}
とさだめる．このとき，
Theorem 2.5 A, B, C ⊆ ω とする．A が，Σ01 (B, C) であることと Σ01 (B ⊕ C) である
ことは同値である．
Theorem 2.6 S を ω-モデルとする．このとき，S が ACA0 のモデルであることと，S
が次の 3 条件をみたすことは同値である．
(1) 任意の A, B ∈ S に対して，A ⊕ B ∈ S である．
(2) 任意の A ≤T B, B ∈ S に対して，A ∈ S である．
(3) 任意の A ∈ S に対して，AT ∈ S である．
Proof. S が ACA0 のモデルならば，上の 3 条件をみたすのは明らかである．よって逆
を示す．ω-モデル S は上の 3 条件をみたしているとする．このとき，Π10 -内包公理をみ
たすことを示せばよい．
そこで，主張「S は Σ0k -内包公理をみたす」を k に関する数学的帰納法11 で示す. k = 1
のときは，Theorem 2.3 から 2.5 の主張と上の 3 条件より明らか．次に k で成り立つと
して，k + 1 で成り立つことを示す．
9
再帰理論の大概の教科書には述べられているので，正確な定義はそちらを参照のこと．
再帰理論では，B T は B 0 とかくのが普通であるが他の使用との混乱を防ぐためにここではこれを
用いる．
11
この「帰納法」はメタ理論における帰納法で，形式体系内の帰納法ではないことに注意する．
10
9
ϕ(x) を x のみを自由変数にもつ S 上のパラメータ付き Σ0k+1 -論理式とする．このと
き，ある Σ0k -論理式 θ(m, n) を使って，ϕ(n) ↔ ∃m¬θ(m, n) とあらわせる．帰納法の
仮定から，B = {hm, ni | S |= θ(m, n)} は S に属する．よって，条件 (2), (3) より，
A = {n ∈ ω | ∃mhm, ni 6∈ B}
も S に属し，明らかに，S |= ∀n(n ∈ A ↔ ϕ(n)) である．
以上より，S は Σ0k+1 -内包公理をみたすことがわかった．2
A ⊆ ω に対して，A(0)T = A, A(1)T = AT , . . ., A(n+1)T = (A(n)T )T , . . . とする．
Corollary 2.2 と Theorem 2.6 から，ARITH = {A ⊆ ω | ∃n ∈ ω(A ≤T φ(n)T )} である．
各 A ⊆ ω, n ∈ ω に対して，An = {m ∈ ω | hn, mi ∈ A} とする．また，任意の自然数
m に対し， lim XAn (m) が存在するとき，A(もしくは，hAn | n ∈ ωi) は極限をもつと
n→∞
いい，XB (m) = lim XAn (m) によって定まる集合 B を A(もしくは，hAn | n ∈ ωi) の
n→∞
極限という．ここで，XY は Y の特性関数である．
Lemma 2.7 (極限補題) A, B ⊆ ω とする．このとき，A ≤T B T であることと，A が
ある B-計算可能な集合の極限になることは同値である．
Theorem 2.8 S を ω-モデルとする．このとき，S が ACA0 のモデルであることと，S
が次の 3 条件をみたすことは同値である．
(1) 任意の A, B ∈ S に対して，A ⊕ B ∈ S である．
(2) 任意の A ≤T B, B ∈ S に対して，A ∈ S である．
(3) 任意の A ∈ S に対して，A が極限 B をもつならば，B ∈ S である．
Proof. Theorem 2.6 と Lemma 2.7 よりわかる．2
2.4
Π11 -CA0 の β-モデルの特徴付け
次の定理から Π11 -CA0 に最小の ω-モデルが存在しないことがわかる．
Theorem 2.9 (Quinsey) [9] 自然数 k > 0 をとる．S を Π1k -CA0 の ω-モデルとする．
このとき，S 0 ( S となる Π1k -CA0 のモデル S 0 が存在する．
このように，Π10 集合全体 ARITH は明らかに Π11 -CA0 のモデルではない．Π11 -CA0 の ωモデルの特徴付けが，ACA0 の時のようにうまくいかないわけは，ω-モデル S と標準
構造とでは，Π11 文に関する真偽が異なる場合があるからである．
Theorem 2.10 B ⊆ ω とする．このとき，次をみたす Σ11 (B) 集合 T が存在する：任
意の Σ11 (B) 集合 A に対して，ある e ∈ ω が存在して，
∀n ∈ ω(n ∈ A ⇔ he, ni ∈ T ).
各 B に対するこのような T を，B H とかく．
10
Theorem 2.11 (クリーネの基底定理) [8] ϕ(Y, X) は，Y, X のみを自由変数にもつ Σ11 論理式とする．このとき，B ⊆ ω に対し，∃Y ϕ(Y, B) が真ならば，ある A ≤T B H で
ϕ(A, B) が真となる．
Proof. ϕ(Y, X) を Y, X のみを自由変数にもつ Σ11 -論理式とする．このとき，ϕ はある
Σ11 -論理式 θ(m, X) によって，∀nθ(Y [n], X) とあらわせる12 ．
いま，B ⊆ ω に対し，∃Y ϕ(Y, B) が真であるとする．このとき，
C = {σ ∈ 2<ω | ∃Y (∀nθ(Y [n], B) ∧ Y [lh(σ)] = σ)} ≤T B H
である．ここで，A ⊆ ω を C を用いて再帰的に，n ∈ A ⇔ A[n]_ h1i ∈ C で定める．
すると，A ≤T C より A ≤T B H であり，ϕ(A, B) は真となる．2
Theorem 2.12 S を ω-モデルとする．このとき，S が Π11 -CA0 の β-モデルであること
と，S が次の 3 条件をみたすことは同値である．
(1) 任意の A, B ∈ S に対して，A ⊕ B ∈ S である．
(2) 任意の A ≤T B, B ∈ S に対して，A ∈ S である．
(3) 任意の A ∈ S に対して，AH ∈ S である．
Proof. S が Π11 -CA0 の β-モデルならば，上の 3 条件をみたすのは明らかである．よっ
て逆を示す．ω-モデル S は上の 3 条件をみたしているとする．
まず，S が β-モデルであることを示す．ϕ をパラメータ付き Σ11 -文とする．このと
き，条件 (1) から，ϕ のパラメータは集合パラメータただ一つと考えてよい．これを B
とする．したがって，ϕ は，B のみをパラメータにもつある算術的論理式 θ(Y, B) を用
いて ∃Y θ(Y, B) とあらわされている．一方，条件 (2), (3) により，任意の A ≤T B H に
対して A ∈ S である．これとクリーネの基底定理から，
S |= ∃Y θ(Y, B) ⇒ P (ω) |= ∃Y ϕ(Y, B) ⇒ P (ω) |= ∃Y ≤T B H ϕ(Y, B) ⇒ S |= ∃Y ϕ(Y, B).
したがって，P (ω) |= ∃Y ϕ(Y, B) ⇔ S |= ∃Y ϕ(Y, B). よって，S は β-モデルである．
次に S が Π11 -内包公理をみたすことを示す．条件 (2) により S は補集合に関して閉
じているので，Σ11 -内包公理をみたすことを示せばよい．ϕ(x) を x のみを自由変数に
もつパラメータ付き Σ11 -論理式とする．このとき，ϕ(x) のパラメータは集合パラメー
タただ一つと考えてよい．これを再び B とする．S は β-モデルであるから，
A = {n ∈ ω | S |= ϕ(n)} = {n ∈ ω | P (ω) |= ϕ(n)} ≤T B H
である．よって．条件 (2), (3) より，A ∈ S となる．以上より S は Σ11 -内包公理をみ
たす．2
A ⊆ ω に対して，A(0)H = A, A(1)H = AH , . . ., A(n+1)H = (A(n)H )H , . . . とする．
クリーネの標準化定理を考えよ．Y [n] は hXY (0), . . . , XY (n − 1)i のことである．ここでは，より
厳密にはそのゲーデル数のことである．また，下の 2<ω は 0-1 の有限列（のゲーデル数）全体のなす集
合をさす．
12
11
Corollary 2.13
{A ⊆ ω | ∃n ∈ ω(A ≤T φ(n)H )}
は Π11 -CA0 の最小の β-モデルとなる13 ．
なんらかの Π02 -論理式 θ を用いて，∃Xθ の形であらわせる論理式を Σ1,w
1 -論理式とい
う．ただし X は集合変数である．
Definition 2.5 S を ω-モデルとする．
(1) 集合 A ⊆ ω は，B1 , . . . , Bm だけをパラメータにもつパラメータ付き Σ11 -論理式を
用いて S 上定義可能であるとき，Σ11 (B1 , . . . , Bm ; S) であるという．
(2) 集合 A ⊆ ω は，B1 , . . . , Bm だけをパラメータにもつパラメータ付き Σ1,w
1 -論理式
を用いて S 上定義可能であるとき，Σ1,w
1 (B1 , . . . , Bm ; S) であるという．
H
(3) B ∈ S とする．このとき，次をみたす Σ1,w
1 (B; S) 集合 T を BS とかく：任意の
Σ1,w
1 (B; S) 集合 A に対して，ある e ∈ ω が存在して，
∀n ∈ ω(n ∈ A ↔ he, ni ∈ T ).
は真である．
Theorem2.12 中の条件 (1), (2) をみたす任意の ω-モデル S と B ∈ S に対して，BSH
は存在する14 ．
Lemma 2.14 S を ACA0 の ω-モデルとし，B ∈ S とする．このとき，任意の Π11 (B; S)
集合 A に対して, A ≤T BSH である．
Theorem 2.15 S を ω-モデルとする．このとき，S が Π11 -CA0 の ω-モデルであること
と，S が次の 3 条件をみたすことは同値である．
(1) 任意の A, B ∈ S に対して，A ⊕ B ∈ S である．
(2) 任意の A ≤T B, B ∈ S に対して，A ∈ S である．
(3) 任意の A ∈ S に対して，AH
S ∈ S である．
Proof. S が Π11 -CA0 の ω-モデルならば，上の 3 条件をみたすのは明らかである．Theorem 2.6 より，上の 3 条件をみたす ω-モデル S は ACA0 のモデルである．このとき更
に，Lemma 2.12 と同じようにして，S が Σ11 -内包公理をみたすことも明らか．2
∩
{A ⊆ ω | ∃n ∈ ω(A ≤T φ(n)H )} = Lα P (ω) ( ∆12 である．ここで，α = sup{βn | n ∈ ω} であ
り，βn は n 番目の許容的順序数 (admissible ordinal) である．また．一般に，任意の 1 ≤ k ≤ ∞ に対
し，Π1k -CA0 はそれぞれ最小の β-モデルをもつ．
14
ただし，S に属するとは限らない．
13
12
3
3.1
ω-部分モデル
体系 RCA0
Definition 3.1 (1) 次の帰納法公理を Σ01 -帰納法という：任意の Σ01 -論理式 ϕ(n) に対し，
ϕ(0) ∧ ∀n(ϕ(n) → ϕ(n + 1)) → ∀nϕ(n).
(2) 次の制限された集合内包公理を ∆01 -内包公理，もしくは再帰的内包公理という：X
を自由変数にもたない任意の Σ01 -論理式 ϕ(n) と ψ(n) に対し，
∀n(ϕ(n) ↔ ¬ψ(n)) → ∃X∀n(n ∈ X ↔ ϕ(n)).
Definition 3.2 RCA0 は次の３種類の公理からなる15 ．
(1) 基本公理. (2) Σ01 -帰納法16 ．(3) ∆01 -内包公理.
Theorem 2.3, 2.4 にしたがえば，RCA0 の ω-モデルは次のように特徴づけられる．
Lemma 3.1 S を ω-モデルとする．このとき，S が RCA0 のモデルであることと，S
が次の 2 条件をみたすことは同値である．
(1) 任意の A, B ∈ S に対して，A ⊕ B ∈ S である．
(2) 任意の A ≤T B, B ∈ S に対して，A ∈ S である．
Corollary 3.2 計算可能集合全体 REC = {A ⊆ ω|A ≤T φ} は RCA0 の最小の ω-モデ
ルである17 ．
RCA0 は自然数に関する素朴な事実を証明するには十分な強さをもつ体系である．例
えば．順序 < の線形性，和や積の可換性や順序の保存性などの基本的な性質, 関数の
合成，再帰理論に関する基本定理などである．本講演では，そのあたりのことは厳密
に扱うことはしないが，暗黙のうちにこれらの事実を利用する．興味のある方は，[10]
などを参照されたい．
3.2
ω-部分モデル
Definition 3.3 (ω-部分モデル) (1) L2 -構造 M , M 0 は，一階部分が同じで SM ⊆ SM 0
であるとき，M は M 0 の ω-部分モデルといい，M ⊆ω M 0 とあらわす．
(2) M ⊆ω M 0 とする．M の任意のパラメータ付き Σ11 文 ϕ に対して，M |= ϕ ⇔ M 0 |= ϕ
となるとき，M は M 0 の β-部分モデルといい，M ⊆β M 0 とあらわす．
15
RCA はこの体系を特徴づける集合存在公理である再帰的内包公理（recursive comprehension axiom）
の略である．
16
RCA0 には帰納法公理 (Definition1.3 (2)) ではなく Σ10 -帰納法が公理として含まれていることに注
意する．RCA0 において Σ01 -帰納法をもとの帰納法公理におきかえると，RCA0 より真に弱い体系にな
り，以下で必要な素朴な結果さえ示すことができない場合がある．歴史的な背景として，数学的帰納法
を制限した体系をフリードマン [3] が最初に導入したとき，彼は集合変数ではなく関数変数をもつ言語
を使って定義した．また，基本公理として原始再帰法や µ-演算に対応する公理をふくめている．そのた
め，対応する体系を現在風に改めるには RCA0 の場合 Σ01 -帰納法が必要になる．
17 T
φ 6∈ REC なので REC は ACA0 のモデルではない．
13
上の定義では L2 -構造の一階部分に対する制限はない．したがって，ω-部分モデル
は必ずしも ω-モデルとは限らない．ω-モデルと β-モデルはそれぞれ，標準構造の ω部分モデル．β-部分モデルということである．前節や 2.3 節，2.4 節で述べられたこと
は，ω-部分モデルについて拡張したものにできる．特に，Theorem 2.12 を拡張したも
のは次のようになる．
Lemma 3.3 M 0 |= Π11 -CA0 とし，M ⊆ω M 0 とする．このとき，次の 2 条件は同値で
ある．
(1) M ⊆β M 0 かつ M |= Π11 -CA0
(2) M |= RCA0 かつ, 任意の X ∈ SM に対して，M 0 の解釈における「XSH 」は SM に
属する18 ．
Corollary 3.4 Π11 -CA0 の任意のモデルは，最小の β-部分モデルをもつ．
3.3
可算披コード ω-モデル
（RCA0 などの）形式体系の枠内で定める形式的な自然数全体の集合を N とあらわす19 ．
Definition 3.4 (可算披コード ω-モデル) RCA0 で次が定義できる．W ⊆ N を可算披
コード ω-モデルという．このとき，W は，
M = (N, {Wn | n ∈ N}, 0, 1, +, ·, <)
という L2 -構造のコードしたものとみなされる．M のパラメータ付き文の（ゲーデル
数の）全体の集合を SntM とする．各 ϕ ∈ SntM に対し，Sub(ϕ) を，ϕ の部分論理式
に適当な代入をすることで得られる文 ψ ∈ SntM 全体の集合とする．このとき，ϕ の
付置 f : Sub(ϕ) → {0, 1} は次のタルスキの充足条件をみたすものである：
(1) f (t1 = t2 ) = 1 ↔ t1 = t2 ,
(2) f (¬ψ) = 1 − f (ψ),
(3) f (∀nψ(n)) = 1 ↔ (∀m ∈ N f (ψ(m)) = 1),
(4) f (∀Xψ(X)) = 1 ↔ (∀m ∈ N f (ψ(Wm )) = 1) など．
ϕ に対する付置 f に対し，f (ϕ) = 1 となるとき，W |= ϕ とかく．
Lemma 3.5 ϕ を L2 の文とする．ACA0 で次が示せる．任意の可算披コード ω-モデル
W に対し，ϕ の付置がただ一つ存在する．
Theorem 3.6 Π11 -CA0 で次が示せる20 ．任意の X ⊆ N に対し，X ∈ W かつ ACA0 の
モデルとなる可算披コード ω-モデル W が存在する21 ．
X H = XPH(ω) であり，M 0 = P (ω) のときが，Theorem 2.12 である．
N は ∀n(n ∈ X) となるただ一つの集合で，論理式 x = x に対する内包公理により，RCA0 より強い
体系ではその存在が示されるものである．N は自然数全体の集合 ω と区別されなくてはならない．RCA0
のモデル M において，N の M における解釈 NM は |M | である．つまり，NM は M の 1 階の領域を
あらわす．ω は ω-モデルにおける N の解釈であるが，ω-モデルでない場合，N の解釈は ω と異なる．
20
実際は，それより弱い ACA0 + で示せる．
21
すなわち，∃nX = Wn かつ，ACA0 の任意の公理 ϕ に対して，W |= ϕ となる W が存在するとい
うこと．
18
19
14
Proof.(アイデア) Π11 -CA0 で考える22 . X ⊆ N とする．このとき，hX (n)T | n ∈ Ni が
存在する．ここで, （オラクル付きの）計算可能集合の index を利用して，W = {Y ⊆
ω | ∃n ∈ N(Y ≤T X (n)T )} を考えればよい．2
Corollary 3.7 Π11 -CA0 で，ACA0 の無矛盾性が示せる23 ．
4
4.1
ω-モデルの拡大
体系 WKL0
RCA0 において次が定義できる．有限列（のコード）全体の集合を N<N とあらわす．
σ ∈ N<N に対し，σ の「長さ」を lh(σ) とあらわし，
「σ の i 番目の値」は σ(i) とあらわす．
σ が τ の始切片 (initial segment) すなわち，lh(σ) ≤ lh(τ ) かつ (∀i < lh(σ))(σ(i) = τ (i))
であることを σ ⊆ τ とかく．また，0 または 1 だけを値にとる有限列（のコード）全体
の集合を 2<N とする．
Definition 4.1 (ケーニッヒの補題) RCA0 において次が定義できる．T ⊆ N<N は，そ
の各要素のすべての始切片が再び T の要素となるとき，すなわち ∀σ ∈ T (∀τ ⊆ σ)(σ ∈
T ) であるとき，木 (tree) という．木 T に対して，関数 f : N → N は ∀n(f [n] ∈ T ) とな
るとき，すなわち T に沿った枝別れのない無限道をあらわすとき，単に T の道 (path)
という．ここで，f [n] = hf (0), . . . , f (n − 1)i である．2<N の部分集合となる木を 0-1
木という．
「有限枝分かれの無限木は必ず道をもつ」という主張をケーニッヒの補題と
いい，
「無限 0-1 木は必ず道をもつ」という主張を弱ケーニッヒの補題という．
Definition 4.2 RCA0 に弱ケーニヒの補題を加えた体系 WKL0 という24 ．
RCA0 にケーニッヒの補題を加えた体系は ACA0 と同じであることが知られている．
したがって，WKL0 は，RCA0 と ACA0 の中間に位置する体系である．WKL0 は数学を
展開する上でも非常に豊かな体系である．そこで証明できるものは，例えば，有界実
閉区間上のハイネ=ボレルの被覆定理，実数値連続関数の最大値原理，ワイエルシュト
ラスの多項式近似定理，微分方程式についてのコーシー・ペアノの定理，ブラウワー
の不動点定理，可分バナッハ空間におけるハーン・バナッハの定理，可算可換環は素
イデアルの存在，可算順体には代数閉包の一意存在など，枚挙に暇がない．したがっ
て，WKL0 のよい性質をもつ ω-モデルを考えることは．個々の数学的対象の（特に再
帰理論的側面からの）研究にも有効であろう．
22
厳密には，ここでの ∗(n)T や ≤T などの概念は形式化されたものであることに注意する．より正確
には [10] などを参照．
23
2 つ上の脚注に同じ．
24
WKL はこの体系を特徴づける集合存在公理である弱ケーニヒの補題 (weak König’s lemma) の略
である．
15
4.2
WKL0 の ω-モデル
以下では，集合とその特性関数は同一視する．よって，P (ω) と 2ω は同じものであ
る．X のみを自由変数にもつ Π01 論理式 ϕ(X) を用いて，{X ⊆ ω : P (ω) |= ϕ(X)} と
あらわせるものを，2ω の Π01 クラスという．
Lemma 4.1 A ⊆ 2ω が空でない Π01 クラスであることと，A がある計算可能な無限
0-1 木 T の道全体のなす集合 [T ] であらわせることとは同値である．
Lemma 4.2 共通部分をもたない 2 つの Σ01 -集合 A, B で，A ⊆ C ⊆ B c となる計算可
能集合 C が存在しないものがある．
Proof. A, B を Lemma 4.1 のような Σ01 -集合とする．このとき，
A = {X ∈ 2ω | P (ω) |= ∀n ∈ A(n ∈ X) ∧ ∀n ∈ X(n 6∈ B)}
は，空でない Π01 クラスである．もし，REC が WKL0 のモデルであるならば，Lemma
∩
∩
4.1 より，A REC 6= φ である．そこで，C ∈ A REC とすると，C は計算可能で，
A ⊆ C ⊆ B c をみたす．これは矛盾である．2
Corollary 4.3 REC は WKL0 のモデルではない．
ここでは更に特殊な方法で，WKL0 の ω-モデルを構成する方法を紹介する．ここで
用いられる方法は，原則的に S. G. Simpson [11] に基づく．
Definition 4.3 (Simpson) 2ω の Π01 クラスを再帰的にすべて並べたものを hPe : e ∈
ωi とする25 ．ω × ω <ω の有限集合 p に対して，
∀ (e, σ) ∈ p(Xσ(0) ⊕ · · · ⊕ Xσ(lh(σ)−1) ∈ Pe )
がとなるとき，hXn : n ∈ ωi は p と会うという．
P = {p ⊆ ω×ω <ω | p は有限集合で、標準構造において p と会う hXn : n ∈ ωi が存在する }
とする．また P 上に，p ⊇ q で半順序 p ≤ q を定める．
D ⊆ P は，∀p ∈ P∃q ∈ D(q ≤ p) であるとき，稠密という．集合列 hGn : n ∈ ωi は，P
の任意の定義可能な稠密集合 D に対して，D のある要素 p に会うとき，ジェネリック
という．
Lemma 4.4 ϕ(X) を Π01 -論理式とする．このとき，次が WKL0 で示せる．∃Xϕ(X) は，
ある Π01 -論理式と同値である．
Lemma 4.5 任意の p ∈ P に対して, p と会うジェネッリク hGn : n ∈ ωi が存在する.
25
ここでの「再帰的に並べる」意味は，x, X のみを自由変数にもつ Π01 -論理式 ϕ(n, X) で，任意の
e ∈ ω, A ⊆ ω に対し，A ∈ Pe ⇔ P (ω) |= ϕ(e, A) となるもののことをいう．theorem 2.4 の証明を吟
味するとこのようなものが得られる．
16
Proof. [p] を p に会う hXn : n ∈ ωi 全体のなす集合とする．[p] は (2ω )ω 上の閉集合で
ある. G を p ∈ G となる P 上のジェネリック・フィルターとすると，(2ω )ω のコンパク
∩
∩
ト性より {[q] : q ∈ G} 6= φ となる．このとき，hGn : n ∈ ωi ∈ {[q] : q ∈ G} を取
ればよい．2
Lemma 4.6 任意のジェネリック hGn : n ∈ ωi に対し，{Gn : n ∈ ω} は WKL0 の ω-モ
デルである.
Proof. ∃X(X ⊕ Gn1 ⊕ · · · ⊕ Gnk ∈ Pe ) とする．すなわち，Gn1 ⊕ · · · ⊕ Gnk をオラク
ルにもつ e 番目の相対的再帰 0-1 無限木を考える．すると，Gn1 ⊕ · · · ⊕ Gnk ∈ Pe0 と
なる e0 が存在する.
ところで，p ∈ D を
p ∈ P ∧ ((p ∪ {(e0 , hn1 , . . . , nk i)} 6∈ P) ∨ ∃n((e, hn, n1 , . . . , nk i) ∈ p))
であるように D を定めると，D は稠密なので，ジェネリック hGn : n ∈ ωi はある p ∈ D
に会う．
このとき，D の定義より，Gn ⊕ Gn1 ⊕ · · · ⊕ Gnk ∈ Pe となる n が存在する．よって，
最初に与えた 0-1 無限木は {Gn : n ∈ ω} 内に道をもつ．2
Lemma 4.7 p ∈ P, m ∈ ω とする．p と会うどの hXn : n ∈ ωi に対しても m 番目の集
合 Xm がおなじ A であるとき，A は計算可能である.
Proof. A は補題の条件をみたしているとする．このとき，任意の l ∈ ω に対して，
l ∈ A ⇔ ∀hXn : n ∈ ωi(hXn : n ∈ ωi が p と会うなら，
l ∈ Xm )
⇔ ∃hXn : n ∈ ωi(hXn : n ∈ ωi は p と会い，
l ∈ Xm )
となる．Lemma 4.4 により，2 番目の式は Σ01 , 3 番目の式は Π01 (つまり，その否定が
Σ01 ) なので，A は計算可能である．2
Lemma 4.8 C は C∩REC = ∅ である可算集合とし, p ∈ P とする. このとき，C∩{Gn :
n ∈ ω} = ∅ をみたす，p に会うジェネリック hGn : n ∈ ωi が存在する．
Proof. A ∈ C ，m ∈ ω をとる. DA,m を
DA,m = {p ∈ P | ∀hXn : n ∈ ωi(hXn : n ∈ ωi が p と会うなら，
Xm 6= A)}
で定める．
DA,m は稠密であることを示す．p ∈ P とする．A は計算可能ではないので，Lemma
4.7 より，p と会う hXn : n ∈ ωi で Xm 6= A となるものがある. つまり，ある自然数 l
で，l ∈ Xm 6⇔ l ∈ A である．このとき，A = {X | l ∈ Xm 6⇔ l ∈ A} は Π01 クラスな
ので，ある自然数 e で，A = Pe となる．よって，p ∪ {(e, hmi} ∈ DA,m である．以上
より DA,m の稠密性が示せた．
{DA,m : A ∈ C, m ∈ ω} は稠密集合の可算集合であるから，Lemma 4.5 の証明を考
えると，DA,m 全てに会うジェネリック hGn : n ∈ ωi がとれる．このとき，C ∩ {Gn :
n ∈ ω} = ∅ である. 2
17
Corollary 4.9 φT 6∈ S となる WKL0 の ω-モデルが存在する．
Corollary 4.10 WKL0 から ACA0 は導けない．
4.3
更なる結果
ジェネリック hGn : n ∈ ωi による WKL0 の ω-モデルには更に強いことがいえる．
Definition 4.4 L2 に可算個の集合定数 X0 ,X1 , . . . を加えた言語を L2 (hXn : n ∈ ωi)
とする．ϕ を L2 (hXn : n ∈ ωi) の文とする．p に会う任意のジェネッリク hGn : n ∈ ωi
に対し，{Gn : n ∈ ω} |= ϕ となるとき，p は ϕ を強制するといい，p ° ϕ とかく．た
だし，{Gn : n ∈ ω} において，各 Xn は Gn と解釈する．
強制法の標準的な議論により次の補題が成り立つ．
Lemma 4.11 ϕ を L2 (hXn : n ∈ ωi) の文とする．p に会う任意のジェネッリク hGn :
n ∈ ωi に対し, {Gn : n ∈ ω} |= ϕ ならば，q ° ϕ となるある q ≤ p に hGn : n ∈ ωi は
会う.
Definition 4.5 π は ω から ω の全単射とする．このとき，p ∈ P と L2 (hXn : n ∈ ωi)文 ϕ に対し，π(p) = {(e, hπ(n1 ), . . . , π(nk )i) : (e, hn1 , . . . , nk i) ∈ p}，π(ϕ) =「ϕ の中
の各 Xn を Xπ(n) に置き換えたもの」と定める．
明らかに p ° ϕ ⇔ π(p) ° π(ϕ) である．
supp(p) =
∪
{{n1 , . . . , nk } : (e, hn1 , . . . , nk i) ∈ p}.
を p ∈ P のサポートという．
p, q ∈ P に対して， supp(p)∩supp(q) = φ ならば，p∪q ∈ P である. また，hGn : n ∈ ωi
がジェネリックならば，ω から ω の全単射 π に対して，hGπ(n) : n ∈ ωi もジェネリッ
クである．
Lemma 4.12 任意の p, q ∈ P は，同じ L2 -文を強制する.
Proof. ϕ を L2 -文とする. p ° ϕ, q 6° ϕ だとして矛盾を導く．このとき，q 0 ° ¬ϕ とな
る q 0 ≤ q が存在する．π を supp(π(p)) ∩ supp(q 0 ) = φ となる ω から ω の全単射とする．
π(ϕ) = ϕ なので, π(p) ° ϕ である. よって, π(p) ∪ q 0 ° ϕ となる．これは，q 0 ° ¬ϕ に
矛盾する．2
Lemma 4.8, 4.12 から，２つのジェネリック hGn : n ∈ ωi と hG0n : n ∈ ωi によって得
られる２つの ω-モデル {Gn : n ∈ ω}，{Gn : n ∈ ω} は同じ L2 -文をみたす．
Definition 4.6 (定義可能性) M を L2 -構造とする．集合 A ⊆ |M | は，ある（パラメー
タなしの）L2 論理式 ϕ(X) で，M |= ϕ(A) となる（SM の中の）ただ一つの集合であ
るとき，S 上定義可能26 という．
26
この「定義可能性」は Definition 1.6 の定義可能性と異なる．次の Theoreom 4.10, 4.11，および
Theorem 5.6 においてのみ，Definition 4.6 の意味の定義可能性を用いることにする，
18
Theorem 4.13 WKL0 の ω-モデル S で，S 上定義可能な集合がすべて計算可能とな
るものが存在する．
つまり WKL0 の ω-モデル S には計算不可能な集合も属するわけだが，上の定理のよう
なモデルでは，そのようなものは定義てきないわけである．
Proof. ジェネリック hGn : n ∈ ωi に対し，S = {Gn : n ∈ ω} とする．これが求め
るものであることを示そう．A ∈ S は，S で定義可能であるとする．Lemma 4.8 より，
S 0 = {G0n : n ∈ ω} が S ∩ S 0 = REC となるジェネリック hG0n : n ∈ ωi をとる．
ϕ(X) を A を定義する L2 -論理式とする．すなわち S |= ∃!Xϕ(X) ∧ ϕ(A) である27 .
S と S 0 は同じ L2 -文を成り立たせるから S 0 |= ∃!Xϕ(X) である. A0 ∈ S 0 を S 0 |= ϕ(A0 )
となる唯一のものとしよう. このとき n ∈ ω に対し,
n ∈ A ⇔ S |= ∃X(ϕ(X) ∧ n ∈ X) ⇔ S 0 |= ∃X(ϕ(X) ∧ n ∈ X) ⇔ n ∈ A0 .
である．よって A = A0 となり，S ∩ S 0 = REC なので，A は再帰的集合となる. 2
また，任意の集合 Y に対し，Definition 4.3 を相対化したものを考えると，パラメー
タを認めるように拡張した定義可能性について次の結果を得る．
Theorem 4.14 「∀X, Y (X は Y のみをパラメータに使って定義可能ならば，X ≤T Y )
である」をみたす WKL0 の ω-モデルが存在する．
以上の議論は ω-モデルにこだわる必要がなく，WKL0 の可算モデルにおいて同様の
議論をすることができ，次の結果を得る．
Theorem 4.15 ϕ(X, Y ) を X, Y のみを自由変数にもつ算術的論理式とする．このと
き，WKL0 ` ∀X∃!Y ϕ(X, Y ) ならば，RCA0 ` ∀X∃!Y ϕ(X, Y ) である．
補遺
5
5.1
体系 ATR0
β-モデルを考えるとき，これまでに紹介しなかった体系で特に重要なものに ATR0
がある．5.1 節では，ATR0 について簡単に紹介しておく．ATR0 は ACA0 と Π11 -CA0 の
中間の体系であり，ATR はこの体系を特徴づける集合存在公理である算術的超限再帰
(arithmetical transfinite recursion) の略である．
算術的超限再帰について述べる前にまず，算術的超限帰納法について述べよう．算
術的超限帰納法とは，算術的な性質についての与えられた整列集合に沿った超限帰納
法である．
27
∃!Xϕ(X) は「ϕ をみたす X が一意に存在する」ことを意味する
19
Definition 5.1 RCA0 において次が定義できる．N 上の 2 項関係 X ⊆ N × N は (等号
付き) 順序関係であるとする．X の領域を field(X) = {i : (i, i) ∈ X} とする．文脈上
i ∈ field(X) であることが明らかなときは field(X) は省略することもある．この X で
決まる順序を ≤X とする．すなわち，i ≤X j は (i, j) ∈ X のことである．また，i <X j
は i ≤X j かつ i 6= j のこととする．
X は無限下降列をもたない，つまり，∀n ∈ N(f (n + 1) <X f (n)) となる関数 f : N →
field(X) が存在しないとき整礎 (well-founded) という．整礎な全順序 X を可算整列順
序 (countable well-ordering) という．
明らかに「X は全順序である」という主張は Π01 であり「X は可算整列順序である」と
いう主張は Π11 である．
Lemma 5.1 (算術的超限帰納法) ϕ(j) を算術的論理式とする．このとき ACA0 で次が
証明できる．X が可算整列順序のとき，∀j((∀i <X j)ϕ(i) → ϕ(j)) ならば ∀jϕ(j) で
ある．
Proof. ∀jϕ(j) でないとして矛盾を導く．
∀jϕ(j) でないとすると算術的内包公理より ∀j(j ∈ Y ↔ ¬ϕ(j)) となる Y 6= φ が存
在する．超限帰納法の仮定により，j ∈ Y ならば i ∈ Y となる i <X j が存在する．よっ
て，原始再帰法により，
f (0) = j ∈ Y となる最小の j,
f (n + 1) = i <X f (n) ∧ i ∈ Y となる (自然数として) 最小の i，
をみたす関数 f : N → Y が存在する．f は明らかに X の無限下降列であり，これは X
が整列であることに反する．2
ϕ(x, Y ) を x と Y を自由変数にもつ算術的論理式とする．ϕ は，集合 A を集合 {n :
ϕ(n, A)} に換える操作とみなさせる．この操作を与えられた可算整列順序に沿って超
限回繰り返すことによって得られる集合の存在を保証するのが算術的超限再帰の公理
である．
Definition 5.2 (算術的超限再帰) (1) θ(x, Y ) を算術的論理式とする．このとき，Hθ (X, Y )
を次をあらわす算術的論理式とする：
X は全順序で Y = {(n, j) : θ(n, Y j )} ⊆ N2 である.
ただし，Y j は {(m, i) ∈ Y : i <X j ∧ (m, i) ∈ Y } のことである．また θ(x, Y ) は x, Y
以外の自由変数をもってもよい．その場合，Hθ (X, Y ) も同じ自由変数をもつ．
(2) 次の公理図式を算術的超限再帰という：
∀X(X が可算整列順序ならば ∃Y Hθ (X, Y )), ここで θ は算術的論理式である．
Definition 5.3 ACA0 に算術的超限再帰公理を加えた体系を ATR0 という．
Lemma 5.2 任意の β-モデルは ATR0 のモデルである．
Proof. ATR0 の定義より明らか．2
3.3 節のように，この結果は可算披コード ω-モデルを利用して形式化することがで
きる．
20
Definition 5.4 RCA0 で次が定義できる．可算披コード ω-モデル W は，x, y, X, Y の
みを自由変数にもつ任意の Σ1,w
1 -論理式 ϕ(x, y, X, Y ) に対して，
∀n, m, l, k ∈ N(ϕ(n, m, Wl , Wk ) ↔ W |= ϕ(n, m, Wl , Wk ))
をみたすとき，可算披コード β-モデルという．
Theorem 5.3 ACA0 で次が示せる．任意の可算披コード β-モデル W は ATR0 のモデ
ルである．
Theorem 5.4 Π11 -CA0 で次が示せる．任意の X ⊆ N に対し，X ∈ W となる可算披
コード β-モデル W が存在する28 .
Corollary 5.5 Π11 -CA0 で，ATR0 の無矛盾性が示せる．
WKL0 と ATR0 はよく似た性質をもつ．例えば，Theorem 4.13 に対応するものとして
次が成り立つ．
Theorem 5.6 ATR0 の β-モデル S で，S 上定義可能な集合がすべて ∆11 となるものが
存在する29 ．
5.2
逆数学
ここで，あつかった二階算術の部分体系は逆数学と呼ばれる研究プログラムに密接
にかかわっている．本講演とは直接関係ないが最後にこれについて触れたい．
ヒルベルトが当初思い描いていたような数学の無矛盾性の証明は，ゲーデルの第二
不完全性定理によって不可能であることがわかった．しかし，それ以降もどのような
形式体系の上でどれほど数学が展開されうるかという研究が続けられている．逆数学
もまたそのような研究の 1 分野である．
古典的数学の大部分は Z2 で展開できる．更にいくつかの本質的例外はあるものの，
Z2 を Π11 -CA0 や ACA0 に制限してもかなりのことが展開できる．このとき，個々の具
体的な数学の定理についてどの公理が本質的に必要であるのか問うのは自然であろう．
1960 年代後半から 70 年代にかけての Z2 における数学の展開の研究を通し，H. フリー
ドマンはこのような疑問に対して多くの場合で明確な答えがあたえられることを発見
した．逆数学のはじまりとされる 1974 年のカナダのバンクーバーで開かれた国際数学
者会議の講演 [2] で，フリードマンは次のような主張をしている．
(原則 I) 適切な公理から定理が証明できるならば, その公理はその定理
から証明できる．
28
29
この主張は ACA0 のもとで，Π11 -CA0 と同値である．
∆11 とは，Σ11 でも Π11 でもあるということ．
21
つまり，公理から定理を導く数学の通常のパターンとは逆に，定理からそれを証明する
のに用いた公理を導くことができるということである．この原則に基づく研究が「逆
数学」である．
Z2 で数学を展開するとき最も大きな役割を果たしているのは集合内包公理 (Definition1.3(3)) である．内包公理の役割を調べるとき，実際には集合内包公理の制限によっ
て特徴付けられる Z2 の部分体系を調べる方がよい．T をそのようにして得られる部分
体系とする．ただし，RCA0 ⊆ T とする．ここで，τ として何らかの古典的数学の定理
をとろう．多くの場合，τ の中にあらわれる概念は，コード化を利用して RCA0 で定義
できると考えられる．したがって，原則 I をもう少し正確に述べれば，次のようにな
る30 ．
RCA0 で定義できる数学の定理 τ に対して，多くの場合，適切な T を選
べば RCA0 上で T と τ の同値性が証明できる．
具体的な τ としてボルツァノ・ワイエルシュトラスの定理「任意の有界実数列は収束
する部分列をもつ」を例にとる．実際，
「実数列」や「収束」などの概念は RCA0 で定
義できるので，この主張そのものは RCA0 で意味をなす．しかし，一方でボルツァノ・
ワイエルシュトラスの定理は RCA0 で証明できない．このとき，上の原則に乗っ取っ
た次の事実が示される．
Theorem 5.7 RCA0 上で次の同値性が示せる．
(1) ACA0 . (2) ボルツァノ・ワイエルシュトラスの定理.
このように数学の定理 τ と (RCA0 上で) 同値な体系を Sτ とする．無数の τ を考えれ
ば，Sτ としてあらわれる体系は無数にあるように思われる．しかし驚くべきことに，
70 年代後半以降のフリードマンや S. G. シンプソンたちの多くの研究によって，Sτ と
してあらわれる体系はここで紹介した RCA0 ，WKL0 , ACA0 , ATR0 , Π11 -CA0 の 5 つくら
いしかないことが明らかになっている31 ．
以上のことをまとめると次のようになる．
非常に多くの場合において，RCA0 で定義できる数学の定理 τ は，RCA0
で証明できるかもしくは， WKL0 , ACA0 , ATR0 , Π11 -CA0 のいずれかと RCA0
上で同値になる．
結論として，逆数学の目的は上の 5 つの体系のどれが Sτ なっているかで数学の定理
τ を分類することだといえる．
ここからの簡単な本講演と関係する帰結としては，それぞれの ω-モデルの特徴付け
として，ある種の数学的な性質を与えるとことができるということである．例えば，
Theorem 2.6 において，ACA0 の ω-モデルを 3 つの性質によって特徴付けたわけである
30
このように定理と体系の同値性は RCA0 上で証明される．この意味で RCA0 を基本体系 (base theory)
という．定理 τ においては RCA0 では定義すらできない場合がある．この場合 RCA0 は基本体系として
ふさわしくない．このとき RCA0 のかわりに ACA0 を基本体系にして同様の結果が得られることも多い．
また逆に，RCA0 で証明できる定理の中には，RCA0 より弱い体系でも定義できるものがある．そのよ
うな体系を基本体系にして，定理と RCA0 の同値性を調べる場合もある [5, 6, 12]．
31
この事実はいくつかの意味で私には好ましく感じる．
22
が，Theorem 5.7 から，Theorem 2.6 の条件 (3) を「(3)’ S に属する有界実数列（のコー
ド）はかならず，S に属する集積値をもつ．
」におきかえられることがわかる．このよ
うに，Theorem 2.6 の条件 (3) をいろいろ変えることで，WKL0 , ACA0 , ATR0 , Π11 -CA0
の ω-モデルを特徴付けられる．
参考文献
[1] Y. L. Ershov, S. S. Goncharov, A. Nerode, J. B. Remmel and V. W. Marek
(eds.), Handbook of recursive mathematics. Vol. 1, 2. Studies in Logic and the
Foundations of Mathematics (138, 139). North-Holland, Amsterdam, 1998. xlvi
and 1–620, i–xlvi and 621–1372.
[2] H.Friedman, Some systems of second order arithmetic and their use, Proceedings of the International Congress of Mathematicians, Vancouver 1974, vol. 1,
Canadian Mathematical Congress, 235–242.
[3] H.Friedman, Systems of second order arithmetic with restricted induction I, II
(abstracts). J. Symb. Logic (41), 1976, 363–367. 19 pages, unpublished, March
1974.
[4] P. Hájek and P. Pudlák, Metamathematics of First-Order Arithmetic, SpringerVerlag, 1993, xiv + 460 pages.
[5] K. Hatzikiriakou, Algebraic disguises of Σ01 induction, Arch. Math. Logic 29,
1989, 47–51.
[6] K. Hatzikiriakou, Comutative algebra in subsystems of second order arithmetic,
Ph.D. thesis, Pennsylvania state University, 1989, vii+43 pages.
[7] P. Bernays and D. Hilbert, Grundlagen der Mathematik, volume I and volume II,
Grundlehren der mathematischen Wissenschaften, Springer-Verlag, second edition, 1968–1970.
[8] S. C. Kleene, Arithemtical predicates and function quantifiers, Transactions of
the America Mathematical Society (79), 1955, 312–340.
[9] J. E. Quinsey, Applications of Kripke’s Notion of Fulfilment, Ph.D. thesis, Oxford
University, 1980, 132 pages.
[10] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in
Mathematical Logic. Springer-Verlag, 1999. xiv + 445 pages.
[11] Stephen G. Simpson. Π01 sets and models of WKL0 . Reverse mathematics 2001,
Lect. Notes Log., 21, 2005, 352–378.
23
[12] S. G. Simpson and R. Smith, Factorization of polynomials and Σ01 induction,
Annals of Pure and Applied Logic 31 (1986), 289–306.
[13] 田中一之, 逆数学と 2 階算術（数学基礎論シリーズ 4）, 河合出版, 1997.
24