合取消去规则

合取消去规则(elimination rule of conjunction)是推理规则的一种，如果前提p∧q为真，则得结论命题p为真与q为真，由此得到的两个规则称为合取消去规则1。

基本介绍合取消去规则是逻辑演算规则之一。意思是说，如果一个合取命题是真的，那么它的每个支命题都是真的。

合取消去规则是某些自然推理系统中的推理规则之一。简记为∧E或者∧-。可表述为两种形式2：

(1)若Γ├A∧B，则Γ├A;

(2)若Γ├A∧B，则Γ├B。

其中Γ是任意的公式的集合，A、B是公式，├是推出关系。

这一规则意为：若Γ可以推出A与B的合取式A∧B，则Γ可以推出A，Γ也可以推出B。这一规则又可用如下的图式来表示：

也可以表述为如下的图式2：

例如：

公民、法人的合法的民事权益受法律保护，

公民的合法的民事权益营法律僳护。

相关概念谓词逻辑的自然推理系统直觉主义谓词逻辑的自然推理系统是由根岑于1934年建构的推理系统。简记为系统IQN。它的初始符号中有逻辑联结词和量词¬(否定)、∧(合取)、∨(析取)、→(直觉主义蕴涵)、ᗄ(全称量词)、∃(存在量词)，对它们可以作直觉主义的构造性解释。系统IQN包含如下的推理规则：肯定前提规则、合取引入规则、析取引入规则、蕴涵引入规则、否定引入规则、合取消去规则、析取消去规则、蕴涵消去规则、否定消去规则、全称量词引入规则、存在量词引入规则、全称量词消去规则、存在量词消去规则。系统IQN是经典谓词逻辑的自然推理系统QN的真子系统。“间接证明规则”不是系统IQN中有效的推理规则，如果把“间接证明规则”添加到系统IQN中去，就得到了经典谓词逻辑的自然推理系统QN，即系统QN=系统IQN+间接证明规则。系统IQN等价于公理化的直觉主义谓词演算IQ，在语义解释(模型)的基础上，可以证明系统IQN的可靠性和完全性2。

命题逻辑的自然推理系统直觉主义命题逻辑的自然推理系统是由根岑于1934年建构的推理系统。简记为系统IPN。它的初始符号中有逻辑联结词¬(否定)、∧(合取)、∨(析取)和→(直觉主义蕴涵)，对它们可以作直觉主义的构造性解释。系统IPN包含如下的推理规则：肯定前提规则、合取引入规则、析取引入规则、蕴涵引入规则、否定引入规则、合取消去规则、析取消去规则、蕴涵消去规则、否定消去规则。系统IPN是经典命题逻辑的自然推理系统PN的真子系统。“间接证明规则”不是系统IPN中有效的推理规则，如果把“间接证明规则”添加到系统IPN中去，就得到了经典命题逻辑的自然推理系统PN，即系统PN=系统IPN+间接证明规则。系统IPN等价于公理化的直觉主义命题演算IP，在语义解释(模型)的基础上，可以证明系统IPN的可靠性和完全性，系统IPN还是能行可判定的2。

合取式合取式是由合取词联结两个公式构成的真值形式。如p∧q、 (p∨q) ∧r、(p→q) ∧ (⌝p→ ⌝q) 等等。 有时也特 指由合取词联结两个命题变元构成的基本真值形式，即p∧q (读作“p合取q”，或“p并且q”)。合取式与其合取支 (即由合取词联结的两个公式) 之间的真值关系，可用p∧q的真值表来表示(以“T”表示 真，以“F” 表示假) ：

此表说明，当p和q皆真时，p∧q为真; 当p和q中有一假或两者皆假时，p∧q为假。用任一其他公式代替命题变元p或q，并不会改变这种真值关系。合取式是联言命题的真值形式，它舍去了联言命题的支命题之间在内容、意义上的联系。一个合取式的两个合取支可互换位置，而并不改变该合取式的真值。但用日常语言表达的联言命题，其支命题的前后顺序往往是不能随意颠倒的3。

本词条内容贡献者为:

任毅如 - 副教授 - 湖南大学