命题逻辑推理规则

Answer 1

我们的命题演算包括十个推理规则，允许从一组假定为真的公式推导出其他为真的公式。其中前八个规则通常被描述为非假言规则，而最后两个使用了假言推理。假言推理允许在规则的前提中临时假定一个假设作为推导公式集合的一部分。

双重否定除去规则允许从公式"¬¬φ"推导出"φ"。合取介入规则则允许从任何两个公式φ和ψ推导出"(φ∧ψ)"。合取除去规则则反之，从"(φ∧ψ)"推导出φ和ψ。析取介入规则允许从任何公式φ推导出"(φ∨ψ)"和"(ψ∨φ)"。析取除去规则则允许从"(φ∨ψ)"、"(φ→χ)"和"(ψ→χ)"推导出"χ"。双条件介入规则允许从"(φ→ψ)"和"(ψ→φ)"推导出"(φψ)"。双条件除去规则则反之，从"(φψ)"推导出"(φ→ψ)"和"(ψ→φ)"。肯定前件规则允许从φ和"(φ→ψ)"推导出ψ。条件证明规则则允许在假定假设φ时推导出ψ，推出"(φ→ψ)"。反证证明规则允许在假定假设φ时推导出ψ和"¬ψ"，推出"¬φ"。

这组规则的关键特性是它们的可靠性和完备性。非形式地，这意味着规则是正确的且不再需要其他规则。规则定义了真值指派，将命题变量映射到真或假，进而定义了公式的语义。通过这些定义，我们可以形式化公式φ被特定公式集合S语义蕴涵的意义，即在使S成立的所有可能情况下φ也成立。语法蕴涵则允许我们精确地公式化推理规则的可靠性和完备性的意义。

可靠性表示如果S语法蕴涵φ，则S语义蕴涵φ。完备性则表示如果S语义蕴涵φ，则S语法蕴涵φ。对上述规则集合，这些都成立。

扩展资料

命题逻辑以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。（相对于谓词逻辑，它是量化的并且它的原子公式是谓词函数；和模态逻辑，它可以是非真值泛函的。）