前面说完了自然演算规则，现在来说导出规则。
导出规则有四个，分别是：MT导出规则，双重否定引入规则，PBC导出规则，LEM导出规则。
记的的同学可能会问了：咦，前两个不是在自然演算规则里出现了吗？
是的，实际上，前面说的自然演算规则中这两个的确是提前说了，它们属于导出规则。
下面对它们进行证明，你可以看到它们的证明过程只是用了其他的自然演算规则。
MT导出规则证明：
双重否定引入规则证明：
PBC规则也很好理解，规则及证明过程如下：
LEM规则又称“排中律”，这是一个定理形式。一个公式和它公式的否定进行析取的结果一定成立。
排中律的证明稍显复杂，但是看懂还是很容易。
下面看一个比较复杂的例子：德摩根定律的证明。
德摩根定律包含两部分，详细的可以百度一下（http://baike.baidu.com/view/6246938.htm）：
合取的否定等价于否定的析取；
析取的否定等价于否定的合取。
我们来证明第二个：先证明 ┐(p∨q)→┐p∧┐q
然后证明┐p∧┐q→ ┐(p∨q):
你会不会自己证明德摩根定律的第一条呢？
到此为止，命题逻辑的规则就全部结束了。
我们再次总结一下：
合取规则有
析取规则有
蕴含规则有
否定规则有
底公式规则有
双重否定规则有
导出规则有
后面开始了解命题逻辑的形式语言。
