トラクテンブロートの定理

論理学、有限モデル理論、および計算可能性理論において、トラクテンブロートの定理（ボリス・トラクテンブロートによる）は、 すべての有限モデルのクラス上の一階述語論理の妥当性の問題は決定不可能であると述べている。実際、有限モデル上の妥当な文のクラスは再帰的に列挙可能ではない（ただし、共再帰的に列挙可能である）。

トラクテンブロートの定理は、ゲーデルの完全性定理（一階述語論理の基礎）が有限の場合には成り立たないことを意味します。また、すべての構造に対して有効であることは有限の構造に対して有効であることよりも「簡単」であるというのは直感に反しているように思われます。

この定理は1950年に初めて発表された：「有限クラス上の決定可能性問題に対するアルゴリズムの不可能性」^{[1] 。}

^{エビングハウスとフラム[2]}の定式化に従う。

有限構造の充足可能性は、一階述語論理では決定できません。

つまり、集合 {φ | φ はすべての有限構造によって満たされる一階述語論理の文である} は決定不可能である。

σ を少なくとも 1 つの 2 項関係記号を持つ関係語彙とします。

すべての有限構造において有効な σ 文の集合は再帰的に列挙可能ではありません。

備考

1. これは、完全性は再帰的可算性を意味するため、ゲーデルの完全性定理が有限では成立しないことを意味します。
2. したがって、次のような再帰関数 f は存在しません: φ が有限モデルを持つ場合、そのモデルのサイズは最大で f(φ) です。言い換えれば、有限の場合、レーヴェンハイム-スコーレムの定理に有効な類似物は存在しません。

この証明は、H.-D. エビングハウス著『数理論理学』第 10 章、セクション 4、5 から引用したものです。

停止問題の決定不能性 を用いたゲーデルの第一不完全性定理の最も一般的な証明と同様に、各チューリングマシンには、 が空のテープ上で停止する場合にのみ真となる、から効果的に導出可能な対応する算術文 があります。直感的に、は「停止で終わる空のテープ上の の計算記録のゲーデルコードである自然数が存在する」と主張しています。 ${\displaystyle M}$${\displaystyle \phi _{M}}$${\displaystyle M}$${\displaystyle M}$${\displaystyle \phi _{M}}$${\displaystyle M}$

マシンが有限ステップで停止する場合、完全な計算記録も有限であり、算術文もこの初期セグメントで真となるような自然数の有限初期セグメントが存在します。直感的に言えば、この場合、証明には有限数の数の算術特性のみが必要である ためです。${\displaystyle M}$${\displaystyle \phi _{M}}$${\displaystyle \phi _{M}}$

マシンが有限ステップで停止しない場合は、停止で終わる 有限の計算記録が存在しないため、任意の有限モデルでは は偽になります。${\displaystyle M}$${\displaystyle \phi _{M}}$${\displaystyle M}$

したがって、 が停止する場合、は一部の有限モデルでは真です。が停止しない場合、はすべての有限モデルで偽です。 したがって、 がすべての有限モデルで真である場合に限り、 は停止しません。 ${\displaystyle M}$${\displaystyle \phi _{M}}$${\displaystyle M}$${\displaystyle \phi _{M}}$${\displaystyle M}$${\displaystyle \neg \phi _{M}}$

停止しないマシンの集合は再帰的に列挙可能ではないため、有限モデル上の有効な文の集合も再帰的に列挙可能ではありません。

このセクションでは、Libkinによるより厳密な証明を示します。^[3]上記の記述では、系も定理を伴っており、これがここで証明する方向であることに注意してください。

定理

少なくとも1つの2項関係記号を持つすべての関係語彙τについて、語彙τの文φが有限満足可能かどうかは決定できません。

証拠

前の補題によれば、実際には有限個の二項関係記号を使用できます。証明の考え方はフェイギンの定理の証明に似ており、チューリング マシンを一階論理でエンコードします。証明したいのは、すべてのチューリング マシン M に対して、語彙 τ の文 φ _{M を構築し、M が空の入力で停止する場合に限り φ M が}有限に満足可能であることです。これは停止問題と同等であり、したがって決定不可能です。

M = ⟨Q, Σ, δ, q ₀ , Q _a , Q _r ⟩ を単一の無限テープを持つ決定論的チューリングマシンとします。

• Qは状態の集合であり、
• Σは入力アルファベットです。
• Δはテープのアルファベットです。
• δは遷移関数であり、
• q _{0 は}初期状態であり、
• Q _aと Q _{r は}、受け入れ状態と拒否状態の集合です。

空の入力で停止する問題を扱っているので、Δ={0,1} であり、0 は空白を表し、1 はテープ記号を表すと仮定できます。計算を表現できるように τ を定義します。

τ := {<, min , T ₀ (⋅,⋅), T ₁ (⋅,⋅), (H _q (⋅,⋅)) _{(q ∈ Q)} }

どこ：

• < は線形順序であり、min は< に関する最小要素を表す定数記号です (有限領域は自然数の最初のセグメントに関連付けられます)。
• T ₀と T _{1 は}テープ述語です。T _i (s,t) は、時刻 t の位置 s に i が含まれることを示します。ここで、i ∈ {0,1} です。
• H _qはヘッド述語です。H _q (s,t) は、時刻 t にマシンが状態 q にあり、ヘッドが位置 s にあることを示します。

