natural_deduction

基本概念

我们需要有一组规则，每一条都允许我们在特定的前提下得到下一个结论
推断 infer
前提 premise $\phi_1 ,\cdots,\phi_n$
结论 conclusion $\psi$
矢列 sequent

自然演绎规则

合取引入规则 conjunctive introduction

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

合取消去规则 conjunctive elimination

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

双重否定规则 double negative rule

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

蕴含消去规则 modus ponens

已知 $\phi$ 与 $\phi \to \psi$, 那么我们有 $\psi$, 写作 $\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$