查看“︁蕴涵”︁的源代码

{{Expand|time=2013-02-14T05:28:17+00:00 }}
'''蕴涵'''（{{lang-en|Entailment}}）在[[命题逻辑]]和[[谓词逻辑]]中用来描述在两个句子或句子的集合之间的联系，一般使用⇒符号表示。

==语义蕴涵==

<math>A \models B</math>

语义蕴涵也叫做逻辑蕴涵（Logical Implication）<ref>{{Cite book|title=A Friendly Introduction to Mathematical Logic 2nd Edition|last=Christopher C. Leary|pages=36-37}}</ref>，亦可以读作 B 是 A 的语义后承。

陈述句子集合'''A'''语义上蕴涵句子集合'''B'''。

形式定义：集合'''A'''蕴涵集合'''B'''，[[当且仅当]]在其中'''A'''中所有句子都为真的所有模型中，在'''B'''中的所有句子也是真的。在图表形式中，它看起来像：

[[File:Venn_A_subset_B.png|A蕴涵B]]

我们需要蕴涵的定义要求'''A'''的所有的模型也是'''B'''的模型，因为像知识库这样的形式系统在被问到事实的集合（'''A'''）是否蕴涵命题（'''B'''）的时候，不可能知道在用户头脑中对此的解释。

在[[语用学]]（[[语言学]]）中，[[蕴涵 (语用学)|蕴涵]]有不同的但密切相关的意思。

如果对于公式'''X'''有<math>\varnothing \models X</math>则'''X'''被称为"[[有效性|有效的]]"或是"[[重言式]]"。

==语法蕴涵==

<math>A \vdash B</math>

陈述句子集合'''A语法'''蕴涵句子集合'''B'''。它可以读作"B可以证明自A"，或 B 是 A 的语法后承。

定义：'''A语法'''蕴涵'''B'''，如果通过假定所有'''A'''中所有的句子并通过对它们应用一个有限序列的推理规则（比如来自[[命题演算]]的），你可以推导出'''B'''中的所有句子。

当然，这与特定的逻辑（[[证明论|证明演算]]）有关。在讨论多个逻辑的情况下，在<math>\vdash</math>符号上放置[[下标]]是很有用的。

==在语义和语法蕴涵之间的联系==

理想上，[[逻辑的语义|语义]]蕴涵（semantic consequence）和语法蕴涵（syntactic consequence）[[等价]]，但这不总是可行。（参见[[哥德尔不完备定理]]，它陈述了包含为真但不能证明的句子的一些语言（比如[[算术]]））。在这种情况下，把等价分成两部分是有用的：

演绎系统'''S'''对于语言'''L'''是[[完备]]的，当且仅当<math>A \models_L X \to A \vdash_S X</math>：就是说，所有[[有效的]]论证都是可[[证明]]的。

演绎系统'''S'''对于语言'''L'''是[[可靠性|可靠]]的，当且仅当<math>A \vdash_S X \to A \models_L X</math>：就是说，所有可证明的论证都是有效的，没有无效的论证是可证明的。

==与实质蕴涵的联系==

在很多情况下，蕴涵符合于[[实质蕴涵]]：就是说，<math>A, X \models Y</math>当且仅当<math>A \models X \to Y</math>。但是在一些[[多值逻辑]]中这不是真的。

==参见==
*[[逻辑等价]]
*[[实质蕴涵]]
*[[文字蘊涵]]
*[[蕴涵门]]

{{逻辑联结词}}
{{数理逻辑}}
[[Category:邏輯結果| ]]
[[Category:哲学逻辑]]
[[Category:元逻辑学]]
[[Category:命题演算]]
[[Category:演繹]]
[[Category:邏輯概念]]
[[Category:句法 (逻辑学)]]
[[Category:二元運算]]