命题逻辑的推理规则
我们的命题演算有十个推理（inference）规则。这些规则允许我们从给定的一组假定为真的公式中推导出其他为真的公式。前八个简单的陈述我们可以从其他 wff 推论出（infer）特定的 wff。但是最后两个规则使用了假言(hypothetical）推理，这意味着在规则的前提中我们可以临时的假定一个（未证明的）假设（hypothesis）作为推导出的公式集合的一部分，来查看我们是否能推导出一个特定的其他公式。因为前八个规则不是这样而通常被描述为非假言规则，而最后两个就叫做假言规则。
双重否定除去
从 wff ¬ ¬ φ，我们可以推出 φ。
合取介入
从任何 wff φ 和任何 wff ψ，我们可以推出 （φ ∧ ψ）。
合取除去
从任何 wff （φ ∧ ψ），我们可以推出 φ 和 ψ。
析取介入
从任何 wff φ，我们可以推出 （φ ∨ ψ） 和 （ψ ∨ φ），这里的 ψ 是任何 wff。
析取除去
从 （φ ∨ ψ）、（φ → χ） 和 （ψ → χ） 形式的wff，我们可以推出 χ。
双条件介入
从 （φ → ψ） 和 （ψ → φ） 形式的 wff，我们可以推出 （φ ψ）。
双条件除去
从 wff （φ ψ），我们可以推出 （φ → ψ） 和 （ψ → φ）。
肯定前件
从 φ 和 （φ → ψ） 形式的 wff，我们可以推出 ψ。
条件证明
如果在假定假设 φ 的时候可以推导出 ψ，我们可以推出 （φ → ψ）。
反证证明
如果在假定假设 φ 的时候可以推导出 ψ 和 ¬ ψ，我们可以推出 ¬ φ。
规则的可靠性和完备性
这组规则的关键特性是它们是可靠的和完备的。非形式的，这意味着规则是正确的并且不再需要其他规则。这些要求可以如下这样正式的提出。
我们定义真值指派为把命题变量映射到真或假的函数。非形式的，这种真值指派可以被理解为对事件的可能状态（或可能性世界）的描述，在这里特定的陈述是真而其他为假。公式的语义因而可以被形式化，通过对它们把那些事件状态认定为真的定义。
我们通过如下规则定义这种真值 A 在什么时候满足特定 wff:
A 满足命题变量P当且仅当A(P) = 真
A 满足 ¬ φ当且仅当A 不满足 φ
A 满足 （φ ∧ ψ）当且仅当A 满足 φ 与 ψ 二者
A 满足 （φ ∨ ψ）当且仅当A 满足 φ 和 ψ 中至少一个
A 满足 （φ → ψ） 当且仅当没有 A 满足 φ 但不满足 ψ 的事例
A 满足 （φ ψ）当且仅当A 满足 φ 与 ψ 二者，或则不满足它们中的任何一个
通过这个定义，我们现在可以形式化公式φ 被特定公式集合 S 蕴涵的意义。非形式的，就是在使给定公式集合 S 成立的所有可能情况下公式 φ 也成立。这导引出了下面的形式化定义： 我们说 wff 的集合 S 语义蕴涵（蕴涵：entail 或 imply）特定的 wff φ，条件是满足在 S 中的公式的所有真值指派也满足 φ。
最后我们定义语法蕴涵，φ 被 S 语法蕴涵，当且仅当我们可以在有限步骤内使用我们提出的上述推理规则推导出它。这允许我们精确的公式化推理规则的可靠性和完备性的意义：
可靠性
如果 wff 集合 S 语法蕴涵 wff φ，则 S 语义蕴涵 φ
完备性
如果 wff 集合 S 语义蕴涵 wff φ，则 S 语法蕴涵 φ
对上述规则集合这些都成立。
已赞过
已踩过<
