有限モデル理論

有限モデル理論は、モデル理論の一分野です。モデル理論は、形式言語（構文）とその解釈（意味論）の関係を扱う論理学の一分野です。有限モデル理論は、有限な宇宙を持つ有限構造に対する解釈にモデル理論を限定したものです。

モデル理論の多くの中心的な定理は有限構造に限定すると成り立たないため、有限モデル理論は証明方法においてモデル理論とはかなり異なっている。有限モデル理論の下で有限構造に対して成り立たない古典モデル理論の中心的な結果には、コンパクト性定理、ゲーデルの完全性定理、および一階述語論理（FO）の超積法が含まれる。これらの不成立はすべてトラクテンブロートの定理から導かれる。^{[ 1 ]}

モデル理論は数学代数に多くの応用がある一方で、有限モデル理論はコンピュータ科学において「非常に効果的な」^{[ 2 ]}ツールとなった。言い換えれば、「数学論理の歴史において、ほとんどの関心は無限構造に集中してきた。[...] しかし、コンピュータが持つ対象は常に有限である。計算を研究するには、有限構造の理論が必要である。」^{[ 3 ]} したがって、有限モデル理論の主な応用分野は、記述的複雑性理論、データベース理論、形式言語理論である。

有限モデル理論における一般的な問いの一つは、ある構造のクラスを特定の言語で記述できるかどうかである。例えば、循環グラフのクラスをFO文で他のグラフと区別できるかどうかを問うことができる。これは、循環性がFOで表現可能かどうかを問うという形で表現することもできる。

単一の有限構造は常に一階述語論理で公理化できる。ここで、言語Lで公理化するとは、同型を除いて単一のL文によって一意に記述されることを意味する。同様に、有限構造の任意の有限集合は常に一階述語論理で公理化できる。有限構造の無限集合の一部も、単一の一階述語論理文によって公理化できるが、すべてではない。

単一構造の特性評価

言語Lは、単一の有限構造Sを公理化するのに十分な表現力を持っているか？

問題

図中の（１）のような構造は、グラフの論理におけるFO 文によって記述できます。

1. すべてのノードは、他のノードへのエッジを持っています。${\displaystyle \forall _{x}\exists _{y}G(x,y).}$
2. どのノードも、自身へのエッジを持っていません。${\displaystyle \forall _{x,y}(G(x,y)\Rightarrow x\neq y).}$
3. 他のすべてのノードに接続されているノードが少なくとも1つ存在する。${\displaystyle \exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).}$

しかし、これらの性質は構造を公理化するものではありません。なぜなら、構造（1'）についても上記の性質が成り立つにもかかわらず、構造（1）と（1'）は同型ではないからです。

非公式には、十分な特性を追加することで、これらの特性がまとめて（1）を正確に記述し、かつ（すべてまとめて）他の構造に対して（同型を除いて）有効であるかどうかが問題です。

アプローチ

単一の有限構造であれば、常に単一のFO文でその構造を正確に記述することが可能です。ここでは、1つの二項関係を持つ構造を例に、その原理を説明します。${\displaystyle R}$そして定数を用いない。この目的のために、一次変数を導入する。${\displaystyle x_{1},\dots ,x_{n}}$と解釈される${\displaystyle n}$構造の要素。次に、以下の4つの式を紹介します。

1. ${\displaystyle \varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})}$少なくとも${\displaystyle n}$要素;
2. ${\displaystyle \varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)}$最大で${\displaystyle n}$要素;
3. ${\displaystyle \varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})}$関係のすべてのエッジを記述します${\displaystyle R}$;
4. ${\displaystyle \varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})}$関係のすべての非エッジを記述する${\displaystyle R}$。

最後に、構造はFO文によって記述される。$\displaystyle \exists _{x_{1}}\dots \exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})}$。

固定数の構造物への拡張

