クレイグの補間定理

クレイグの補間定理（英: Craig's interpolation theorem）は論理学における定理であり、論理体系によってその定義が異なる。William Craig が1957年、一階述語論理について証明したのが最初である。クレイグの補題とも。

命題論理の場合

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

X \to Y

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

X \to Z

と

Z \to Y

も恒真式なら、 $Z$ を

X \to Y

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

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

P \land R \to P \lor Q

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

X \to Y

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

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

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

クレイグの補間定理は、一貫性の証明、モデル検査、モジュール仕様の証明、モジュールオントロジーの証明などに使われる。

テンプレート:Cite book
テンプレート:Cite book
Eva Hoogland, Definability and Interpolation. Model-theoretic investigations. PdD thesis, Amsterdam 2001.
W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic 22 (1957), no. 3, 269-285.