上一篇说了析取规则和copy规则。还能不能想起来？
今天来看(Ⅷ) 否定规则。
先给一个定义——矛盾公式：称ΦΛ¬Φ或¬ΦΛΦ为矛盾公式。其中Φ是任意公式。
也就是是任意一个公式和自己的否定进行合取得到的公式都是矛盾公式。
和矛盾公式相关的规则有二：
第一个叫“底公式引入消去规则”，第二个当然就叫“底公式引入规则”了。
所谓的底公式就是矛盾公式的通用记号，根据它的记号样子而来，表示绝对不成立。
看一个例子：例19 证明相继式¬p ∨ q ├ p→ q 是有效的
根据相继式类型，选择使用析取消去规则。在第一个盒子中又使用了蕴含引入规则，其中使用了底公式引入规则。因为根据底公式能得出任意公式，所以得到了第五行的结果。
下面是否定引入规则：如果盒子里的一个公司经过演算得到了底公式，则盒子外面写下该公式的否定
再看一个例子：例20 证明相继式p→q, p→﹁q |- ﹁p是有效的.
这个比较简单。你能自己说出每一行用了什么规则吗？
到这里自然演算的规则就全部学完了。我们一起来复习一下：
首先是命题，与之相关的一个概念是断言。然后是原子命题、复合命题、命题连接词。
接着是一些引入规则和一些消去规则：合取的析取的双重否定的蕴含的，还有MT规则和copy规则。
最后还有一个概念：定理！
后面我们要开始学到一些导出规则。
导出规则和自然演算规则相比就好像数学定理和公理的比较：自然演算规则是公认的，不用推导的；导出规则是需要使用自然演算规则推导出来的比较常用的规则。不过并不完全是这样。
