クレイグの定理

数理論理学において、クレイグの定理（クレイグのトリックとも呼ばれる）は、一階述語論理の整形式式の任意の再帰的に列挙可能な集合は再帰的に公理化可能であり、原始的に再帰的に公理化可能であり、多項式時間で決定可能であると述べている。

この結果は、よく知られているクレイグ補間定理とは関係ありませんが、どちらの結果も同じ論理学者であるウィリアム・クレイグにちなんで名付けられています。

させて${\displaystyle A_{1},A_{2},\dots }$再帰的に列挙可能な集合の公理の列挙である${\displaystyle T}$一次式の集合。別の集合を構築する。${\displaystyle T^{*}}$から構成される

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{i}}$

各正の整数に対して${\displaystyle i}$つまり、

${\displaystyle T^{*}=\{A_{1},A_{2}\land A_{2},A_{3}\land A_{3}\land A_{3},\ldots \}}$

演繹的閉包${\displaystyle T^{*}}$そして${\displaystyle T}$したがって、これらは同等である。証明では、${\displaystyle T^{*}}$は再帰的／決定可能な集合である。

任意の数式が与えられた場合${\displaystyle X}$その長さを${\displaystyle |X|}$そして決定する${\displaystyle X\in T^{*}}$まず列挙アルゴリズムをすべて実行すれば十分です${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$出力されたら、${\displaystyle X}$は、$${\displaystyle A_{1},A_{2}\land A_{2},\dots ,\underbrace {A_{|X|}\land \dots \land A_{|X|}} _{|X|}.}$$

公理の集合は、その集合への所属を決定する原始再帰関数が存在する場合に原始再帰的である。上記のアルゴリズムは再帰的であるが、必ずしも原始再帰的ではない。主な問題は、「列挙アルゴリズムをすべての要素が満たされるまで実行する」部分にある。${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$が出力されるまで、列挙アルゴリズムはすべての出力に非常に長い時間を要する場合があります。${\displaystyle A_{1},A_{2},\dots ,A_{|X|}}$。

原始的な再帰では、すべてのループは事前に計算された上限によって制限されなければなりません。したがって、「列挙アルゴリズムを…まで実行する」という表現は許されません。ただし、kの値が分かっている場合は、 「列挙アルゴリズムを最大kステップまで実行する」という表現は可能です。

今度は、数式を置き換える代わりに${\displaystyle A_{i}}$と

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{i}}$

1つはそれを

${\displaystyle \underbrace {A_{i}\land \dots \land A_{i}} _{f(i)}}$(*)

どこ${\displaystyle f}$は、与えられた関数です。${\displaystyle i}$、列挙チューリングマシンが出力するために要するステップ数を返します。${\displaystyle A_{i}}$実際、この構成は多項式時間で実行される決定アルゴリズムを与え、これは特に性質の良い原始再帰関数のクラスである。

この定理はゲーデルの不完全性定理の証明に用いられてきた。まず、原始再帰的な公理系を持つすべての理論に対して定理を証明し、次にクレイグの定理を適用して、再帰的に列挙可能な公理系を持つすべての理論に対して定理が成り立つことを直ちに結論づける。^{[ 1 ]}

もし${\displaystyle T}$これは再帰的に公理化可能な理論であり、その述語記号を互いに素な2つの集合に分割する。${\displaystyle V_{A}}$そして${\displaystyle V_{B}}$すると、${\displaystyle T}$語彙に含まれるもの${\displaystyle V_{A}}$再帰的に列挙可能であり、したがってクレイグの定理に基づいて公理化可能である。カール・G・ヘンペルはこれに基づいて、科学のすべての予測は観察用語の語彙にあるため、科学の理論的語彙は原理的に排除可能であると主張した。彼自身はこの議論に対して2つの反論を提起した。1) 科学の新しい公理は実際には管理不可能であり、2) 科学は帰納的推論を使用しており、理論的用語を排除すると観察文間の帰納的関係が変わる可能性がある。ヒラリー・パトナムはこの議論は、科学の唯一の目的は予測の成功であるという誤解に基づいていると主張する。彼は、理論的用語が必要な主な理由は、理論的な実体（ウイルス、電波星、素粒子など）について議論したいからだと提案している。

• ヘンペル、CG（1963）。「カルナップの著作が科学哲学に及ぼす影響」。シルップ、PA（編）『ルドルフ・カルナップの哲学』所収。イリノイ州ラサール：オープンコート。685-709頁。 

• Craig, William (1953). 「システム内における公理化可能性について」。『記号論理学ジャーナル』18 (1): 30–32 . doi : 10.2307/2266324。

• パトナム、ヒラリー（1965）。「クレイグの定理」。哲学ジャーナル。62 （ 10）：251–260。doi ： 10.2307 /2023298。