今天繼續說自然演算規則。
不過說之前先說一點題外話：每個人都有自己喜歡的東西，雖然大家都是搞開發的，不過最喜歡的也很可能不一樣。你是牛人我也是牛人，隻不過我們牛逼的地方不一樣，我們都沒有必要為了超過對方而去努力學習自己不稀罕的東西。 ——————謹以此開題吧。
上一篇
數理邏輯之 自然演算規則（一）說道了合取規則，應該還蠻簡單的吧。
看第二個規則：（Ⅱ）雙重否定規則
直覺上，一個公式與它的雙重否定 所表達的内容是一樣的。例如，
It is not true that it does not rain. 和It rains. 是一回事。
知道“It rains.”, 如果願意，我們可以用更複雜的方式來陳述這一事實。“ It is not true that it does not rain. ” 是以我們得到下面的雙重否定引入與消去規則：
既然我們都能看懂合取規則，這個也可以吧：兩條規則，第一條是引入規則，第二條是消去規則。
我們來看一個例子：例5 證明相繼式 p, ﹁﹁(q∧r) |— ﹁﹁p∧r是有效的
1 p 前提假設
2 ﹁﹁(q∧r) 前提假設
3 ﹁﹁p ﹁﹁i 1
4 q∧r ﹁﹁e 2
5 r ∧e2 4
6 ﹁﹁p∧r ∧i 3,5
前兩行是前提，第三行對第一行使用了雙重否定引入規則，第四行對第二行使用了雙重否定消去規則，第五航對第四行使用了前面學過的合取規則，第六行根據合取規則得到了結論。證明完畢！
嗨列位看官，能不能别喊“太簡單了吧”。規則就是這麼簡單，但是你要把每一條都秒懂才是難的。
下條是(Ⅲ) 蘊含消去規則
這個也比較簡單，通過兩個前提得到一個顯而易見的結論。比如
p: It rained.
p→q: If it rained, then the street is wet.
q: The street is wet.
如果我們知道天下雨，而且我們知道天下雨街道就會濕。那麼我們綜合這兩則資訊就能得出“街道确實濕了”的結論。這說明，根據我們通常的直覺，蘊含消去規則的合理性是顯而易見的。
我們再看另一個例子（來自于程式設計）
p: The value of the program’s input is an integer.
p→q: If the program’s input is an integer, then the program output a boolean. 在這個例子中，如果程式輸入是一個整數，我們可以斷定程式輸出是一個布爾值。
要強調的是：p的出現是絕對必要的。如果輸入不是整數，即使程式滿足p→q, 我們無法得到q。
例6 證明相繼式 p, p→q, p →(q → r) |— r是有效的
1 p 前提假設
2 p→q 前提假設
3 p →(q → r) 前提假設
4 q→r →e 1,3
5 q →e 1,2
6 r →e 5,4
這個太簡單了我都不想解釋了，不過呀強調的一點是第六行是對第五行和第四行使用了蘊含消去規則，而不能寫成→e 4,5。規則就是規則，我們很機械。
(Ⅳ) MT規則
我去，咋這麼大隻啊？不好意思，圖檔沒處理好。
這個規則會讓你想起曾經反複使用的逆否命題。不過千萬不要和别人說MT規則就是逆否命題和原命題等價的意思，因為寫法完全不同。
例7 證明相繼式 p→(q→r), p, ﹁r |— ﹁q 是有效的
1 p→(q→r) 前提假設
2 p 前提假設
3 ﹁r 前提假設
4 q→r →e 2,1
5 ﹁q MT 4,3
我們在第五行根據第四行和第三行得出來了結論，好簡單！
例8 證明相繼式 ﹁ p→q, ﹁q |— p 是有效的.
1 ﹁ p→q 前提假設
2 ﹁q 前提假設
3 ﹁﹁p MT 1,2
4 p ﹁﹁e 3
第三行得到一個詭異的結論，第四行使用雙重否定消去等到了證明。
謹記，我們不能從前兩行直接得出第四行，因為沒有這樣的規則。
不知道走到這裡感覺怎麼樣。如果你依然頭腦完全清新，說明你是一枚牛人。
不過後面來的規則可能會讓你措手不及。
既然這樣，我們先歇一下，做兩個小題：
思考題: 證明下列相繼式 是有效的.
① ﹁ p→q, ﹁ q |— p
② p → ﹁q , q |— ﹁ p
記住千萬不要無中生有，使用自己創造的規則。題目越簡單，往往會出現很多自編自導的規則。