逻辑蕴涵

逻辑蕴涵
术语名称	逻辑蕴涵
英语名称	logical implication

逻辑蕴涵(logical implication)指两个谓词公式或一组谓词公式和另一个谓词公式之间，在所有可能的赋值下，若赋值满足前一个公式或这组公式则必满足后一个公式。

逻辑蕴涵是形式语言中根据形式可以用于推断的关系，在不同的语言及其模型中，与实质蕴涵的关系是模型论的重要讨论内容。

定义

逻辑蕴涵
关系名称	逻辑蕴涵
关系符号	[math]\displaystyle{ \Rightarrow }[/math],[math]\displaystyle{ \vDash }[/math]
Latex	\Rightarrow, \vDash
关系对象	谓词公式
关系元数	2
类型	偏序

对两个谓词公式 [math]\displaystyle{ A }[/math] 和 [math]\displaystyle{ B }[/math] ，其中有个体变项均为 [math]\displaystyle{ x_1,x_2,\dots,x_n }[/math] ，若对任意指派 [math]\displaystyle{ \sigma }[/math] ，若 [math]\displaystyle{ \sigma \vDash A }[/math] 则 [math]\displaystyle{ \sigma \vDash B }[/math] ，则称谓词公式 [math]\displaystyle{ A }[/math] 逻辑蕴涵(logically imply) [math]\displaystyle{ B }[/math] ，记作 [math]\displaystyle{ A \Rightarrow B }[/math] 或 [math]\displaystyle{ A \vDash B }[/math] 。此时也称 [math]\displaystyle{ B }[/math] 为 [math]\displaystyle{ A }[/math] 的逻辑后承。

这一定义也推广为命题集合 [math]\displaystyle{ A_1,\cdots,A_n }[/math] 和 [math]\displaystyle{ B }[/math] 的情况，此时记作 [math]\displaystyle{ A_1, \dots, A_n \Rightarrow B }[/math] 或 [math]\displaystyle{ \Gamma \vDash B }[/math] ，也称 [math]\displaystyle{ B }[/math] 为 [math]\displaystyle{ \Gamma }[/math] 的逻辑后承。特别地 [math]\displaystyle{ \varnothing\vDash B }[/math] 通常记作 [math]\displaystyle{ \vDash B }[/math] 。

⊨
字符	⊨
Unicode码位	U+22A8 True, Is a Tautology, Satisfies, Results in
Latex命令序列	\vDash

性质

• 在允许命题变量或零元谓词的讨论场景中，若将命题公式的符号嵌入谓词公式的子集，此时谓词公式间的逻辑蕴含关系相当于命题公式的重言蕴含关系。
• 谓词公式 [math]\displaystyle{ A }[/math] 逻辑蕴涵 [math]\displaystyle{ B }[/math] ，当且仅当条件命题 [math]\displaystyle{ A \rightarrow B }[/math] 为有效式。
• 命题公式 [math]\displaystyle{ A }[/math] 逻辑蕴涵 [math]\displaystyle{ B }[/math] ，当且仅当条件命题 [math]\displaystyle{ A \rightarrow B }[/math] 为永真式。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [math]\displaystyle{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理