截止到前文数理逻辑之 自然演算规则（二），我们已经学习了四种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→Ψ))))
的证明。这只要在原有证明中增加n次→i引用。
接下来在介绍一个概念：公式的等价。
如果一个相继式是有效的，且交换该相继式的左右两边公式后依然有效，则相继式左边和右边的公式称为等价的。
例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是有效的
