クレイグの補間定理のソースを表示

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

== 命題論理の場合 ==
[[命題論理]]版は以下のように定義される。

:<math>X \rightarrow Y</math>

が[[恒真式]]であるとき、[[論理式 (数学)|論理式]] <math>Z</math> の全ての命題変数が <math>X</math> と <math>Y</math> の両方に出現する場合で、かつ

:<math>X \rightarrow Z</math>

と

:<math>Z \rightarrow Y</math>

も恒真式なら、<math>Z</math> を

:<math>X \rightarrow Y</math>

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

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

:<math>P \land R \rightarrow P \lor Q</math>

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

:<math>X \rightarrow Y</math>

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

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

== 応用 ==
クレイグの補間定理は、一貫性の証明、[[モデル検査]]、[[モジュール]][[仕様記述言語|仕様]]の証明、モジュール[[オントロジー]]の証明などに使われる。

== 参考文献 ==
* {{cite book | author = Hinman, P. | title = Fundamentals of Mathematical Logic | publisher = A K Peters | date = 2005年 | id = ISBN 1-568-81262-0}}
* {{cite book | author = Dov M. Gabbay and Larisa Maksimova | title = Interpolation and Definability: Modal and Intuitionistic Logics (Oxford Logic Guides) | publisher = Oxford science publications, Clarendon Press | date = 2006年 | id = ISBN 978-0198511748}}
* 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.

== 外部リンク ==
* {{Cite journal|和書|author=永島孝 |title=補間定理 |journal=一橋論叢 |ISSN=00182818 |publisher=日本評論社 |year=1988 |month=sep |volume=100 |issue=3 |pages=353-366 |naid=110000315382 |doi=10.15057/12638 |url=https://doi.org/10.15057/12638}}

{{DEFAULTSORT:くれいくのほかんていり}}
{{Mathlogic-stub}}

[[Category:数理論理学]]
[[Category:数学基礎論の定理]]
[[Category:数学に関する記事]]