1 概要
1.1 定義と対象
モデル理論は、論理式で記述される理論が、具体的な数学的構造（モデル）として実現される様子を研究する論理学の領域である。理論とは、形式言語上の一連の文（公理の集合など）として与えられ、モデルはその言語を通じて構造の上で解釈される。焦点は、同じ理論でも異なるモデルが存在しうること、さらにそのモデルがどのように分類されるか、という点に置かれる。
対象として扱われるのは、数学的構造そのものだけでなく、それを記述する論理言語の選択や、満足（ある式がその構造で真になること）という意味論的概念である。モデル理論の基本的な問題意識は、「公理や定義が意図する性質が、どのような構造の中で実現されるか」を体系的に解明することにある。
1.2 数理論理学における位置づけ
モデル理論は、通常、数理論理学の意味論と密接に結びつく分野として位置づけられる。形式言語と意味を与える枠組みのもとで、構造上の真偽を扱うため、証明論（構文的に証明可能性を研究する側面）や計算理論（計算可能性や計算資源の観点）と相互に影響し合う。
また、集合論や代数、幾何といった数学の諸分野と並走する点でも特徴的である。言語と理論を通して、数学的対象の性質を記述可能な形に落とし込み、モデルとしての存在・分類・不変量を抽出することで、分野横断的な橋渡しを行う。
1.3 主要な研究目的
モデル理論の中心的な目的は、理論のモデルクラスを理解することである。具体的には、次のような問いが典型となる。
第一に、ある理論がモデルを持つか（存在問題）である。第二に、そのモデルがどれほど多様か（分類・同値性）である。第三に、理論の性質が論理式の複雑さの範囲でどの程度決定可能か（可解性・完全性の観点）である。第四に、モデルの濃度や位相に似た振る舞いとして、ある条件を満たす小さな部分が大きな対象へどのように拡張されるか（コンパクト性やレーヴェンハイム・スコーレム型の結果）が研究対象となる。
加えて、どの性質が論理言語で定義可能か（定義可能性）や、どのような構造がある理論に対して計算的・実装的な意味を持つか（計算理論との連携）も重要な目的となる。
2 基本概念
2.1 形式言語
2.1.1 論理記号
形式言語は、論理記号と非論理記号から構成される。論理記号としては、真偽に関わる記号、否定、連言、選言、含意といった論理結合子に加え、量化子（全称・存在）などが用いられる。これらは、論理式の形を規定し、どのように数学的性質を論理文として記述できるかを決める。
論理記号は構造そのものには依存せず、あくまで論理の枠組みを与える。したがって、同じ非論理記号を持つ言語でも、論理記号の選択（たとえば量化の形の違い）がモデル理論の性質を大きく変えることがある。
2.1.2 非論理記号
非論理記号は、対象となる数学的構造に固有の情報を運ぶ。たとえば、定数記号、関数記号、関係記号などが該当する。これらは、群であれば乗法や単位元の記号、順序構造であれば大小関係の記号といった形で導入される。
非論理記号が与えるのは「その言語では何が語れるか」である。たとえば関数記号を含めるか、関係だけを扱うかで、同じ対象でも記述される式の種類が変わり、結果として理論のモデルクラスの振る舞いにも差が生じる。
2.2 構造
2.2.1 台集合
構造は、台集合(ドメイン)と呼ばれる対象の母集合、さらにその上で解釈される非論理記号の意味の組として定義される。台集合上の要素が、変数の取り得る値を表す。
モデル理論では、台集合の濃度や可算性なども重要なパラメータとなる。理論がどの大きさの台集合で実現可能か、また異なる濃度のモデルが同じ理論を満たすか、といった問いが定理として現れる。
2.2.2 解釈
解釈は、非論理記号に対して台集合上の具体的な対応を与える操作である。定数記号なら台集合の特定の要素、関数記号なら台集合から台集合への写像（多変数なら対応する多変数関数）、関係記号なら台集合のべき集合上の関係を指定する。
この解釈の違いによって同じ言語でも異なる構造が生じる。したがってモデル理論の議論では、形式的な文の意味が、解釈された構造の上でどのように真になるかを追跡することが中心となる。
2.3 理論
2.3.1 公理系
理論は、通常は形式言語の文の集合として与えられる。公理系とは、理論のうち特定の文群を生成元として提示したものと見なせる。理論の要点は、そこに含まれる文がモデルで満足されるべき性質を規定する点にある。
また、理論の間には包含関係が考えられる。ある理論が別の理論の全公理を含むとき、モデルクラスも包含関係を持つ。さらに、同じモデルクラスを持つ理論は意味論的に同値視されることがある。
2.3.2 モデル
ある理論のモデルとは、その理論に属するすべての文を満足する構造である。満足の定義は意味論に依存するため、モデルの概念は論理式の解釈に裏打ちされる。
モデル理論では、「理論がモデルを持つか」だけでなく、「理論が持つモデルがどのように互いに似ているか」も追う。とくに同型やより弱い同値概念は、数学的に意味のある分類を可能にする。
2.4 満足関係
2.4.1 式の真偽
満足関係とは、構造と変数代入のもとで、ある式が真になるかどうかを定義する関係である。たとえば原子式（関係記号により作られる基本文）では、解釈された関係が成立するかで決まる。
複雑な式については、連言や選言、否定といった論理結合子に従って真偽が構成され、量化子に対しては台集合の全要素または存在する要素についての評価が行われる。この帰納的定義により、論理式の真偽が構造上で一貫して定義される。
2.4.2 文と理論の満足
文は自由変数を持たない式であるため、満足は代入に依存しない。ある文が構造で満足されるとは、その文がその構造上で真になることを意味する。
理論の満足は、理論に属するすべての文が同一の構造で満足されることとして定義される。したがって、モデルという概念は満足関係の集約として理解できる。
3 中心的定理と性質
3.1 完全性
3.1.1 完全性定理
完全性定理とは、構文的な導出（証明可能性）と意味論的な満足（真であること）の対応を与える結果である。粗く言えば、ある文が論理規則によって証明できるならば、その文はすべてのモデルで真であり、逆にすべてのモデルで真ならば証明可能である、という対応が成立する。
この種の定理により、モデル理論の意味論的視点が、証明論の言語で扱える形に橋渡しされる。つまり、「モデルでの真理」が「形式体系での証明」という構文的事実と整合する保証が得られる。
3.1.2 充足可能性との関係
充足可能性とは、ある集合の文（あるいは単一の文集合）が、どこかの構造で同時に満足されるかを問う概念である。完全性は、この充足可能性を論理体系の証明可能性に結びつける。
結果として、ある文集合が矛盾しないことを示すには、代数的・集合論的に構成する代わりに、形式的な矛盾の非導出を検討すればよい、という手法が可能になる。逆方向にも、証明可能性の欠如が意味論的な実現可能性を示唆する。
3.2 コンパクト性
3.2.1 有限充足性
コンパクト性定理は、（一階論理の範囲で）無限に多くの文からなる理論が充足可能であるかどうかが、その理論の任意の有限部分の充足可能性だけで決まる、という性質を述べる。すなわち、有限個ずつは実現できるのに全体としては実現できない、という挙動は一階では起こりにくい。
この性質はモデル理論の基本道具であり、理論を無限の制約として扱う際に、有限段階で得られた情報を組み合わせることで結論を導ける。
3.2.2 応用例
コンパクト性は、定義や存在の証明に広く利用される。たとえば「ある性質を満たしつつ他の性質を満たさない」構造を構成したい場合、有限部分の要求が矛盾しないことを示せれば、全体の実現可能性が保証される。
また、量化の深さを抑えた断片的情報が、より大きなモデルの存在にまで影響することを可能にする。結果として、超準モデル理論や定義可能性の議論にも滑らかに接続されることが多い。
3.3 レーヴェンハイム・スコーレムの定理
3.3.1 下方レーヴェンハイム・スコーレム性
下方レーヴェンハイム・スコーレム性は、ある無限モデルが存在するなら、その理論のモデルとして、より小さい濃度のモデルも存在しうることを述べる。要点は、モデルの大きさが特定の下限を跨いで柔軟に実現できる場合があるという点である。
この性質は、可算性や多様体の基礎付けのように、対象のサイズを調整したい場面で有効になる。理論が一度成立していれば、別の濃度での実現にも波及するからである。
3.3.2 上方レーヴェンハイム・スコーレム性
上方レーヴェンハイム・スコーレム性は、反対方向の現象として、あるモデルが存在すると、より大きい濃度のモデルも作れることを扱う。コンパクト性と組み合わさることで、理論の制約が「台集合をあまりにも厳密に固定する」ことが一階の枠では難しい、という見取り図が得られる。
特に、定理が成立するための前提や、無限性の必要条件などは重要である。これらを理解することで、同じ論理言語でも高階に上がると挙動が変わり得ることが見えてくる。
3.4 同型と元素的同値
3.4.1 元素的部分構造
要素的部分構造とは、台集合の部分を選び、関係や関数の解釈を制限して得られる部分モデル的な構造である。モデル理論では、単なる包含にとどまらず、「その部分が式の真偽をどの程度保つか」が関心の中心となる。
この観点で部分構造に対して、量化をまたぐ式でどれほど振る舞いが一致するかを調べる。一致の程度は、後述する元素的同値（elementary equivalence）や、どの断片まで一致するかという形で表現される。
4.4.2 元素的拡大
元素的拡大は、部分構造を適切に含むより大きな構造を考え、その部分と元の構造で論理式の評価が同じになる状況を扱う概念である。直感的には、「小さい世界で真だったことが大きい世界でも同様に真である」ことを保証する拡張として捉えられる。
この考え方は、超準拡大のような大きな枠組みとも相性が良い。有限・無限の境界をまたいで、論理的性質の保存を軸にモデルを比較することで、数学的直観を論理の精度で支える。
4 主要分野
4.1 古典モデル理論
4.1.1 一階理論
古典モデル理論の中心は、一階論理の理論研究である。一階とは、量化が台集合上の個体にのみ作用し、述語や関係そのものを量化の対象にしない枠組みを指すことが多い。これにより、コンパクト性やレーヴェンハイム・スコーレム型の強力な定理が利用可能になる。
一階理論では、具体的な数学構造（群、環、順序など）を言語で記述し、その公理のモデルがどう振る舞うかを解析する。分類可能性や決定可能性といった性質も、この枠の中で大きな焦点となる。
4.1.2 可算理論
可算理論は、可算言語上の一階理論を中心に研究する方向性である。可算性は、理論のモデルや型の取り扱いにおける技術的単純化をもたらし、分類・特徴付けの議論を進めやすくする。
また、可算性は直観的に「有限記述に近い」振る舞いを示す場合があり、構成法や分岐の制御に役立つ。結果として、安定性理論への橋渡しや、型理論的な整理にも関係してくる。
4.2 安定性理論
4.2.1 安定理論
安定性理論は、モデル理論において「無秩序に増殖する振る舞い」を抑えた形で、理論の性質を分類する流れである。直感的には、あるパターンの多様性が過剰に増える状況を排し、型の構造が整った場合に強い結論が得られる。
この枠組みでは、安定（stability）という性質が中心概念となる。安定性があると、型の振る舞いがより規則的になり、モデルの分類や幾何的な対応が取りやすくなる。
4.2.2 特徴付け
安定性理論では、安定性を複数の同値な条件として特徴付けることがよく行われる。たとえば、型の実現のされ方、ある種の分岐の制御、無限列に基づく計数など、複数の視点から同じ概念を捉え直す。
特徴付けの価値は、どの条件が扱いやすいかは研究対象により変わるためである。ある代数構造では型の計数が自然に計算でき、別の場面では別種の分岐条件が検証しやすい。安定性の同値条件は、その選択肢を提供する。
4.3 超準モデル理論
4.3.1 超準拡大
超準拡大は、ある構造をより大きな構造に埋め込み、その拡大の上で「無限小」や「無限大」に見える要素を扱う技法として知られることが多い。数学的には、ある種の体上での拡大や、論理的条件を満たす拡大モデルの構成として現れる。
超準拡大の特徴は、元の構造で真であった論理的性質が、拡大後も同じ形で反映されるように設計される点にある。これにより、直観的には極限操作に近い挙動を、モデル内の通常の計算で再現できる。
4.3.2 超準解析
超準解析は、超準モデル理論の手法を解析学へ応用する流れである。実数の拡大体上で、無限小量の振る舞いを厳密に扱い、微分や積分に相当する議論を再構成する試みが行われる。
この分野では、論理的に保証された要素の存在や、真理の保存に基づく推論が中核となる。結果として、従来の解析の概念を、モデル論的な枠組みで捉え直す道が開かれる。
4.4 有限モデル理論
4.4.1 有限構造
有限モデル理論は、モデルを「有限構造」に限定して研究する方向性である。一般のモデル理論では、無限モデルの存在が強力な定理を支えるが、有限性を強制すると事情が変わり、同じ論理式でも結論が細かくなる。
この制約は計算機科学との関係を生む。有限構造だけを考えることで、データの有限表現やアルゴリズム的扱いやすさに直結するためである。
4.4.2 計算理論との関係
有限モデル理論は、計算計画や計算複雑性との相互作用が深い。たとえば、ある計算問題が、特定の論理言語によって記述可能かどうかが研究される。これにより、論理の表現能力が計算能力と対応づけられる。
また、決定手続きや検証可能性といった観点が、論理式の断片（たとえば量化の範囲）と関連付けられる。こうした対応は、形式検証や仕様記述の理論基盤にも波及する。
5 応用
5.1 代数学への応用
5.1.1 群論
群論では、群を記述する一階言語を選び、公理化された性質をモデルとして検討する。たとえば可換性や指数、中心の振る舞いなどが論理式として表現される場合、モデル理論は同値性や不変量の分類に役立つ。
さらに、同一理論を満たす群の間の関係、部分構造の拡張、型の実現などを通じて、代数的な構造の違いを論理的に測ることができる。
5.1.2 環論
環論の応用では、加法と乗法、単位元、零元などを非論理記号として導入し、環の性質を論理式として記述する。可換性、整域性、体性といった性質は、それぞれ特定の文の形で捉えられることがある。
その結果、あるクラスの環が共通の理論を満たすか、逆に区別できるかといった問題が整理される。モデルに関する情報は、代数的性質の間の含意関係を論理の形で明確にする。
5.1.3 体論
体論では、位相ではなく代数的構造の公理化が中心となる。体、素体、代数閉包に関わる性質などが言語で表され、それがモデルとしてどう実現されるかが検討される。
特に、特定の量化範囲でどこまで性質が決まるか、あるいは拡大でどの性質が保存されるかといった問いが自然に出てくる。超準や安定性の枠組みも、この種の分類に関与することがある。
5.2 幾何学への応用
5.2.1 定義可能集合
幾何学的対象を座標付けし、その上で定義可能な集合を考えると、モデル理論は「論理式で記述できる形」を分類の軸にできる。定義可能集合は、パラメータを用いた式によって記述され、構造の内部でどのように現れるかが追跡される。
この観点では、幾何の直観を論理的な構造として捉え、定義可能性や分類可能性に基づく整理が行われる。特に、安定性理論や幾何学的安定性の発想が橋渡しになることがある。
5.2.2 幾何構造の分類
モデル理論は、幾何構造がどの程度まで論理的に区別されるかを考えるためにも使われる。対象の族を言語で記述し、その理論のモデルとして分類することで、幾何学的な不変量や同値類が論理の用語に翻訳される。
また、位相や連続性の性質を直接扱うのは難しい場合が多いが、代数的に記述可能な枠（たとえば多項式方程式の系）では、理論的分類が現れやすい。結果として、代数幾何との連携が強まる。
5.3 計算機科学への応用
5.3.1 論理プログラミング
論理プログラミングでは、ルールや述語を論理式として捉え、問い合わせに対する充足や導出を計算機で実行する。モデル理論は、どの仕様がどの構造で満たされるかという意味論的理解を与え、プログラムの正しさ検討に寄与しうる。
特に、断片的な論理言語で記述した仕様が、どの程度まで一意な挙動を保証するか、という観点で役立つことがある。計算の手続きと、論理的意味の対応を整理するための理論資源となる。
5.3.2 形式検証
形式検証では、システム仕様と設計の振る舞いを形式言語で記述し、満足や非矛盾の形で保証する。モデル理論の枠組みは、論理式が表す性質が、モデルとしてどう現れるかを理解する助けになる。
また、有限モデル理論は有限状態の系との親和性が高い。仕様の記述能力と検証可能性の関係を理論的に見通すことで、検証手法の設計や限界評価に繋がる。
5.4 組合せ論との関係
5.4.1 構造の制約
組合せ論では、有限の離散構造を対象として、満たすべき制約を研究することが多い。有限モデル理論の視点から見ると、制約は論理文として記述でき、その充足がどのように現れるかが整理される。
このとき、論理式の表現能力が、組合せ構造の作り方や不可能性の証明の形に影響する。有限性を強制した枠での推論は、組合せ論の問題設定と相性がよい。
5.4.2 離散数学への影響
モデル理論が離散数学へ与える影響としては、分類や定義可能性の概念が挙げられる。離散構造の性質がどの言語断片で表現できるかを明確にすることで、問題の難しさを論理の言葉で比較できる。
さらに、論理と計算量の対応を通じて、組合せ問題に対するアルゴリズム的観点が入りやすくなる。これにより、構造の制約と計算の限界を同じ視点で扱う道が開ける。
6 研究手法
6.1 省略記法
省略記法とは、形式的に書けば長くなる論理式や記号列を、慣習に従って簡潔に表す工夫である。たとえば量化子や括弧の整理、集合や変数の省略などが含まれる。
省略記法は読みやすさを高める一方、曖昧さを避けるために厳密な規約が必要になる。モデル理論では、どの変数が自由か、どの量化がかかっているかが本質なので、表記の管理は理論の厳密性に直結する。
6.2 逐語的構成
逐語的構成は、理論やモデルの条件を、論理式の形に沿って段階的に満たしていく構成法を指す。特に、コンパクト性と相性が良い場合が多く、有限部分の充足から全体を得るための枠組みとして現れる。
具体的には、満足すべき文集合の拡張や、整合性を保ちながら条件を追加していく作業が中心になる。この方法により、モデルの存在だけでなく、その内部の構造的特徴を引き出す方向へ進めることがある。
6.3 解釈可能性
解釈可能性は、ある構造を別の言語・別の理論の枠で表現できるか、あるいは一方の対象が論理的に再構成できるかを問う概念である。通常、対象の要素や関係を、別の構造上の定義から作り直す手続きが問題となる。
この観点は、理論同士の関係を分類する道具にもなる。あるクラスの構造が別のクラスの理論により「論理的に含まれる」なら、性質の移送が可能になる。
6.4 定義可能性
定義可能性は、ある性質や集合が論理式で記述できるかどうかを研究する中心概念である。一般に、どの論理言語（あるいはどの断片）で記述可能かが問題になる。
定義可能性はモデル間での不変性とも密接である。ある集合が特定の論理式で定義できるなら、同型な構造では同じように現れる。加えて、安定性理論の文脈では、定義可能な対象の整理や分類がより強い形で得られることがある。
7 歴史
7.1 起源
モデル理論の萌芽は、論理と数学的構造の橋渡しを志向した19世紀末から20世紀初頭の流れに見いだせる。特に、形式論理の整備と、数学的推論を記号化する動きが背景にある。
また、意味論的な視点から「理論がどの構造で成立するか」を捉える発想が次第に明確化していった。形式体系の証明可能性だけでなく、解釈のもとでの真理を研究する必要が意識されるようになった。
7.2 発展
発展期には、一階論理における完全性やコンパクト性のような原理的定理が確立され、モデル理論が体系として立ち上がった。これにより、意味論的な性質を普遍的な原理で扱えるようになった。
その後、同型・同値性の観点や、型（タイプ）と呼ばれる情報の統一的扱いが整備され、分類問題を解くための道具が増えた。安定性理論や超準モデル理論といった大きな枝分かれも、この流れの中で生まれる。
7.3 現代的展開
現代では、古典的な一階モデル理論に加えて、安定性理論、有限モデル理論、超準モデル理論、さらにはより一般の枠組みへの拡張が並行して研究されている。計算機科学との結びつきも一段と強まり、論理で書けることと計算でできることの対応が積極的に追究される。
また、幾何学や代数学との連携も深く、定義可能性や分類を軸にした研究が盛んである。論理的手法を用いて数学の対象を再整理する潮流は、多方面へ広がっている。
7.4 主要研究者
モデル理論には、多数の研究者が貢献している。歴史的には、完全性やコンパクト性に関わる基礎定理の確立に関与した研究者、超準的手法の発展に寄与した研究者、安定性理論を体系化した研究者などが挙げられる。
また、有限モデル理論や計算理論との対応を作り上げた研究者も重要な役割を果たしている。分野ごとに重点領域が異なるため、主要研究者の並びは研究テーマに応じて変化する。
8 関連項目
8.1 数理論理学
数理論理学は、形式論理や計算可能性、集合論的枠組みなどを含む論理学全般の領域である。モデル理論はその中で、意味論と構造の関係を軸に発展してきた分野として位置づけられる。
相互参照として、証明論や集合論、計算理論との接点が常に意識され、定理の成立条件や言語の選択が研究の方向性を左右する。
8.2 集合論
集合論は数学の基礎に近い位置を持ち、濃度や可算性といった概念を支える。モデル理論では、モデルの大きさや構成の可能性に集合論的な側面が関わることが多い。
また、超準拡大やコンパクト性を利用する際にも、集合論的手法が背後に必要になる場合がある。
8.3 証明論
証明論は形式体系における証明可能性を構文的に研究する。モデル理論との関係では、完全性定理のように、証明可能性と満足の関係が重要な接点になる。
さらに、モデル理論が扱う意味論的概念を、証明論の枠でどの程度反映できるかという観点が、研究上の橋渡しとなる。
8.4 計算理論
計算理論は計算可能性や計算複雑性を扱う。有限モデル理論や論理プログラミング、形式検証の領域では、論理式で記述できる性質が計算可能な範囲に対応するかが中心問題となる。
このため、モデル理論の言語能力と計算上の限界の関係を理解することが、相互の発展を促している。