単一の有限構造を一階述語論理式で記述する方法は、任意の固定数の構造にも容易に拡張できる。各構造の記述を論理和で結ぶことにより、一意の記述が得られる。例えば、2つの有限構造の場合${\displaystyle A}$そして${\displaystyle B}$定義文付き$\displaystyle \varphi _{A}}$そして$\displaystyle \varphi _{B}}$これは

${\displaystyle \varphi _{A}\lor \varphi _{B}.}$

無限構造への拡張

定義上、無限構造を含む集合は、FMTが扱う領域外となる。レーヴェンハイム・スコレムの定理により、無限構造はFOでは区別できないことに注意されたい。この定理は、無限モデルを持つ一階理論は、同型を除いて一意のモデルを持つことができないことを意味する。

最も有名な例はおそらくスコレムの定理だろう。それは、算術には可算な非標準モデルが存在するという定理である。

構造クラスの特性評価

言語Lは、特定の性質Pを持つ有限構造を（同型を除いて）正確に記述するのに十分な表現力を持っているか？

問題

これまで述べてきた記述はすべて、宇宙を構成する要素の数を明示している。しかし残念ながら、興味深い構造の集合の多くは、木構造を持つグラフ、連結グラフ、非巡回グラフといった特定のサイズに限定されない。したがって、有限個の構造を識別することは特に重要である。

アプローチ

一般的な説明ではなく、以下では、区別可能な構造と区別不可能な構造を区別するための方法論の概要を示す。

