跳转到内容

Advertising:

逻辑蕴涵:修订间差异

来自GSXAB的知识库
Admin留言 | 贡献
Admin移动页面逻辑蕴含逻辑蕴涵
Gsxab留言 | 贡献
无编辑摘要
第4行: 第4行:
|eng_name=logical implication
|eng_name=logical implication
}}
}}
'''逻辑蕴涵'''('''logical implication''')指两个[[谓词公式]]之间,在所有可能的指派下,若一个为真则另一个必为真的关系。
'''逻辑蕴涵'''('''logical implication''')指两个[[谓词公式]]或一组谓词公式和另一个谓词公式之间,在所有可能的[[赋值(谓词逻辑)|赋值]]下,若赋值[[满足(谓词逻辑)|满足]]前一个公式或这组公式则必满足后一个公式。
或者说若第一个被[[满足(谓词逻辑)|满足]]则第二个被满足的关系。


== 定义 ==
== 定义 ==
第16行: 第15行:
|prototype=偏序
|prototype=偏序
}}
}}
对两个谓词公式 <math>A</math> 和 <math>B</math> ,其中有个体变项均为 <math>P_1,P_2,\dots,P_n</math> ,若对任意指派, <math>A</math> 为真的解释的相同指派下 <math>B</math> 也为真,(或者说若 <math>\sigma \vDash A</math> 则 <math>\sigma \vDash B</math>),则称谓词公式 <math>A</math> '''逻辑蕴涵'''('''logically implies''') <math>B</math> ,记作 <math>A \Rightarrow B</math> 或 <math>A \vDash B</math> 。
对两个谓词公式 <math>A</math> 和 <math>B</math> ,其中有个体变项均为 <math>x_1,x_2,\dots,x_n</math> ,若对任意指派 <math>\sigma</math> ,若 <math>\sigma \vDash A</math> 则 <math>\sigma \vDash B</math> ,则称谓词公式 <math>A</math> '''逻辑蕴涵'''('''logically imply''') <math>B</math> ,记作 <math>A \Rightarrow B</math> 或 <math>A \vDash B</math> 。此时也称 <math>B</math> 为 <math>A</math> 的'''逻辑后承'''


这一定义也推广为左侧是命题集合的情况,记作 <math>A_1, \dots, A_n \Rightarrow B</math> 或 <math>\Gamma \vDash B</math> 。
这一定义也推广为命题集合 <math>A_1,\cdots,A_n</math> 和 <math>B</math> 的情况,此时记作 <math>A_1, \dots, A_n \Rightarrow B</math> 或 <math>\Gamma \vDash B</math> ,也称 <math>B</math> 为 <math>\Gamma</math> 的'''逻辑后承'''。特别地 <math>\varnothing\vDash B</math> 通常记作 <math>\vDash B</math> 。
 
{{CharMetaInfo
|char=&#x22A8;
|unicodeCodePoint={{UnicodeCodePoint|U+22A8|True, Is a Tautology, Satisfies, Results in}}
|latex=\vDash
}}


== 性质 ==
== 性质 ==


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




{{谓词逻辑}}
{{谓词逻辑}}

2026年1月8日 (四) 15:02的版本

逻辑蕴涵
术语名称 逻辑蕴涵
英语名称 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 范式
个体变项代入 可自由代入易字简单易字变形、易字变形
命题变元代入 置换定理

Advertising: