カリー／ハワード対応を通して（標準的な）型付きラムダ計算と対応する論理は、連言（∧）と含意（⊃）を持つ論理です。これら2つの体系に共通することは、デカルト閉圏をモデルに持つことです。デカルト閉圏が繋ぎになって、2つの形式体系が結ばれていると言ってもよいでしょう。
デカルト閉圏の代わりにコンパクト閉圏を取ると、対応する論理体系は連言と否定（¬）を持つ論理です。ただし、連言（∧）と選言（∨）は一致してしまい、そのせいで否定も古典論理の否定とは違った振る舞いをします。含意は選言（＝連言）と否定を使って、(A⊃B) := (¬A∨B) と定義します。
連言と選言が一致してしまった論理演算（論理結合子）を×と書いて、×、¬ を持つ（そしてコンパクト閉圏がモデルになる）論理をコンパクト論理と呼ぶことがあります。
さらに、自己双対コンパクト閉圏をモデルにするような論理を考えると、否定もなくなってしまいます。正確に言うと、¬A = A なので、否定は無意味・不要なのです。(A⊃B) := (¬A∨B) = (¬A×B) = (A×B) なので、含意と連言（＝選言）も一致してしまいます。論理演算の数はコンパクト論理よりさらに減って、×だけです。×だけの論理を超コンパクト論理*1と呼ぶことにします。
| モデルとなる圏 | 連言 | 選言 | 否定 | 含意 |
|---|---|---|---|---|
| デカルト閉圏 | ∧ | なし | なし | ⊃ |
| コンパクト閉圏 | × | × | ¬ | ¬(-)×(-) |
| 自己双対コンパクト閉圏 | × | × | なし | × |
関係圏Relは自己双対コンパクト閉圏なので、対応する論理計算は超コンパクト論理のシーケント計算ということになります。論理演算が1個だけの論理なんて面白く無いと思うかもしれませんが、そうでもないです。それなりに考えるべきことはあります。論理演算が1個でも、シーケント計算には高次多圏を用いることになります。
自己双対コンパクト閉圏の例はRelしかないかと言うと、そうでもなくて、Rel類似のスパンの圏も自己双対コンパクト閉圏のようです。有限次元ヒルベルト空間（内積ベクトル空間）の圏も自己双対コンパクト閉圏です。余談ですが、「スパンの圏」という呼び名はどうも分かりにくいので「対応（correspondence）の圏」にしようと思っています。スパンは単なる射の図形で、対応はスパンの同値類と区別すれば分かりやすくなると思います。
