論理学では、含意（⊃）の真理表は前件が偽のときは、全体が真になることを習う。このことは日常的な「ならば」の用法と食い違うことから、実質含意（material implication）のパラドクスと呼ばれる。例えば、
- Q⊃(P⊃Q)
- ￢P⊃(P⊃Q)
- (P⊃Q)v(Q⊃P)
こういった式がトートロジーになってしまう。
もっとも、こんなのはただの取り決めだから、本当はパラドクスではない。しかし、どうすれば日常的な「ならば」の用法を反映させられるのだろうか、という問題は残る。
直観主義論理
3. がトートロジーになるのは、選言の解釈がおかしいからかもしれない。実際、古典論理で妥当とされる排中律を捨てた直観主義論理では、3. はトートロジーではない*1。
このように、実質含意のパラドクスの一部は直観主義論理では回避できる。他の例として、古典述語論理には"Drinker paradox"と呼ばれる妥当式が挙げられる*2。次のような式である。
- ∃x[Px ⊃ ∀yPy]
"Drinker paradox"という呼び名はスマリヤンによる。もしこの式が論理的に真ならば、"There is someone in the pub such that, if he is drinking, everyone in the pub is drinking." もそうなる。直観主義論理の存在量化の解釈では、この式は妥当にならないと思う。
しかし、直観主義論理でも1.と2.はトートロジーのままである。
厳密含意
哲学者C. I. ルイスは厳密含意という概念を提示し、様相論理の体系を作り始めた。厳密含意（→）は
- P→Q iff □(P⊃Q)
という風に定義される。"⊃" の代わりに"→"を使うと、1.--3. はすべて拒否できる。というのも、S5の体系ですら、1.--3.は妥当でないからである。
しかし、S5の体系でも、2.とよく似た次式は妥当である。
- (P＆￢P)→Q
EFQ、つまり矛盾からは何でも帰結するという原理は、日常的な「ならば」の用法が要求するような前件と後件の「つながり」を無視しているように見える（厳密含意のパラドクス）。
反事実的条件法
実質含意よりも強い条件法としては反事実的条件法もある。これは「もしAだったならばCだっただろう」といった反実仮想を表現する。「A＞C」などと記号で書いておこう。
しかし、反事実的条件法の標準的な論理VCでは
- AかつCならば、A＞C
が成り立ってしまう（strong centering）。AとCの間になんの繋がりもなくても、両者がともに真ならば条件文も真というわけである。また、そもそも反事実的条件法は厳密含意よりも弱いので
- Aが不可能ならば、A＞C
- Bが必然的ならば、A＞C
も成り立つ。空虚に真になってしまうケースが排除されていない。
関連論理
わざわざ様相論理に向かうのではなく、命題論理の範囲内で実質含意のパラドクスに立ち向かうことを考えてみよう。2.の式、あるいは、それと似た
- (P＆￢P)⊃Q
シークエント計算で、これらの証明に使われるのは弱化の構造規則を使う。P⇒Pという公理から出発し、右辺のPを左辺に移し、右の弱化規則によってP, ￢P⇒Ｑというシークエントを得るわけだ。
してみると、実質含意のパラドクスの元凶は、弱化規則ではないかという推測がたつ。実際、1.を導くには左の弱化を使うし、3.を導くには左右の弱化を使うことになる。そこで、弱化規則をすべて捨ててしまおう。こうして得られる論理を、関連論理（relevance logic）という。
関連論理の自然演繹
こうしてシークエント計算の上では、日常の「ならば」に近い論理が得られた。では、自然演繹でも同じことができないだろうか。
ここで厄介なのは、自然演繹には構造規則などないということである。シークエント計算における弱化規則に反映する何かを見つける必要がありそうだ。思うに、これは一筋縄ではいかない。弱化規則は自然演繹の中でいろいろな形で埋め込まれているからだ。そのため対応策はちょっと泥縄になる。
とりあえず、2.についてはEFQの推論規則を捨てればよいだろう。つまり、右の弱化に相当するのはEFQであった。
1. はちょっと厄介だ。まず、これの正規の証明は Q /P⊃Q というステップを含むので、空虚な仮定を落とすことは禁じよう。しかし、それだけでは不十分だ。というのも、次のような証明図があるからだ。
P Q
P＆Q
Q
P⊃Q
Q⊃(P⊃Q)
こういう証明図も拒否しなければならない。でも、どうやって？
答えは連言の導入則に制限を設けることである。ふつう自然演繹の連言導入は、前提（文脈）を共有していなくてもできてしまう*3。これを改めて、連言を導入するときの連言肢はともに同じ前提からの帰結でなければならない、としよう。
Q / P⊃Q という証明図を拒否できれば、3.も拒否できるだろう。こうして、自然演繹の上でも日常の「ならば」に近い論理が得られた。
