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

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

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

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

この定理は、第一階述語論理における有効な式の集合は決定可能ではない（ただし、この集合は半決定可能である）というチャーチの結果に関連している。

数学的定式化

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

定理

有限構造の満足度は第一階述語論理では決定できません。

つまり、{φ | φはある有限構造で満たされる一階述語論理の文である}という集合は決定不可能である。(p. 127, Th. 7.2.1 in ^[2] )

推論

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

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

備考

これは、完全性は再帰的列挙可能性を意味するため、ゲーデルの完全性定理が有限では成立しないことを意味します。
したがって、φ が有限のモデルを持つならば、そのモデルの大きさは最大で f(φ) となるような再帰関数 f は存在しない。言い換えれば、有限な関数においてはレーヴェンハイム・スコーレムの定理に類似するものは存在しない。

直感的な証明

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

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

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

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

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

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

代替証明

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

定理

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

証拠

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

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

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

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

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

どこ：

< は線形順序であり、minは < に関する最小要素の定数記号です (有限領域は自然数の最初のセグメントに関連付けられます)。
T ₀と T ₁はテープ述語です。Ti (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 ₀で、ヘッドは最初の位置にあり、テープにはゼロのみが含まれています。γ ≡ H _{q ₀} ( min , min ) ∧ ∀s T ₀ (s, min )
ηは、Mのあらゆる構成において、各テープセルにはΔの要素が1つだけ含まれることを示しています: ∀s ∠t(T ₀ (s, t) ↔ ¬ T ₁ (s, t))
_{βは述語H q}に基本的な一貫性条件を課す。つまり、マシンは常に1つの状態にあるということである。

\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が停止状態にあることを示します。

\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' に移行することを意味します。この条件は、θ ₀と θ ₁の論理和で表されます。

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

ここでθ ₂は次式で表される。

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)))

そして：

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

ここでθ ₃は次式で表される。

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

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

推論

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

証拠

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

推論

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

証拠

前の補題から、有限充足文の集合は再帰的に可算である。有限的に妥当な文全体の集合が再帰的に可算であると仮定する。¬φ が有限的に妥当であるのは、φ が有限充足可能でない場合のみであるので、有限的に充足可能でない文の集合は再帰的に可算であると結論付けられる。集合 A とその補集合の両方が再帰的に可算である場合、A は再帰的である。したがって、有限的に充足可能な文の集合は再帰的であり、これはトラクテンブロートの定理と矛盾する。

参考文献

^ トラクテンブロート, ボリス(1950). 「有限クラスにおける決定可能性問題に対するアルゴリズムの不可能性」.ソ連科学アカデミー紀要(ロシア語). 70 (4): 569– 572.
^ ab エビングハウス、ハインツ＝ディーター;フルム、ヨルグ (1995)。有限モデル理論。シュプリンガーサイエンス+ビジネスメディア。ISBN 978-3-540-60149-4。
^ Libkin, Leonid (2010). 『有限モデル理論の要素』 .理論計算機科学テキスト. ISBN 978-3-642-05948-3。

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

[1] トラクテンブロート, ボリス(1950). 「有限クラスにおける決定可能性問題に対するアルゴリズムの不可能性」.ソ連科学アカデミー紀要(ロシア語). 70 (4): 569– 572.

[:0-2] エビングハウス、ハインツ＝ディーター;フルム、ヨルグ (1995)。有限モデル理論。シュプリンガーサイエンス+ビジネスメディア。ISBN 978-3-540-60149-4。

[3] Libkin, Leonid (2010). 『有限モデル理論の要素』 .理論計算機科学テキスト. ISBN 978-3-642-05948-3。