截止到前文數理邏輯之 自然演算規則（二），我們已經學習了四種7個命題邏輯的自然演算規則，分別是合取規則、雙重否定規則、蘊含消去規則、mt規則。
接下來我們要學習的規則不僅從規模上看起來比前面的要大，理解和使用上也提公升了難度。
第五種規則叫(ⅴ) 蘊含引入規則
蘊含引入規則會基於前提進行合理的假設提出，並根據合理的規則得出相應的結論。最後進行蘊含引入，完成證明。
來乙個例子讓我們理解一下這是什麼意思：例9 證明相繼式 p→q |— ﹁q → ﹁p 是有效的。
在證明之前說一句，這個和mt的結果很類似（實際上可以認為是等價的），不過這個是合乎邏輯的逆否命題，所以前文說mt並不能這樣說。
證明：1 p→q 前提假設
| 2 ﹁q 引入假設 |
| 3 ﹁p mt 1,2 |
4 ﹁q → ﹁p →i 2-3
在第二行我們提出了乙個假設條件，並根據mt規則得到了第三行(這些由假設引起的證明行都用乙個盒子包著，實際上就是乙個方框，但是我不好表示就用了橫線豎線)。通過這兩行得到了第四行，證明了相繼式。
所以蘊含引入規則的思想就是：為了證明θ→ψ，需要暫時作假設θ，然後證明ψ。在ψ 的證明中，你可以使用θ及其它公式，包括前提及至此已得到的結論。
一般地，在證明中的某一步，我們只能使用在此步前出現的公式θ 且包含θ的盒子還沒有閉合。（相當於作用域）
關於盒子有一點要強調：對於蘊含引入規則，我們必須在盒子後面緊接著寫上公式θ→ψ，並且滿足θ
是盒子中最頂公式而ψ是盒子中的最底公式。
再來看乙個例子：
例10 證明 ﹁q → ﹁p |— p → ﹁﹁ q 是有效的
我還是不畫線了，上吧。這個也很簡單是吧，要注意的還是嚴格遵守規則，不要想當然耳。
接下來引入乙個概念：定理！
定理：如果相繼式 |—θ有效，則稱公式θ
為定理。
也就是定理不需要任何前提。
例11 證明相繼式 |— (q→r) → ((﹁q → ﹁p) → (p → r))有效
這個相繼式左邊沒有東西，右邊很長很複雜，你仔細一看真想大罵：尼瑪這也叫定理啊？
是的，因為他滿足定理的定義。
證明過程如下：
這個證明有點長，而且還假設了三次。不過你只要記得前面說的盒子閉合後要寫上盒子的頂公式蘊含盒子的底公式就方便了。
接下來說一下你剛才的疑問：一般有效相繼式和定理的關係是什麼？
我們可以將相繼式
θ1, θ
2, θ
3, …, θ
n├ψ
的證明變為定理
├ θ1→(θ2→(θ3→(...→(θn→ψ))))接下來在介紹乙個概念：公式的等價。
如果乙個相繼式是有效的，且交換該相繼式的左右兩邊公式後依然有效，則相繼式左邊和右邊的公式稱為等價的。
例12 證明相繼式 p∧q → r |- p → (q → r) 是有效的
例13 證明相繼式 p → (q → r) |- p ∧ q → r是有效的
由上可見，公式p→ (q→r)與公式p∧q→r等價。記為p→ (q→r) -||- p∧q→r。（等價的記號就是把匯出記號正寫乙個反寫乙個：┫┣）
總結一下：這一票學習了蘊含引入規則和兩個概念。我們先休息休息，消化一下。
練習：例14 證明相繼式 p → q |- p ∧ r →q ∧ r是有效的
數理邏輯1 命題演算3
形式理論 formal theory 上一節給出了一套命題演算系統的語言，接下來我們就基於這套語言，定義乙個 公理化的命題演算系統 即 形式理論 我們感興趣的是假定一些wf已存在 公理 和一套推導規則，我們能推導出何種wf，或者說判定某些wf能否被證明。形式理論的目的就在於研究在不同公理和不同推導規...
數理邏輯之 正規化
今天開始說正規化。先介紹幾個概念。語義等值 令 和 是命題邏輯公式，我們稱 和 語義等值當且僅當 且 成立。記為 可滿足公式 給定命題邏輯公式 我們說 是可滿足的，如果存在 的一次求值使得 取值 true.文字 文字l 是指命題原子p或 p。l p p 析取子句 析取子句 d是若干個文字的析取 d ...
數理邏輯之 horn公式
horn公式，中文名一般翻譯成 霍恩公式 也是正規化的一種。horn原子有三 p t p horn原子分別是底公式 頂公式和命題原子。horn原子合取後的蘊含稱為horn字句 a p p a c a p horn子句 繼續合取就是horn公式 h c c h horn公式下面的都是horn公式例子 ...