令人滿意

數學邏輯中,如果在對其變量的某些值分配下為真實,則可以滿足公式。例如,公式令人滿意,因為這是真的 ,而公式對整數無法滿足。令人滿意的雙重概念是有效性;如果將值分配到其變量使得公式為真,則公式是有效的。例如, 在整數上有效,但是不是。

正式地,對定義允許符號的語法(例如一階邏輯二階邏輯命題邏輯)的語法進行了滿意度。但是,令人滿意的不是語義屬性,而不是句法,因為它與符號的含義有關,例如在諸如 。正式地,我們將解釋(或模型)定義為對變量的值分配,並將含義分配給所有其他非邏輯符號,並且如果有一些解釋使其成為真實的解釋,則可以滿足公式。雖然這允許對符號的非標準解釋 ,可以通過提供其他公理來限制其含義。令人滿意的模量理論問題考慮了公式相對於形式理論的滿意度,即正式理論,即(有限或無限)公理集。

為單個公式定義了可滿足性和有效性,但可以推廣到任意理論或一組公式:如果至少一種解釋使理論中的每個公式都正確,並且如果每個公式在每個解釋中都是真實的,那麼理論是可以滿足的,並且有效。例如,諸如peano算術之類的算術理論是可滿足的,因為它們在自然數中是真實的。這個概念與理論的一致性密切相關,實際上與一階邏輯的一致性相當,這是哥德爾的完整性定理。否定可滿足性是不可信的,有效性的否定是無效的。這四個概念以類似於亞里士多德反對派的方式相互關聯。

確定命題邏輯中的公式是否令人滿意的問題可決定的,被稱為布爾值可滿足問題,或者SAT。通常,確定一階邏輯句子是否令人滿意的問題是無法決定的。在通用代數中,方程理論自動定理證明術語重寫一致性關閉統一的方法用於決定令人滿意。特定理論是否可以決定是否取決於該理論是否無變量和其他條件。

降低有效性到令人滿意的

對於否定的古典邏輯,通常可以重新表達公式對涉及滿意度的有效性的問題,因為在上述反對派中表達的概念之間的關係。尤其僅當且僅當€不可滿足時才有效,也就是說,這是錯誤的。換句話說,僅當€φ無效時,φ才能滿足。

對於沒有否定的邏輯,例如積極的命題演算,有效性和滿意度的問題可能無關。在積極的命題演算的情況下,令人滿意的問題是微不足道的,因為每個公式都是可滿足的,而有效性問題是完整的

對古典邏輯的命題滿足感

經典命題邏輯的情況下,對於命題公式,可滿足性是可決定的。特別是,滿意度是NP完整的問題,並且是計算複雜性理論中最深入研究的問題之一。

一階邏輯上的可滿足性

對於一階邏輯(fol),令人滿意的性能是不可確定的。更具體地說,這是一個共同完成的問題,因此不是半決定的。這一事實與FOL有效性問題的不確定性有關。戴維·希爾伯特(David Hilbert)首先提出了有效性問題的狀況的問題,即所謂的Entcheidungsproblem 。公式的普遍有效性是Gödel的完整定理的半確定問題。如果令人滿意也是一個半確定的問題,那麼存在反模型的問題也將是(如果滿足其否定,公式具有反模型)。因此,邏輯有效性的問題將是可決定的,這與教會定理相矛盾,結果表明了Entscheidungsproblem的負面答案。

模型理論的滿足感

模型理論中,如果存在使公式為true的結構的集合,則可以滿足原子公式。如果A是一個結構,則φ是一個公式, A是從結構中獲取的元素的集合,可以滿足φ的滿足,那麼通常寫的是

A⊧φ [a]

如果φ沒有自由變量,也就是說,如果φ是原子句,並且它得到了A的滿足,那麼一個人寫道

A ⊧ φ

在這種情況下,也可以說a是φ的模型,或者在a中為φ是正確的。如果TA的原子句子(一種理論),一個人寫道

a t

有限的滿意度

與滿意度相關的問題是有限的可滿足性,這是確定公式是否承認有限模型使其成立的問題。對於具有有限模型屬性的邏輯,可滿足性和有限的滿足性問題是該邏輯的公式,並且僅當其具有有限模型時才具有模型。這個問題在有限模型理論的數學領域很重要。

一般來說,有限的滿意度和滿意度不必重合。例如,將獲得的一階邏輯公式視為以下句子的連詞,其中常數


所得公式具有無限模型 ,但可以證明它沒有有限模型(從事實開始並遵循必須在第二個公理上存在的原子,模型的有限性將需要循環的存在,這將違反第三和第四個公理,是否循環重新循環或在其他元素上)。

確定給定邏輯中輸入公式的滿意度的計算複雜性可能與確定有限的滿意度的計算複雜性不同;實際上,對於某些邏輯,只有一個是可以決定的

對於經典的一階邏輯,有限的滿足性是遞歸列舉的(在班級中),而Trakhtenbrot的定理無法確定,用於否定公式的否定。

數值約束

數值約束通常出現在數學優化領域,其中通常希望最大化(或最小化)受某些約束的目標函數。但是,撇開目標函數,簡單地確定約束是否令人滿意的基本問題在某些設置中可能具有挑戰性或不可決定。下表總結了主要案例。

約束 實現 超過整數
線性 PTIME (請參閱線性編程 NP完整(請參閱Integer編程
多項式 通過EG圓柱代數分解可定義 不確定(希爾伯特的第十個問題

表來源:Bockmayr和Weispfenning.

對於線性約束,下表提供了更完整的圖片。

約束: 理性 整數 自然數
線性方程組 ptime ptime NP完整
線性不平等 ptime NP完整 NP完整

表來源:Bockmayr和Weispfenning.

也可以看看