蘊涵

蘊涵（英語：Entailment）在命題邏輯和謂詞邏輯中用來描述在兩個句子或句子的集合之間的聯繫，一般使用⇒符號表示。

語義蘊涵

$A\models B$

語義蘊涵也叫做邏輯蘊涵（Logical Implication）^[1]，亦可以讀作 B 是 A 的語義後承。

陳述句子集合A語義上蘊涵句子集合B。

形式定義：集合A蘊涵集合B，當且僅當在其中A中所有句子都為真的所有模型中，在B中的所有句子也是真的。在圖表形式中，它看起來像：

我們需要蘊涵的定義要求A的所有的模型也是B的模型，因為像知識庫這樣的形式系統在被問到事實的集合（A）是否蘊涵命題（B）的時候，不可能知道在用戶頭腦中對此的解釋。

在語用學（語言學）中，蘊涵有不同的但密切相關的意思。

如果對於公式X有 $\varnothing \models X$ 則X被稱為"有效的"或是"重言式"。

$A\vdash B$

陳述句子集合A語法蘊涵句子集合B。它可以讀作"B可以證明自A"，或 B 是 A 的語法後承。

定義：A語法蘊涵B，如果通過假定所有A中所有的句子並通過對它們應用一個有限序列的推理規則（比如來自命題演算的），你可以推導出B中的所有句子。

當然，這與特定的邏輯（證明演算）有關。在討論多個邏輯的情況下，在 $\vdash$ 符號上放置下標是很有用的。

理想上，語義蘊涵（semantic consequence）和語法蘊涵（syntactic consequence）等價，但這不總是可行。（參見哥德爾不完備定理，它陳述了包含為真但不能證明的句子的一些語言（比如算術））。在這種情況下，把等價分成兩部分是有用的：

演繹系統S對於語言L是完備的，當且僅當 $A\models _{L}X\to A\vdash _{S}X$ ：就是說，所有有效的論證都是可證明的。

演繹系統S對於語言L是可靠的，當且僅當 $A\vdash _{S}X\to A\models _{L}X$ ：就是說，所有可證明的論證都是有效的，沒有無效的論證是可證明的。

在很多情況下，蘊涵符合於實質蘊涵：就是說， $A,X\models Y$ 當且僅當 $A\models X\to Y$ 。但是在一些多值邏輯中這不是真的。

^ Christopher C. Leary. A Friendly Introduction to Mathematical Logic 2nd Edition. : 36–37.