モデル理論: 決定可能性および量限定子消去

ウィキペディア小見出し辞書

モデル理論: 決定可能性および量限定子消去

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/11/17 02:16 UTC 版)

「実閉体」の記事における「モデル理論: 決定可能性および量限定子消去」の解説

実閉体の理論は初めは代数学の中で発展したものだけれども、重要な示唆はモデル理論からもたらされた。順序体の公理系に 任意の正元が平方根を持つことを要請する公理 任意の奇数次多項式が少なくとも一つの根を持つことを要請する公理図式 を加えることにより、一階の理論が得られる。Tarski (1951) は、半順序環（英語版）に関する一階の言語（二項述語記号 "=", "≤", 加法、減法、乗法の演算および定数記号 0, 1 からなる）において、実閉体の理論が 量限定子消去（英語版）を許すことを示した。このことのもっとも重要なモデル理論的帰結は、実閉体の理論が完全（英語版）、o-極小（英語版）かつ決定可能なることである。 決定可能性が意味するのは少なくとも一つの決定手順が存在すること、すなわち実閉体に関する一階言語で書かれた文が真であるかどうかを決定するためのwell-definedなアルゴリズムが存在することである。ユークリッド幾何学（角度の決定可能性は除く）もまた実体の公理のモデルであって、したがって決定可能である。 この決定手順が「実用的」であるかは問わない。実閉体に対する決定手順は何れも計算量が極めて大きいことが知られているから、非常に単純な問題を除けば実際の実行時間は極めて長くなりうる。 タルスキーのアルゴリズムは量限定子消去（英語版）が複雑性クラス NONELEMENTARY（英語版） に属する可能性を示唆している。つまり、問題の大きさを n とするとき、アルゴリズムの実行時間を上から評価するような冪の塔 2 2 ⋅ ⋅ ⋅ n {\textstyle 2^{2^{\,\cdot ^{\,\cdot ^{\,\cdot ^{\,n}}}}}} は存在しない。Davenport & Heintz (1988) は量限定子消去が実は（少なくとも）二重指数的であることを示した。つまり、Ω 漸近記法を用いれば、n 個の量限定子を持つ式の族 Φn で長さ O(n) のものと一定の次数が存在して、Φn に同値な量限定子を持たない任意の式が次数 22Ω(n) かつ長さ 22Ω(n) の多項式を必ず含む。Ben-Or, Kozen & Reif (1986) は実閉体の理論が EXPSPACE において（したがって二重指数時間で）決定可能であることを示した。 Basu and Roy (1996)[要文献特定詳細情報] は ∃x1, …, ∃xk; P1(x1, …, xk) ⋈ 0 ∧ ⋯ ∧ Ps(x1, …, xk) ⋈ 0 なる式（ただし、⋈ は "<", ">", "=" の何れか）が真かを決定するためのよく振る舞うアルゴリズムで、算術演算 sk+1dO(k) の複雑性に属するものが存在することを示した。実は実数の存在理論（英語版）は PSPACE で決定できる。 追加の函数記号（例えば正弦函数 sin や指数函数 exp）を加えて、理論の決定可能性を変更（英語版）することができる。 まだほかにも、実閉体の重要なモデル理論的性質として、それが弱 o-極小構造（英語版）を持つことが挙げられる。逆に、任意の弱 o-極小順序体は実閉でなければならない。