レーヴェンハイム–スコーレムの定理

**レーヴェンハイム–スコーレムの定理**（）とは、可算な一階の理論が無限モデルを持つとき、全ての無限濃度 κ について大きさ κ のモデルを持つ、という数理論理学の定理である。そこから、一階の理論はその無限モデルの濃度を制御できない、そして無限モデルを持つ一階の理論は同型の違いを除いてちょうど1つのモデルを持つようなことはない、という結論が得られる。

## 背景
シグネチャ（非論理記号の一覧）には、関数記号の集合 *S*func、関係記号の集合 *S*rel、関数記号と関係記号のアリティを表す関数 \operatorname{ar}\colon S_{\mathrm{func}} \cup S_{\mathrm{rel}} \rightarrow \mathbb{N}_0 から成る（0項の関数記号は、定項記号と呼ばれる）。一階述語論理では、シグネチャを**言語** (language) とも呼ぶ。シグネチャに含まれる関数記号と関係記号の集合が可算であるとき、そのシグネチャは可算であると言い、一般にシグネチャの濃度とは、そこに含まれる全記号の集合の濃度を意味する。

一階の**理論** (theory) は、固定されたシグネチャと、そのシグネチャにおける固定された文（自由変項のない論理式）の集合で構成される。その論理式の集合は論理的帰結の下で閉じている。理論はその理論を生成する一連の公理で指定されたり、構造を与えてその構造を満足する文で理論を構成したりすることが多い。

シグネチャ σ があるとき、σ の構造 *M* とは、σ にある記号群の具体的な解釈である。それには、基盤となる集合（それ自体もしばしば "*M*" で表される）とσの関数記号および関係記号の解釈が含まれる。*M* におけるσの定数記号の解釈は、単に *M* の元である。より一般化すれば、*n*引数の関数記号 *f* の解釈は、*M**n* から *M* への関数である。同様に関係記号 *R* の解釈は *M* 上の *n*項関係であり、すなわち *M**n* の部分集合である。

σ構造 *M* の**部分構造** (substructure) は、σの全ての関数の解釈の下で閉じた（つまり、σの全定数記号の解釈を含む）*M* の部分集合 *N* を取り、関係記号の解釈を *N* に制限することで得られる。**[[初等部分構造]]** (elementary substructure) はその非常に特殊な場合であり、元の構造と全く同じ一階の文を満たす。（このとき*N*は*M*の**初等的拡張**(elementary extension)という。）

## 正確な記述
この定理の現代的な形式は、本項目の導入部で行っている可算なシグネチャのバージョンよりも一般的で強い。

一般化されたレーヴェンハイム–スコーレムの定理では、あらゆるシグネチャ σ、あらゆる無限濃度の σ構造 *M*、あらゆる無限濃度 κ ≥ |σ| について、|N| = κ となる σ構造 *N* があり、
* κ  |*M*| なら、*N* は *M* の初等的拡張である。

この定理は、上の箇条書きされた部分に対応して2つに分割されることが多い。ある構造がより小さい濃度の初等部分構造を持つとする定理の部分を**下方レーヴェンハイム–スコーレムの定理**  と呼ぶ。ある構造がより大きい濃度の初等拡張を持つとする定理の部分を**上方レーヴェンハイム–スコーレムの定理** と呼ぶ。

冒頭の簡単な言明の場合、理論の無限のモデルとは、ここでいう M である。定理の上方部分の証明は、いくらでも大きな有限のモデルを持つ理論は無限のモデルを持たねばならないことをも示す。この事実を定理の一部とする場合もある。

## 例と帰結
自然数を **N**、実数を **R** とする。この定理によれば、(**N**, +, ×, 0, 1) の理論（真の一階算術の理論）には非可算なモデルがあり、(**R**, +, ×, 0, 1) の理論（実閉体の理論）には可算なモデルがある。もちろん同型の違いを除いて、(**N**, +, ×, 0, 1) と (**R**, +, ×, 0, 1) を特徴付ける公理化が存在する。レーヴェンハイム–スコーレムの定理は、それらの公理化が一階ではあり得ないことを示している。例えば、線型順序の完備性は実数が完備な順序体であることを特徴付けるのに使われるが、その線型順序の完備性は一階の性質ではない。