1. 基本的な考え方は、ある性質P がFO で表現できるかどうかを確認したい場合、構造AとBを選択する。ここで、AはPを持ち、B はPを持たない。A と B で同じ FO 文が成り立つ場合、PはFOで表現できない。要するに、

   ${\displaystyle A\in P,B\not \in P}$そして${\displaystyle A\equiv B,}$

   どこ${\displaystyle A\equiv B}$は略語です${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$すべての FO 文αに対して、P は特性Pを持つ構造のクラスを表します。
2. この手法では、言語の可算個の部分集合を考慮し、それらの和集合が言語自体を形成する。例えば、FO の場合、各mに対してクラス FO[ m ] を考える。各mに対して、上記の中心的な考え方を示す必要がある。すなわち、次のようになる。

   ${\displaystyle A\in P,B\not \in P}$そして${\displaystyle A\equiv _{m}B}$

   ペアで${\displaystyle A,B}$各${\displaystyle m}$そしてα (≡ 内) は FO[ m ] から取られます。クラス FO[ m ] を選択して言語の分割を形成することが適切かもしれません。
3. FO[ m ]を定義する一般的な方法の 1 つは、量化子の入れ子の深さを表すFO 式αの量化子ランクqr( α )を用いることです。たとえば、前置標準形の式の場合、qr は単純にその量化子の総数になります。この場合、FO[ m ] はqr( α ) ≤ mとなるすべての FO 式αとして定義できます (または、分割が必要な場合は、量化子ランクがmに等しい FO 式として定義できます)。
4. つまり、すべては示すことに尽きる${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$部分集合 FO[ m ] 上で。ここでの主なアプローチは、エーレンフォイヒト-フレッセ ゲームによって提供される代数的特徴付けを使用することです。非公式には、これらはAとB上の単一の部分同型を取り、それをm回拡張して、証明または反証します。${\displaystyle A\equiv _{m}B}$試合の勝者によって異なる。

例

順序構造A = (A, ≤)のサイズが偶数であるという性質は FO では表現できないことを示したい。

1. アイデアは、A ∈ EVENかつB ∉ EVENを選択することです。ここで、EVEN は偶数サイズのすべての構造のクラスです。
2. _{まず、A 2} = {1, 2, 3, 4} および B ₂ = {1, 2, 3}のユニバースを持つ2 つの順序構造A ₂およびB ₂から始めます。明らかにA ₂ ∈ EVENであり、B ₂ ∉ EVEN です。
3. m = 2の場合、 A ₂とB ₂上の2 手エーレンフォイヒト–フレッセ ゲームでは、複製者が常に勝つため、A ₂とB _{2 は}FO[2] で区別できません。$\displaystyle \mathbf {A} _{2}\models \alpha \iff \mathbf {B} _{2}\models \alpha }$すべてのα ∈ FO[2]に対して。
4. 次に、 mを増やして構造をスケールアップする必要があります。たとえば、m = 3の場合、複製者が 3 手ゲームで常に勝つようなA ₃とB _{3を見つける必要があります。これは、A 3} = {1, ..., 8} および B _{3 = {1, ..., 7} で実現できます。より一般的には、A m} = {1, ..., 2 ^m } および B _m = {1, ..., 2 ^m − 1}を選択できます。任意のmに対して、この構造のペアでは複製者が常にm手ゲームで勝ちます *。
5. したがって、有限順序構造であっても、FO で表現することはできません。

Glebskiĭ ら (1969)と、独立に Fagin (1976) は、有限モデルにおける一階述語論理のゼロイチ法則を証明した。Fagin の証明はコンパクト性定理を用いた。この結果によれば、関係シグネチャにおけるすべての一階述語論理はゼロイチ法則を満たす。${\displaystyle \sigma }$有限では、ほぼ常に真であるか、ほぼ常に偽であるかのどちらかである。${\displaystyle \sigma }$-構造。つまり、Sを固定された一階述語論理文とし、ランダムに${\displaystyle \sigma }$-構造${\displaystyle G_{n}}$ドメイン付き${\displaystyle \{1,\dots ,n\}}$すべてにおいて均一に${\displaystyle \sigma }$ドメインを持つ構造${\displaystyle \{1,\dots ,n\}}$そして、 nが無限大に近づく極限では、 G _nモデルSとなる確率はゼロまたは1のいずれかに近づく。

${\displaystyle \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.}$

与えられた文の確率がゼロに近づくか1に近づくかを判定する問題はPSPACE完全である。^{[ 4 ]}

同様の解析は、一階述語論理よりも表現力の高い論理体系に対しても行われている。0-1法則は、最小不動点演算子で拡張された一階述語論理であるFO(LFP)の文、そしてより一般的には無限論理の文に対して成り立つことが示されている。${\displaystyle L_{\infty \omega }^{\omega }}$これにより、潜在的に任意の長さの論理積と論理和が可能になります。もう1つの重要な変種はラベルなし0-1法則で、ドメインを持つ構造の割合を考慮する代わりに、${\displaystyle \{1,\dots ,n\}}$n個の要素を持つ構造の同型クラスの割合を考察する。任意の 2 つの同型構造が同じ文を満たすため、この割合は明確に定義される。ラベルなし 0-1 法則は、${\displaystyle L_{\infty \omega }^{\omega }}$したがって、特に FO(LFP) および一階述語論理の場合に当てはまります。^{[ 5 ]}

有限モデル理論の重要な目標の一つは、複雑性クラスを、そのクラスに含まれる言語を表現するために必要な論理の種類によって特徴づけることである。例えば、多項式階層におけるすべての複雑性クラスの和集合であるPHは、まさに二階述語論理の命題によって表現可能な言​​語のクラスである。複雑性と有限構造の論理とのこのつながりにより、結果を一方の領域から他方の領域へ容易に転用することが可能になり、新たな証明方法の開発を促進するとともに、主要な複雑性クラスが何らかの形で「自然」であり、それらを定義するために使用される特定の抽象機械に縛られていないことを示す追加的な証拠を提供する。

具体的には、各論理システムは、そのシステム内で表現可能な一連のクエリを生成する。これらのクエリは、有限構造に限定した場合、従来の計算複雑性理論における計算問題に対応する。

よく知られているいくつかの複雑性クラスは、論理言語によって以下のように表現されます。

• 線形順序が存在する場合、可換かつ推移的な閉包演算子を追加した一階述語論理は、対数空間で解ける問題であるLを生成します。
• 線形順序が存在する場合、推移閉包演算子を持つ一階述語論理は、非決定性対数空間で解ける問題であるNLを生成する。
• 線形順序が存在する場合、最小不動点演算子を持つ一階述語論理は、決定論的多項式時間で解ける問題であるPを与える。
• すべての有限構造（順序付けされているかどうかに関わらず）において、存在二階述語論理はNPを与える（フェイギンの定理）。^{[ 6 ]}

• Trakhtenbrot 1950: failure of completeness theorem in first-order logic
• Scholz 1952: characterisation of spectra in first-order logic
• Fagin 1974: the set of all properties expressible in existential second-order logic is precisely the complexity class NP
• Chandra, Harel 1979/80: fixed-point first-order logic extension for database query languages capable of expressing transitive closure -> queries as central objects of FMT
• Immerman, Vardi 1982: fixed-point logic over ordered structures captures PTIME -> descriptive complexity (Immerman–Szelepcsényi theorem)
• Ebbinghaus, Flum 1995: first comprehensive book "Finite Model Theory"
• Abiteboul, Hull, Vianu 1995: book "Foundations of Databases"
• Immerman 1999: book "Descriptive Complexity"
• Kuper, Libkin, Paredaens 2000: book "Constraint Databases"
• Darmstadt 2005/ Aachen 2006: first international workshops on "Algorithmic Model Theory"

• エビングハウス、ハインツ・ディーター;フルム、ヨルグ (1995)。有限モデル理論。スプリンガー。ISBN 978-3-540-60149-4。

• Fagin, Ronald (1976). 「有限モデル上の確率」。『記号論理学ジャーナル』41 (1): 50–58。doi : 10.2307 / 2272945。JSTOR 2272945。 
• グレブスキー、ユウ V.ディリノイ州コーガン。ミシガン州リオゴンキイ。バージニア州タラノフ (1969)。 "Объем и доля выполнимости формул узкого исчисления предикатов" [一次述語計算の式の充足可能性の体積と割合]。キベルネティカ。5 (2)：17～ 27。また、 「制限述語論理における式の実現可能性の範囲と程度」としても入手可能。サイバネティクス。5 （ 2）：142–154。1972年。doi：10.1007/BF01071084。
• リブキン、レオニード（ 2004）。有限モデル理論の基礎。シュプリンガー。ISBN 3-540-21202-7。

• アビテブール、セルジュ；ハル、リチャード；ヴィアヌ、ヴィクター（1995）。データベースの基礎。アディソン・ウェスリー。ISBN 0-201-53771-0。

• イマーマン、ニール（1999）。記述的複雑性。ニューヨーク：スプリンガー。ISBN 0-387-98600-6。

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007).有限モデル理論とその応用. 理論計算機科学テキストシリーズ. EATCSシリーズ. ベルリン: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 . 

• Libkin, Leonid (2009). 「データベース理論家の有限モデル理論ツールボックス」. PODS 2009: 第28回 ACM SIGACT–SIGMOD データベースシステムの原理に関するシンポジウム議事録. pp. 65–76 . doi : 10.1145/1559795.1559807 .  一般的な入門書や概要としても適しています。
• レオニード・リブキン著。『有限モデル理論の要素』の序章。 2015年9月24日にWayback Machineにアーカイブ済み。データベース、複雑性、形式言語という3つの主要な応用分野について論じている。
• ヨーコ・ヴァアナネン。有限モデル理論に関する短期コース。ヘルシンキ大学数学学部。 1993年から1994年にかけての講義を基にしたもの。
• Anuj Dawar。「無限および有限モデル理論」、スライド、ケンブリッジ大学、2002年。
• 「アルゴリズムモデル理論」。アーヘン工科大学。2012年7月17日時点のオリジナルからアーカイブ。 2013年11月7日取得。未解決のFMT問題の一覧が含まれています。