クレイグの補間定理
提供: miniwiki
2015/5/4/ (月) 12:37時点におけるja>Sureturnによる版
クレイグの補間定理(英: 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 \and R \rightarrow P \or Q[/math]
命題論理でのクレイグの補間定理は、含意
- [math]X \rightarrow Y[/math]
が恒真式なら、常に補間が存在する、というものである。
証明
クレイグの補間定理は以下のような方法で証明できる。
- モデル理論的には、コンパクト性、否定、論理積が存在するとき、Robinson's joint consistency theorem とクレイグの補間定理は等価である。
- 証明理論的には、シークエント計算によって証明できる。カット除去定理が成り立ち、結果として部分論理式特性が保持されるなら、クレイグの補間定理は証明の構成に関する帰納法で証明される。
- 代数学的には、論理を表す代数の多様性についての融合の定理を使う。
- クレイグの補間定理のある他の論理体系に変換する。
応用
クレイグの補間定理は、一貫性の証明、モデル検査、モジュール仕様の証明、モジュールオントロジーの証明などに使われる。
参考文献
- 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