クレイグの補間定理

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

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

命題論理の場合[編集]

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

X \rightarrow Y

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

X \rightarrow Z

Z \rightarrow Y

も恒真式なら、Z

X \rightarrow Y

の「補間(interpolant)」と呼ぶ。

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

P \and R \rightarrow P \or Q

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

X \rightarrow Y

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

証明[編集]

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

応用[編集]

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

参考文献[編集]

  • Hinman, P. (2005年). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-568-81262-0. 
  • Dov M. Gabbay and Larisa Maksimova (2006年). Interpolation and Definability: Modal and Intuitionistic Logics (Oxford Logic Guides). Oxford science publications, Clarendon Press. 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.

外部リンク[編集]

  • 補間定理 永島孝、1988年。一橋大学機関リポジトリ HERMES-IR