文 φ _{M は}、(i) <、min、T _iおよび H _qが上記のように解釈され、(ii) マシンが最終的に停止することを述べています。停止条件は、H _{q∗ (s, t) がいくつかの s、t、q∗ ∈ Q a} ∪ Q _rに対して成り立ち、その状態の後、マシンの構成は変化しないと言うことと同等です。停止マシンの構成 (非停止は有限ではありません) は、τ (有限) 文 (より正確には、文を満たす有限の τ 構造) として表すことができます。文 φ _Mは、φ ≡ α ∧ β ∧ γ ∧ η ∧ ζ ∧ θ です。

コンポーネントごとに分類します。

• αは、<が線形順序であり、minがその最小元であることを示す。
• _{γ は M の初期構成を定義します。つまり、状態 q 0}にあり、ヘッドは最初の位置にあり、テープにはゼロのみが含まれています。 γ ≡ H _{q 0} ( min , min ) ∧ ∀s T ₀ (s, min )
• ηは、Mのあらゆる構成において、各テープセルにΔの要素が1つだけ含まれることを示しています: ∀s∀t(T ₀ (s, t) ↔ ¬ T ₁ (s, t))
• _{βは述語H q}に基本的な一貫性条件を課す。つまり、マシンは常に1つの状態にあるということである。

${\displaystyle \forall t\exists !s(\bigvee _{q\in Q}H_{q}(s,t))\land \neg \exists s\exists t(\bigvee _{q,q'\in Q,q\neq q}H_{q}(s,t)\land H_{q'}(s,t))}$

• ζは、ある時点でMが停止状態にあることを示しています。

${\displaystyle \exists s\exists t\bigvee _{q\in Q_{a}\cup Q_{r}}H_{q}(s,t)}$

• _{θ は、T i}と H _qが M の遷移に関して適切に動作することを示す文の連言で構成されています。例として、δ(q,0)=(q',1, left) とすると、M が状態 q で 0 を読み取っていたら、1 を書き込み、ヘッドを 1 つ左に移動して状態 q' に移行することを意味します。この状態は、θ 0_とθ ₁の論理和で表されます。

${\displaystyle \theta _{0}\equiv \forall s\forall t(s\neq {\underline {min}}\land T_{0}(s,t)\land H_{q}(s,t))\to \theta _{2}}$

ここでθ ₂は:

${\displaystyle T_{1}(s,t+1)\land H_{q'}(s-1,t+1)\land \forall s'(s\neq s'\to (\bigwedge _{i=0,1}T_{i}(s',t+1)\leftrightarrow T_{i}(s',t)))}$

そして：

${\displaystyle \theta _{1}\equiv \forall s\forall t(s={\underline {min}}\land T_{0}(s,t)\land H_{q}(s,t))\to \theta _{3}}$

ここでθ ₃は:

${\displaystyle T_{1}(s,t+1)\land H_{q'}(s,t+1)\land \forall s'(s\neq s'\to (\bigwedge _{i=0,1}T_{i}(s',t+1)\leftrightarrow T_{i}(s',t)))}$

s-1 と t+1 は、順序 < に従った先行処理と後続処理の 1 次定義可能略語です。文 θ ₀は、位置 s のテープの内容が 0 から 1 に変化し、状態が q から q' に変化し、テープの残りの部分は同じままで、ヘッドが s-1 (つまり、1 つ左の位置) に移動することを保証します (s がテープの最初の位置ではないと仮定した場合)。最初の位置である場合、すべては θ ₁によって処理されます。つまり、ヘッドが左に移動せずにその位置に留まる以外はすべて同じです。

φ _Mに有限モデルがある場合、そのようなモデルは M の計算（空のテープ（つまり、すべてゼロのテープ）で始まり、停止状態で終了する）を表す。 M が空の入力で停止する場合、 M の停止計算のすべての構成の集合（<、T _i、および H _{qでコード化される）は φ M}のモデルであり、これは有限である。これは、停止計算のすべての構成の集合が有限であるためである。したがって、 φ _{M が有限モデルを持つ場合と同値である。空の入力で停止することは決定不可能であるため、 φ M}に有限モデルがあるかどうか（つまり、 φ _Mが有限に満足可能かどうか）という質問も決定不可能である（再帰的に列挙可能であるが、再帰的ではない）。これで証明は終了である。 ${\displaystyle {\mathcal {A}}}$

帰結

有限満足可能な文の集合は再帰的に列挙可能である。

証拠

が有限であり、であるすべてのペアを列挙します。 ${\displaystyle ({\mathcal {A}},\phi )}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}\models \phi }$

帰結

少なくとも 1 つの 2 項関係記号を含む語彙の場合、有限に有効なすべての文の集合は再帰的に列挙できません。

証拠

前の補題から、有限満足可能な文の集合は再帰的に列挙可能である。有限に有効なすべての文の集合が再帰的に列挙可能であると仮定する。¬φ が有限に有効である場合、φ は有限に満足可能でない場合と同数なので、有限に満足可能でない文の集合は再帰的に列挙可能であると結論付けられる。集合 A とその補集合の両方が再帰的に列挙可能である場合、A は再帰的である。したがって、有限に満足可能な文の集合は再帰的であり、これは Trakhtenbrot の定理と矛盾する。

• Boolos、Burgess、Jeffrey。計算可能性と論理、ケンブリッジ大学出版局、2002年。
• シンプソン、S.「チャーチとトラクテンブロートの定理」2001年[1]