モデル理論におけるフェファーマン・ヴォート定理[ 1 ]は、ソロモン・フェファーマンとロバート・ローソン・ヴォートによる定理であり、構造の積の1階理論を、その構造の要素の1階理論にアルゴリズム的に還元する方法を示している。
この定理は、モデル理論における標準的な結果の 1 つと考えられています。[ 2 ] [ 3 ] [ 4 ]この定理は、理論の直積に関するAndrzej Mostowskiの以前の結果を拡張したものです。[ 5 ]これは、普遍代数における等式 (恒等式) が代数構造の直積に引き継がれるという 性質(これはBirkhoff の定理の一方向の結果です) を (任意の量化子を持つ式に) 一般化しています。
一階述語論理のシグネチャLを考える。積構造の定義は、 L構造の族を取る。のためにあるインデックス集合Iに対して、積構造を定義する。 これもL構造であり、すべての関数と関係はポイントごとに定義されます。
この定義は、普遍代数における直積を、関数記号だけでなく関係記号も含む言語の構造に一般化するものである。
もしは関係記号ですLの引数とはデカルト積の要素であり、 の解釈を定義します。でによる
いつこれは関数関係であり、この定義は普遍代数における直積の定義に帰着する。
一次式の場合自由変数を持つ署名Lの部分集合解釈のために変数のインデックスの集合を定義しますそのために保持する
自由変数を含む一次式が与えられた場合等価なゲーム正規形を計算するアルゴリズムがあり、それは有限の選言である。互いに矛盾する公式の。
フェファーマン・ヴォートの定理は、一次式を入力とするアルゴリズムを与える。そして式を構築するそれは、製品には以下の条件が満たされている。解釈において保持するインデックスのセット:
式したがって、は式である。例えば、集合体の第一階理論における自由集合変数。
式開始式の構造に従って構築することができる。 いつ量化子フリーであれば、上記の直積の定義により、
したがって、平等であること集合体の言語で。
条件を量化式に拡張することは、量化子消去の一形態と見なすことができ、積要素に対する量化はでは、サブセットに対する定量化に還元される。。
直接積構造の部分構造を考察することは、しばしば興味深い。部分構造に属する積要素を定義する制約が、インデックス要素の集合に対する条件として表現できる場合、結果を一般化することができる。
一例として、有限個のインデックスを除くすべてのインデックスで定数である積要素の部分構造が挙げられる。言語Lには定数記号が含まれていると仮定する。そして、それらの製品要素のみを含む部分構造を検討する。セット
は有限である。定理は、そのような部分構造における真理値を式に還元する。集合の分野では、特定の集合は有限であるという制約がある。
一般化された積を定義する一つの方法は、集合がある分野に属するセットのインデックスのサブセット(冪集合代数))、かつ製品のサブストラクチャが接着を許容する場合。[ 6 ]ここで接着を許容するとは、次の閉鎖条件を指します。2 つの製品要素があり、が集合体の要素であるならば、 も集合体の要素である。「接着」によって定義されるそしてによると:
フェファーマン・ヴォートの定理は、算術の基本定理を通して、乗法を伴う自然数の構造をプレスバーガー算術構造の一般化された積(冪乗)として捉えることで、スコレム算術の決定可能性を示唆する。
インデックスの集合上の超フィルタが与えられた場合積要素上に商構造を定義することができ、それによって超実数を構成するために使用できるイェジー・ウォシの定理が得られます。