基本概念

我们需要有一组规则，每一条都允许我们在特定的前提下得到下一个结论
推断 infer
前提 premise ϕ1,⋯ ,ϕn\phi_1 ,\cdots,\phi_n
结论 conclusion ψ\psi
矢列 sequent
文字 literal: 原子命题或其否定
子句 clause: CNF 的每一个析取向

自然演绎规则

合取引入规则 conjunctive introduction

在分别得到结论 ϕ\phi 和结论 ψ\psi 的前提 下推导出结论 ϕ∧ψ\phi \land \psi. 这个规则写为 ∧e\wedge e
前提是证明两个结论各自分别正确

合取消去规则 conjunctive elimination

在已知 ϕ∧ψ\phi \wedge \psi 的条件下有 ϕ\phi 与 ψ\psi 各自成立，分别写作 ∧e1,∧e2\wedge e_1, \wedge e_2

双重否定规则 double negative rule

对于双重否定我们可以得到其本身

蕴含消去规则 modus ponens

已知 ϕ\phi 与 ϕ→ψ\phi \to \psi, 那么我们有 ψ\psi, 写作 →e\to e

反证规则 Modus Tollens (不是反证法)

已知 蕴含关系 ϕ→ψ\phi \to \psi 和 ¬ψ\neg\psi, 我们有 ¬ϕ\neg \phi
证明思路: 假设 ϕ\phi 则有 ψ\psi 与 ¬ψ\neg\psi 矛盾, 因此 ¬ϕ\neg \phi

蕴含引入规则

在已知 ϕ→ψ\phi \to \psi 的前提下有 ¬ψ→¬ϕ\neg\psi\to\neg\phi

命题逻辑的合理性

语义推导关系

若对使 ϕ1⋯ϕn\phi_1\cdots\phi_n都赋值为 TT 的一切赋值，ψ\psi 的赋值也是 TT 那么我们定义

ϕ1⋯ϕn⊨ψ\phi_1\cdots\phi_n\models \psi

其中 ⊨\models 为语义推导关系 semantic entailment relation
这个概念是用来描述正确合理的逻辑推导关系的，强调 前提真则结果必为真

合理性定理 (和演绎推理的关系)

设 ϕ1⋯ϕn\phi_1\cdots\phi_n 和 ψ\psi 是命题逻辑公式，若 ϕ1⋯ϕn⊢ψ\phi_1 \cdots \phi_n \vdash \psi 是有效的，那么 ϕ1⋯ϕn⊨ψ\phi_1 \cdots \phi_n\models \psi 成立

合理性有什么用

命题逻辑合理性对保证一个给定矢列的证明 不存在 非常好用
上述的 ⊨\models 是任意关系，如果要证明不成立，就是找 ∃\exists 逻辑

命题逻辑的完备性

与上部分的 合理性定理 相比，这里我们要证明的反向逻辑，也就是 当且仅当 ϕ1⋯ϕn⊨ψ\phi_1 \cdots \phi_n\models \psi 成立，ϕ1⋯ϕn⊢ψ\phi_1\cdots\phi_n\vdash\psi 有效
每一个在语义上为真的命题都可以被证明（完备性）