2.3 严格蕴涵系统LSIS 避免了实质蕴涵怪论
由以上的基本符号、基本定义，以及推理的基本规则，我们就构成了一个严格蕴涵系统。由于在这个系统中也可以表达实质蕴涵和实质等价的关系，我们既可以导出严格蕴涵的公式，也可以导出实质蕴涵的公式。
但细心的读者会感到疑惑，严格蕴涵系统的建立来自于对“实质蕴涵怪论”的消除怪论的驱动，那这个系统既然可以导出全部的实质蕴涵定理，那个纠缠不休的怪论问题不是依然存在，并没有得到解决吗？我们可以通过这两个系统的比较来回答这个问题。
在实质蕴涵系统中有这样一个基本定义：
(1)(p→q)≡¬(p∧¬ q)
依据实质蕴涵的这个定义，我们有理由获得如下蕴涵公式（2），那就是：
(2)(p→q)→¬(p∧¬ q)
依据命题（1），我们自然可以获得命题（2），但我们可以获得命题（3）和命题（4）的结果吗？
(3)(p→q)⇒¬(p∧¬ q)
(4)(p∧¬ q)⇒(p→q)
遵照严格蕴涵系统和实质蕴涵系统的公设和规则，我们对上述（3）和（4）来进行推演：
(p→q)⇒¬(p∧¬ q)
证明：
①（p∧q）⇒p（公设2）
②（p∧p）⇒p（以p 代q，替换规则）
③（（p⇒q）∧（q⇒r））⇒（p⇒r）（公设⑥）
用p∧p 替换q，用p 替换r
④（（p⇒p∧p）∧（p∧p ⇒p））⇒（p⇒p）（公设⑥）
⑤（p⇒p∧p）（公设③）
⑥（p⇒p∧p）∧（p∧p ⇒p）（②③合取规则）
⑦p⇒p（④⑥分离规则）
⑧（p→q）≡¬（p∧¬ q）（实质蕴涵定义）
用（p→q）替换p
⑨（p→q）⇒（p→q）（⑦替换规则）
用¬（p∧¬ q）替换后件（p→q）
⑩（p→q）⇒¬（p∧¬ q）（等值替换）
证毕。
由命题（3）的证明过程同样可以获得以下命题：
(¬(p∧¬ q))⇒(p→q)
所以，这个实质蕴涵的等值式（1）同样适用于以下严格蕴涵的等值式。
（5）¬（p∧¬ q）⇔（p→q）（命题（2）和（4），严格等值定义）
我们再来证明以下的命题，它们可以为说明实质蕴涵和严格蕴涵之间的关系提供方便，我们首先证明适用于严格蕴涵也适用于实质蕴涵的同一律命题。
（6）p≡p（同一律），也可以表示为：p⇔p
证明：
①p∧q⇒p（公设②）
用p 替换q
②p∧p⇒p（替换规则）
③（（p⇒q ）∧（q⇒r））⇒（p⇒r ）（公设⑥）
用p∧p 替换q，p 替换r
④((p⇒(p∧p )∧(p∧p)⇒p))⇒(p⇒p)
⑤p⇒p∧p（公设③）
⑥（p⇒（p∧p ）∧（p∧p）⇒p）（合取规则）
⑦p⇒p（④⑥分离）
⑧（p≡p）≡（p⇒p）∧（p⇒p）（严格等值定义）
⑨p≡p(p⇔p)
证毕。
交换律的等值形式命题也同样适用于严格蕴涵和实质蕴涵。
（7）p∧q≡q∧p（交换律）
证明：
①（p∧q）⇒（q∧p）（公设①）
用q 替换p，用p 替换q
②（q∧p）⇒（p∧q）（替换规则）
③（p≡q）≡（p⇒q）∧（q⇒p）（严格等值定义）
用p∧q 替换p，q∧p 替换q
④（p∧q≡q∧p）≡（p∧q⇒q∧p）∧（q∧p⇒p∧q）（替换规则）
⑤（p∧q≡q∧p）（严格等值定义）
证毕。
从等值命题的证明，我们转向严格蕴涵命题形式的证明。
(8)(p∧¬ q)⇒((¬(p⇒q))
证明：
①¬◇（（p∧q）∧¬ r））≡¬◇（（p∧q）∧¬ r））（已证命题（6））
②¬◇（（p∧q）∧¬ r））≡¬◇（（p∧¬ r）∧q））（已证命题（7））
③¬◇（（p∧q）∧¬ r））≡¬◇（（p∧¬ r）∧¬ ¬ q））（公设5）
④（（p∧q）⇒r））≡（（p∧¬ r）⇒¬ q））（严格蕴涵定义）
⑤（（p∧q）⇒r））⇒（（p∧¬ r）⇒¬ q））（严格等值定义）
用（p⇒q）替换q，用q 替换r。
⑥((p∧(p⇒q))⇒q)),((p∧¬ q)⇒¬(p⇒q))
⑦（（p∧（p⇒q））⇒q））（公设⑦）
⑧（p∧¬ q）⇒¬（p⇒q）（⑥⑦分离）
证毕。
(9)(p⇒q)⇒¬(p∧¬ q)
①¬◇（¬ p∧¬ q）≡¬◇（¬ p∧¬ q）（已证命题（6））
②（¬ p∧¬ q）≡（¬ q∧¬ p）（已证命题（7））
③¬◇（¬ p∧¬ q）≡¬◇（¬ q∧¬ p）（等值替换）
④¬◇（¬ p∧¬ q）≡（¬ p⇒q）（严格蕴涵定义）
⑤（¬ q⇒p）≡¬◇（¬ q∧¬ p）（严格蕴涵定义）
⑥（¬ p⇒q）≡（¬ q⇒p）（严格等值）
⑦（¬ p⇒q）⇒（¬ q⇒p）（严格等值定义）
用¬ p 替换p
⑧（¬ ¬ p⇒¬ q）⇒（q⇒¬ p）（替换规则）
⑨（p⇒¬ q）⇒（q⇒¬ p）（公设⑤）
用p∧¬ q 替换p，p⇒q 替换q
⑩((p∧¬ q)⇒¬(p⇒q))⇒((p⇒q)⇒¬(p∧¬ q))
○1（p∧¬ q）⇒¬（p⇒q）（已证命题（6））
○12（p⇒q）⇒¬（p∧¬ q）（○10○1分离）
证毕。
现在我们开始关注带有实质蕴涵形式的命题了。
(10)(p⇒q)⇒(p→q)
证明：
①（p⇒q）⇒¬（p∧¬ q）（已证命题（9）
②p→q≡¬（p∧¬ q）（实质蕴涵定义）
③（p⇒q）⇒（p→q）（等值替换）
证毕。
由以上已证命题，我们立刻可以获得命题（11）的证明。
(11)(p→q)⇒¬(p∧¬ q)
证明：
①（p→q）⇒（p→q）（已证命题（6））
②（p→q）→¬（p∧¬ q）（已证命题（2））
③（p→q）⇒¬（p∧¬ q）（公设⑥）
证毕。
以上所证明的命题表明两个蕴涵，即实质蕴涵和严格蕴涵之间的某种关系。在严格蕴涵关系下可证的命题，它们在实质蕴涵关系下也是可证的，因为严格蕴涵这种蕴涵形式，严格蕴涵着实质蕴涵，如命题（10）和命题（11）所显示的。但是在实质蕴涵关系下的可证命题，在严格蕴涵关系条件下则一定是不可证的，[20]如命题（¬（p∧¬ q））⇒（p⇒q）。这表明，我们在前所讨论的实质蕴涵怪论的诸多命题，如果把其实质蕴涵形式转换为严格蕴涵形式，则这些命题也是不可证的。例如以下有与实质蕴涵形式同构的严格蕴涵形式命题，它们在严格蕴涵形式下就是不可证的。
①p⇒(q⇒p)
②¬ p⇒(p⇒q)
③(p∧q)⇒(p⇒q)
④(p∧q)⇒(q⇒p)
⑤(¬ p¬ ∧¬ q)⇒(p⇒q)
⑥(¬ p¬ ∧¬ q)⇒(q⇒p)
⑦(¬ p¬ ∧q)⇒(p⇒q)
⑧¬(p⇒q)⇒p
⑨¬(p⇒q)⇒¬ q
⑩¬(p⇒q)⇒(p⇒¬ q)
○1¬(p⇒q)→(¬ p⇒q)
○12¬(p⇒q)→(¬ p⇒¬ q)
○13¬(p⇒q)→(q⇒p)
等等。[21]
在严格蕴涵系统LSIS 中，不再出现实质蕴涵中的怪论情形，但这并不排除LSIS 仍有可能出现怪论。不过就重要性而言，C.I.刘易斯的这个LSIS 出现怪论和它导引出模态逻辑相比，后者显得更为重要，需要我们格外的予以关注。