上一篇說了析取規則和copy規則。還能不能想起來？
今天來看(Ⅷ) 否定規則。
先給一個定義——沖突公式：稱ΦΛ¬Φ或¬ΦΛΦ為沖突公式。其中Φ是任意公式。
也就是是任意一個公式和自己的否定進行合取得到的公式都是沖突公式。
和沖突公式相關的規則有二：
第一個叫“底公式引入消去規則”，第二個當然就叫“底公式引入規則”了。
所謂的底公式就是沖突公式的通用記号，根據它的記号樣子而來，表示絕對不成立。
看一個例子：例19 證明相繼式¬p ∨ q ├ p→ q 是有效的
根據相繼式類型，選擇使用析取消去規則。在第一個盒子中又使用了蘊含引入規則，其中使用了底公式引入規則。因為根據底公式能得出任意公式，是以得到了第五行的結果。
下面是否定引入規則：如果盒子裡的一個公司經過演算得到了底公式，則盒子外面寫下該公式的否定
再看一個例子：例20 證明相繼式p→q, p→﹁q |- ﹁p是有效的.
這個比較簡單。你能自己說出每一行用了什麼規則嗎？
到這裡自然演算的規則就全部學完了。我們一起來複習一下：
首先是命題，與之相關的一個概念是斷言。然後是原子命題、複合命題、命題連接配接詞。
接着是一些引入規則和一些消去規則：合取的析取的雙重否定的蘊含的，還有MT規則和copy規則。
最後還有一個概念：定理！
後面我們要開始學到一些導出規則。
導出規則和自然演算規則相比就好像數學定理和公理的比較：自然演算規則是公認的，不用推導的；導出規則是需要使用自然演算規則推導出來的比較常用的規則。不過并不完全是這樣。