Trakhtenbrot的定理

邏輯有限模型理論可計算理論中, Trakhtenbrot的定理(由於Boris Trakhtenbrot )指出,所有有限模型的類別的一階邏輯中的有效性問題是不可確定的。實際上,有限模型上的有效句子類別並不是遞歸列舉的(儘管它是共同奪取的)。

Trakhtenbrot的定理意味著Gödel的完整性定理(對一階邏輯至關重要)在有限的情況下不存在。同樣,在所有結構上都比僅在有限的結構上“更容易”有效,這似乎是違反直覺的。

該定理於1950年首次出版:“有限類別的可定性問題的算法不可能”。

數學公式

我們遵循像ebbinghaus和flum中的配方

定理

一階邏輯中,有限結構的滿意度無法確定。
也就是說,集合{φ| φ是在有限結構中令人滿意的一階邏輯的句子。

推論

令σ為具有至少二進制關係符號的關係詞彙。

在所有有限結構中有效的σ句子集並非遞歸地枚舉

評論

  1. 這意味著Gödel的完整性定理在有限的情況下失敗,因為完整性意味著遞歸枚舉性。
  2. 因此,沒有遞歸函數f,因此:如果φ具有有限的模型,那麼它最多具有f(φ)的大小模型。換句話說,在有限的löwenheim -skolem定理中沒有有效的類似物。

直觀的證明

此證明摘自H.-D的數學邏輯第10章,第5章第5節。 Ebbinghaus。

就像戈德爾通過使用停止問題的不可證明的第一個不完整定理的最常見證明一樣,對於每台圖靈機器有一個相應的算術句子 ,有效地從 ,使得且僅當停在空膠帶上。直覺, 斷言“存在一個自然數字,這是Gödel的計算記錄的Gödel代碼在空的膠帶上停止。”

如果是機器是否在有限步驟中停止,然後完整的計算記錄也是有限的,那麼自然數的初始部分有限,以便算術句子在此初始細分市場上也是正確的。直覺上,這是因為在這種情況下,證明需要僅有限的數字的算術屬性。

如果是機器不會在有限步驟中停止在任何有限模型中都是錯誤的,因為沒有有限的計算記錄結束時停止。

因此,如果停頓在某些有限模型中是正確的。如果不停止, 在所有有限模型中都是錯誤的。所以, 當且僅當在所有有限模型上都是正確的。

一組不停止的機器無法遞歸地枚舉,因此在有限模型上的一組有效句子集不能遞歸地枚舉。

替代證明

在本節中,我們將展示Libkin的更嚴格的證據。請注意,上面的說法表明推論還需要定理,這是我們在這裡證明的方向。

定理

對於每個具有至少一個二進制關係符號的關係詞彙τ,詞彙τ的句子是否有限滿足是不可確定的。

證明

根據以前的引理,我們實際上可以使用有限的許多二進制關係符號。證明的想法類似於Fagin定理的證明,我們用一階邏輯編碼圖靈機。我們要證明的是,對於每台圖靈機M,我們構建了一個詞彙τ的句子φm ,因此當且僅當m停止空輸入上時, φM是有限的,這與停止問題相當,因此無法確定。

令M =⟨Q,σ,δ,Q 0 ,Q a ,Q r⟩是帶有單個無限膠帶的確定性圖靈機。

  • Q是一組狀態,
  • σ是輸入字母,
  • δ是磁帶字母,
  • δ是過渡函數,
  • Q 0是初始狀態,
  • Q A和Q R是接受和拒絕國家的集合。

由於我們正在處理停止在空輸入上的問題,因此我們可以假設wlog認為δ= {0,1},而0代表空白,而1表示一些磁帶符號。我們定義τ,以便我們可以表示計算:

τ:= {<, min ,t 0 (Å,走為),t 1 (Å,走為),(h q (β,β)) (q∈q) }

在哪裡:

  • <是線性順序,最小值是最小元素相對於<(我們的有限域將與自然數的初始段相關聯)的恆定符號。
  • t 0和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 's和h q 's被解釋為上述,(ii)機器最終停止。停止條件相當於說H Q ∗ (s,t)對於某些S,T和Q ∗ ∈Qa∪q r ,在該狀態之後,機器的配置不會改變。停止計算機的配置(非釋放不是有限的)可以表示為τ(有限)句子(更確切地說,是滿足句子的有限τ結構)。句子φm是:φ²α∧β∧γ∧η∧η∧δθ。

我們通過組件將其分解:

  • α表明<是線性秩序,最小是其最小元素
  • γ定義M的初始配置:在狀態Q 0中,頭部位於第一個位置,磁帶僅包含零:γh Q 0Minmin )∧St 0 (s, min
  • η指出,在M的每種配置中,每個磁帶單元格完全包含一個δ的一個元素:∀S∀T(t 0 (s,t) ↔t1 (s,s,t))
  • β對謂詞H Q施加了基本的一致性條件:機器正好處於一個狀態時:
  • ζ指出,在某個時候,M處於停止狀態:
  • θ由句子的結合組成,表明T i 's和h q 's相對於M的過渡表現良好。如果M處於狀態Q讀數0中,則寫入1,將頭部一個位置向左移動並進入狀態Q'。我們通過θ0θ1的分離來表示這種情況:

其中θ2是:

和:

其中θ3是:

S-1和T+1是根據順序<的前身和繼任者的一階可定義縮寫。句θ0確保位置s中的磁帶含量從0變為1,狀態從Q變為q',其餘的磁帶保持相同,頭部移動到S-1(即一個位置到一個位置到左),假設S不是膠帶中的第一個位置。如果是這樣,則全部由θ1處理:一切都是相同的,除了頭部不移動到左側,而是保持放置。

如果φM具有有限的模型,那麼代表M計算的模型(以空磁帶(即包含所有零的磁帶)開始並以停止狀態結束)。如果M停止空輸入,則M的所有配置集合M的停止計算的集合(用<,t i 's and H q 's編碼)是φM的模型,這是有限的,因為停止計算的所有配置都是有限的。因此,M在空輸入IFFφM上停止具有有限模型。由於在空輸入上停止是不可決定的,所以φM是否具有有限模型的問題也是如此 (等效地,是否有限滿足φM )也是不可確定的(遞歸枚舉,但不是遞歸)。這是證明的結論。

推論

有限令人滿意的句子集是遞歸枚舉的。

證明

列舉所有對在哪裡是有限的

推論

對於任何包含至少一個二進制關係符號的詞彙,所有有限有效的句子的集合併非遞歸地枚舉。

證明

從以前的引理中,有限令人滿意的句子是遞歸枚舉的。假設所有有限有效的句子的集合都是遞歸枚舉的。由於如果沒有有限的滿足,我們得出的結論是,不可有限滿足的句子是有限的,因此我們得出結論。如果一組A及其補體都是遞歸枚舉的,則A是遞歸的。因此,有限令人滿意的句子是遞歸的,與Trakhtenbrot的定理相矛盾。