クレイグの補間定理

命題論理版は以下のように定義される。

${\displaystyle X\rightarrow Y}$

が恒真式であるとき、論理式 ${\displaystyle Z}$ の全ての命題変数が ${\displaystyle X}$ と ${\displaystyle Y}$ の両方に出現する場合で、かつ

${\displaystyle X\rightarrow Z}$

と

${\displaystyle Z\rightarrow Y}$

も恒真式なら、${\displaystyle Z}$ を

${\displaystyle X\rightarrow Y}$

の「補間（interpolant）」と呼ぶ。

単純な例として、次の式に対して ${\displaystyle P}$ は補間である。

${\displaystyle P\land R\rightarrow P\lor Q}$

命題論理でのクレイグの補間定理は、含意

${\displaystyle X\rightarrow Y}$

が恒真式なら、常に補間が存在する、というものである。

クレイグの補間定理は以下のような方法で証明できる。

• モデル理論的には、コンパクト性、否定、論理積が存在するとき、Robinson's joint consistency theorem とクレイグの補間定理は等価である。
• 証明理論的には、シークエント計算によって証明できる。カット除去定理が成り立ち、結果として部分論理式特性が保持されるなら、クレイグの補間定理は証明の構成に関する帰納法で証明される。
• 代数学的には、論理を表す代数の多様性についての融合の定理を使う。
• クレイグの補間定理のある他の論理体系に変換する。