クレイグ補間

数理論理学において、クレイグの補間定理は、異なる論理理論間の関係に関する結果である。大まかに言うと、この定理は、式φ が式 ψ を含意し、かつ 2 つの式が少なくとも 1 つの共通の原子変数記号を持つ場合、補間式と呼ばれる式 ρ が存在し、ρ のすべての非論理記号はφ と ψ の両方に現れ、φ は ρ を含意し、ρ は ψ を含意する、というものである。この定理は、1957 年にウィリアム・クレイグによって一階述語論理に対して初めて証明された。この定理の変形は、命題論理などの他の論理に対しても成り立つ。一階述語論理に対するクレイグの補間定理のより強い形式は、 1959 年にロジャー・リンドンによって証明された。^{[ 1 ] [ 2 ]}全体的な結果は、クレイグ-リンドン定理と呼ばれることもある。

命題論理では、

${\displaystyle \varphi =\lnot (P\land Q)\to (\lnot R\land Q)}$

${\displaystyle \psi =(S\to P)\lor (S\to \lnot R)}$。

それから${\displaystyle \varphi }$トートロジー的に意味する${\displaystyle \psi }$これは、次のように書くことで確認できます。${\displaystyle \varphi }$連言標準形：

${\displaystyle \varphi \equiv (P\lor \lnot R)\land Q}$。

したがって、もし${\displaystyle \varphi }$保持して、${\displaystyle P\lor \lnot R}$保持する。

${\displaystyle \rho =(P\lor \lnot R)}$。

順番に、${\displaystyle P\lor \lnot R}$トートロジー的に意味する${\displaystyle \psi }$2 つの命題変数が出現するため${\displaystyle P\lor \lnot R}$両方で発生する${\displaystyle \varphi }$そして${\displaystyle \psi }$つまり、${\displaystyle P\lor \lnot R}$は含意の補間である${\displaystyle \varphi \to \psi }$。

SとTを2つの1階理論とする。表記法として、 S ∪ TをSとTの両方を含む最小の理論とし、S ∪ TのシグネチャはSとTのシグネチャを含む最小のシグネチャとする。また、S ∩ Tを2つの理論の言語の共通部分とし、 S ∩ Tのシグネチャは2つの言語のシグネチャの共通部分とする。

リンドンの定理によれば、 S ∪ T が充足不能である場合、 S ∩ Tの言語には、Sのすべてのモデルで真であり、 Tのすべてのモデルで偽となる補間文 ρ が存在する。さらに、ρ には、ρ において正の出現を持つすべての関係記号が、Sの何らかの式で正の出現を持ち、 Tの何らかの式で負の出現を持ち、ρ において負の出現を持つすべての関係記号が、 Sの何らかの式で負の出現を持ち、 Tの何らかの式で正の出現を持つという、より強い性質がある。

ここでは、命題論理に対するクレイグ補間定理の構成的証明を提示する。^{[ 3 ]}

上記の証明は構成的であるため、補間関数を計算するアルゴリズムを抽出できます。このアルゴリズムを使用すると、 n = | atoms (φ') − atoms (ψ)| の場合、補間関数 ρ はφ よりもO (exp( n )) 個多くの論理結合子を持ちます(この主張の詳細については、ビッグ O 記法を参照してください)。同様の構成的証明は、基本的な様相論理K、直観主義論理、μ 計算に対しても、同様の複雑さの尺度で提供できます。

クレイグ補間は他の方法でも証明できる。ただし、これらの証明は一般的に非構成的である。

• モデル理論的には、ロビンソンの結合一貫性定理を介して、コンパクト性、否定、および連言が存在する場合、ロビンソンの結合一貫性定理とクレイグ補間は同等である。
• 証明論的には、シーケント計算を用いて証明する。カット除去が可能であり、その結果として部分式特性が成り立つ場合、クレイグ補間は導出に関する帰納法によって証明可能である。
• 代数的に、論理を表す様々な代数に対して融合定理を用いる。
• クレイグ補間を利用する他の論理への翻訳を介して。

クレイグ補間には多くの応用例があり、その中には一貫性証明、モデル検査、^{[ 4 ]}モジュール仕様の証明、モジュールオントロジーなどがあります。

• ジョン・ハリソン（2009）。『実践論理と自動推論ハンドブック』ケンブリッジ、ニューヨーク：ケンブリッジ大学出版局。ISBN 978-0-521-89957-4。
• ヒンマン、P. (2005).数理論理学の基礎. AK Peters. ISBN 1-56881-262-0。
• Dov M. Gabbay、Larisa Maksimova (2006) 『補間と定義可能性：様相論理と直観主義論理』（オックスフォード論理ガイド）。オックスフォード科学出版、クラレンドン・プレス。ISBN 978-0-19-851174-8。
• エヴァ・フーグランド、「定義可能性と補間。モデル理論的研究」、博士論文、アムステルダム、2001年。
• W. クレイグ、「モデル理論と証明理論を関連付けるヘルブランド＝ゲンツェンの定理の３つの使用法」、記号論理学ジャーナル 22 (1957)、第 3 号、269–285。