矛盾許容論理
2つの論理体系の双対性はシークエント計算のフレームワークでよくわかる。直観論理では次のシークエントを導出できない。
⊢ A ∨ ¬ A {\displaystyle \vdash A\lor \neg A}
しかし、双対直観論理では次のシークエントを導出できない。
A ∧ ¬ A ⊢ {\displaystyle A\land \neg A\vdash }
同様に、直観論理では次のシークエントを導出できない。
¬ ¬ A ⊢ A {\displaystyle \neg \neg A\vdash A}
一方、双対直観論理では次のシークエントを導出できない。
A ⊢ ¬ ¬ A {\displaystyle A\vdash \neg \neg A}
双対直観論理には結合子 # があり、これは直観的含意の双対である。大まかに言えば、A # B は「Aだが、Bでない」(A but not B)という意味である。ただし、# は真理関数ではない。