クレイグの補間定理

クレイグの補間定理（英: Craig's interpolation theorem）は論理学における定理であり、論理体系によってその定義が異なる。William Craig が1957年、一階述語論理について証明したのが最初である。クレイグの補題とも。
命題論理の場合.
命題論理版は以下のように定義される。
が恒真式であるとき、論理式 formula_2 の全ての命題変数が formula_3 と formula_4 の両方に出現する場合で、かつ
と
も恒真式なら、formula_2 を
の「補間（interpolant）」と呼ぶ。
単純な例として、次の式に対して formula_9 は補間である。
命題論理でのクレイグの補間定理は、含意
が恒真式なら、常に補間が存在する、というものである。
証明.
クレイグの補間定理は以下のような方法で証明できる。
応用.
クレイグの補間定理は、一貫性の証明、モデル検査、モジュール仕様の証明、モジュールオントロジーの証明などに使われる。