数理逻辑之 命题逻辑导出规则

前面说完了自然演算规则，现在来说导出规则。

 

导出规则有四个，分别是：MT导出规则，双重否定引入规则，PBC导出规则，LEM导出规则。

记的的同学可能会问了：咦，前两个不是在自然演算规则里出现了吗？

是的，实际上，前面说的自然演算规则中这两个的确是提前说了，它们属于导出规则。

下面对它们进行证明，你可以看到它们的证明过程只是用了其他的自然演算规则。

MT导出规则证明：

 双重否定引入规则证明：

 PBC规则也很好理解，规则及证明过程如下：

 LEM规则又称“排中律”，这是一个定理形式。一个公式和它公式的否定进行析取的结果一定成立。

排中律的证明稍显复杂，但是看懂还是很容易。

 

下面看一个比较复杂的例子：德摩根定律的证明。

德摩根定律包含两部分，详细的可以百度一下（http://baike.baidu.com/view/6246938.htm）：

合取的否定等价于否定的析取；

析取的否定等价于否定的合取。

我们来证明第二个：先证明 ┐(p∨q)→┐p∧┐q

 然后证明┐p∧┐q→ ┐(p∨q):

 你会不会自己证明德摩根定律的第一条呢？

 

到此为止，命题逻辑的规则就全部结束了。

我们再次总结一下：

合取规则有

 析取规则有

 蕴含规则有

 否定规则有

 底公式规则有

 双重否定规则有

 导出规则有

 

 

后面开始了解命题逻辑的形式语言。