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

[[分类:命题逻辑]]
{{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 implies'''/'''tautological implies''') <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>A</math> 重言蕴含 <math>B</math> ，当且仅当[[蕴含|条件命题]] <math>A \rightarrow B</math> 为永真式。


{{命题逻辑}}