理論が**範疇的** categorical であるとは、同型の違いを除いて唯一のモデルを持つことを意味する。この用語は1904年、オズワルド・ヴェブレンが考案したもので、その後しばらくの間、数学者らは集合論を範疇的な一階の理論で記述することで、数学の堅固な基盤を築けると考えていた。レーヴェンハイム-スコーレムの定理はこの希望への最初の打撃となった。なぜなら、その定理によれば無限のモデルを持つ一階の理論は範疇的にはなり得ないからである。さらに1931年、ゲーデルの不完全性定理によって希望は完全に打ち砕かれた。

レーヴェンハイム-スコーレムの定理から導かれる結論の多くは、一階とそうでないものの違いがはっきりしていなかった20世紀初頭の論理学者にとっては直観に反していた。例えば、真の算術 (true arithmetic) には非可算なモデルがあり、それらは一階のペアノ算術を満足するが、同時に帰納的でない部分集合を持つ。さらに悩ましかったのは、集合論の可算なモデルの存在である。それにもかかわらず、集合論は実数が非可算であるという文を満たさなければならない。この直観に反するような状況はスコーレムのパラドックスと呼ばれ、可算性 (countability) は絶対的 (absolute) ではないことを示している。

## 歴史
以下の記述は主に  に基づいている。モデル理論の初期の歴史を理解するには、統語論的整合性（一階論理の推論規則を使って導かれるものには矛盾がないこと）と充足可能性（satisfiability、モデルがあること）を区別しなければならない。驚くことに、ゲーデルの完全性定理が同値であることを証明する以前なのに、整合性 (consistency) という用語はどちらの意味にも使われていた。

後にモデル理論となる重要な成果は、 が "Über Möglichkeiten im Relativkalkül"（1915年）で発表した下記の「レーヴェンハイムの定理」であった。

:全ての可算なシグネチャ σ について、充足可能な全てのσ文は可算モデルにおいて充足可能である。

しかし、レーヴェンハイムの証明は間違っていた。1920年、トアルフ・スコーレムは後にスコーレム標準形と呼ばれるようになる論理式を使って選択公理に基づいた正しい証明を行った。

:モデル *M* で充足可能な全ての可算な理論は、*M* の可算な部分構造において充足可能である。

1923年、スコーレムは選択公理を使わない以下のような弱い形の定理も証明した。
:あるモデルで充足可能な全ての可算な理論は、可算なモデルにおいても充足可能である。
さらに1929年、スコーレムは1920年の成果を単純化した。そして Anatoly Ivanovich Maltsev (Анато́лий Ива́нович Ма́льцев, 1936年) が完全に汎用的な形式でレーヴェンハイム-スコーレムの定理を証明した。彼が引用したスコーレムのメモによれば、アルフレト・タルスキが1928年にこの定理を既に証明していたという。このため一般化した定理を「レーヴェンハイム-スコーレム-タルスキの定理」とも呼ぶ。しかし、タルスキは自分が証明したことを覚えておらず、彼がコンパクト性定理を使わずにどうやって証明しえたのかは謎のままである。

スコーレムの名が下方の定理（下降定理）だけでなく上方の定理（上昇定理）にも付与されているのは、ある意味で皮肉である。
:「私は、系 6.1.4 を慣例に従って上方レーヴェンハイム-スコーレムの定理と呼ぶ。しかし、実のところスコーレムは非可算集合の存在を信じておらず、したがってこの定理の意味するところを信じてすらいなかった」 - 
:「スコーレムは … その結論を意味がないとして拒絶した。タルスキは … スコーレムの形式主義的観点に立つなら、上方の定理を無意味だとするなら下方レーヴェンハイム-スコーレム定理も無意味とすべきではないか、と非常に適切に応えた」 - 
:「トアルフ・スコーレムは亡くなる直前まで、この定理に彼の名が冠せられていることに憤慨していたという。彼は非可算集合の存在そのものが不合理であるとし、実在しないと考えていた」 - 

## 脚注

## 参考文献
レーヴェンハイム-スコーレムの定理は、モデル理論や数理論理学の教科書には必ずといってよいほど登場する。

### 一次文献
* 
**  ()
* 
* 
**  ()
* 
**  ()
* 
* 

### 二次文献
* ; A more concise account appears in chapter 9 of 
* 
* 
* 
* 

## 外部リンク
* 
* Burris, Stanley N., Contributions of the Logicians, Part II, From Richard Dedekind to Gerhard Gentzen
* Burris, Stanley N., Downward Löwenheim&ndash;Skolem theorem
* Simpson, Stephen G. (1998),  Model Theory