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

[[分类:命题逻辑]]{{DEFAULTSORT:chong2yan2yun4han2}}
{{#seo:
|keywords=重言蕴涵, 重言蕴含, 逻辑蕴涵, 逻辑蕴含, 推理关系
|description=重言蕴涵是命题逻辑中的重要概念，指在所有真值指派下，若公式A为真则公式B必为真的关系。重言蕴涵当且仅当条件命题A→B为永真式，是逻辑推理和定理证明的基础。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-08-06
}}
{{InfoBox
|name=重言蕴涵
|eng_name=tautological implication
|aliases=逻辑蕴涵,logical implication
}}
'''重言蕴涵'''('''tautological implication''')指两个[[命题公式]]在任意[[指派（命题逻辑）|指派]]下，若第一个为真则另一个必为真的关系。
或者说若第一个被[[满足（命题逻辑）|满足]]则第二个被满足的关系。

重言蕴涵是[[逻辑蕴涵]]在命题逻辑中的简化形式，故有时也称为逻辑蕴涵。

形式语言层级上，重言蕴涵涉及对命题真假的判断，是元语言中的谓词，连接两个对象命题公式；与属于对象语言的[[蕴涵]]逻辑联结词不同。

== 定义 ==

{{Relation
|name=重言蕴涵
|symbol=<math>\Rightarrow</math>,<math>\vDash</math>
|latex=\Rightarrow,\vDash
|operand_relation=命题公式
|prototype=预序
}}
对两个命题公式 <math>A</math> 和 <math>B</math> ，其中成员命题变元均为 <math>P_1,P_2,\dots,P_n</math> ，则两命题公式存在 <math>2^n</math> 个不同指派。
若这 <math>2^n</math> 个指派下，公式 <math>A</math> 为真时 <math>B</math> 也为真，或者说若 <math>\sigma \vDash A</math> 则 <math>\sigma \vDash B</math> ，则称命题公式 <math>A</math> '''重言蕴涵'''('''logically imply'''/'''tautologically imply''')公式 <math>B</math> ，记作 <math>A \Rightarrow B</math> 。也记作 <math>A \vDash B</math> 。

这一定义也推广为左侧是命题集合的情况，记作 <math>A_1, \dots, A_n \Rightarrow B</math> 或 <math>\Gamma \vDash_0 B</math> 。其中记号 <math>\vDash_0</math> 的下标指在 <math>\mathcal{L}_0</math> 中全体指派中可推出。

== 性质 ==

* 命题公式 <math>A</math> 重言蕴涵 <math>B</math> ，当且仅当[[条件命题]] <math>A \rightarrow B</math> 为[[永真式]]。
* 两命题公式等值（[[重言等价]]），当且仅当两命题公式互相重言蕴涵。
* 等值关系符合以下性质：
* 自反性：对任意公式<math>A</math>，有 <math>A \Rightarrow A</math> ；
* 传递性：若 <math>A \Rightarrow B</math> 且 <math>B \Rightarrow C</math> ，则 <math>A \Rightarrow C</math> 。

== 常见重言蕴涵关系 ==
单独分类：[[：分类:命题逻辑常见结论]]

在[[自然演绎]]系统中，重言蕴涵对应着形式上能否形式推导，推理规则对应特定的重言蕴涵关系。


{{命题逻辑}}