スコレムの通常形態

数理論理学において、一階述語論理の式は、全称一階述語量化子のみを含む前置標準形である場合に、スコレム標準形である。

すべての一階述語論理式は、スコレム化（スコレム化と綴られることもある）と呼ばれるプロセスによって、充足可能性を変えることなくスコレム標準形に変換できます。結果として得られる論理式は、必ずしも元の論理式と等価ではありませんが、等充足可能です。つまり、元の論理式が充足可能な場合に限り、結果として得られる論理式も充足可能です。^{[ 1 ]}

スコレム標準形への還元は、形式論理の文から存在量化子を取り除く方法であり、自動定理証明器の最初のステップとしてよく実行されます。

スコレム化の最も単純な形式は、全称量化子のスコープ内にない存在量化変数です。これらは、新しい定数を作成することで簡単に置き換えることができます。たとえば、${\displaystyle \exists xP(x)}$次のように変更される可能性があります${\displaystyle P(c)}$、 どこ${\displaystyle c}$は新しい定数です（式中の他の箇所には出現しません）。

より一般的に言えば、スコレム化は、存在量化された変数をすべて置き換えることによって行われる。${\displaystyle y}$用語とともに${\displaystyle f(x_{1},\ldots ,x_{n})}$その機能記号${\displaystyle f}$は新しい。この項の変数は次のとおりである。式が前置正規形の場合、${\displaystyle x_{1},\ldots ,x_{n}}$は普遍的に量化され、その量化子が の前に来る変数です。${\displaystyle y}$一般的に、これらは普遍的に量化される変数です（存在量化子を順番に取り除くと仮定します。したがって、すべての存在量化子は、${\displaystyle \exists y}$削除された）そして${\displaystyle \exists y}$量化子の範囲内で発生します。${\displaystyle f}$このプロセスで導入されるものはスコレム関数（または、アリティがゼロの場合はスコレム定数）と呼ばれ、項はスコレム項と呼ばれます。

例えば、式${\displaystyle \forall x\exists y\forall zP(x,y,z)}$は存在量化子を含んでいるため、スコレム標準形ではありません。${\displaystyle \exists y}$スコレム化は${\displaystyle y}$と${\displaystyle f(x)}$、 どこ${\displaystyle f}$は新しい関数記号であり、 の量化を削除します${\displaystyle y}$結果として得られる式は${\displaystyle \forall x\forall zP(x,f(x),z)}$スコレムの用語${\displaystyle f(x)}$含まれる${\displaystyle x}$しかし、${\displaystyle z}$なぜなら、削除される量化子は${\displaystyle \exists y}$の範囲内にある${\displaystyle \forall x}$しかし、${\displaystyle \forall z}$; この式は前置正規形なので、これは量化子のリストにおいて、${\displaystyle x}$先行する${\displaystyle y}$その間${\displaystyle z}$そうではない。この変換によって得られる式は、元の式が満たされる場合に限り満たされる。

スコレム化は、第1階充足可能性の定義と第2階同値関係を適用することによって機能します。この同値関係は、存在量化子を全称量化子の前に「移動」させる方法を提供します。

${\displaystyle \forall x\exists yR(x,y)\iff \exists f\forall xR(x,f(x))}$

どこ

${\displaystyle f(x)}$は、${\displaystyle x}$に${\displaystyle y}$。

直感的に、「すべての${\displaystyle x}$存在する${\displaystyle y}$そのため${\displaystyle R(x,y)}$「は同等の形式に変換されます。関数が存在します」${\displaystyle f}$すべてのマッピング${\displaystyle x}$に${\displaystyle y}$すべての${\displaystyle x}$それは、${\displaystyle R(x,f(x))}$「。

この等価性は、一階述語論理の充足可能性の定義が関数記号を解釈する関数に対して暗黙的に存在量化を行うため有用である。特に、一階述語論理式は${\displaystyle \Phi }$モデルが存在する場合、それは充足可能である。${\displaystyle M}$そして評価${\displaystyle \mu }$式を真と評価する式の自由変数のうち。モデルにはすべての関数記号の解釈が含まれているため、スコレム関数は暗黙的に存在量化されます。上記の例では、${\displaystyle \forall xR(x,f(x))}$は、モデルが存在する場合に限り充足可能である。${\displaystyle M}$これには、${\displaystyle f}$、したがって${\displaystyle \forall xR(x,f(x))}$これは、自由変数のいくつかの評価（この場合はなし）に対して真である。これは、2 次式で次のように表すことができる。${\displaystyle \exists f\forall xR(x,f(x))}$上記の等価性により、これは以下の充足可能性と同じです。${\displaystyle \forall x\exists yR(x,y)}$。

メタレベルでは、式の一次充足可能性${\displaystyle \Phi }$表記法を少し乱用すれば、次のように書けるかもしれない。${\displaystyle \exists M\exists \mu (M,\mu \models \Phi )}$、 どこ${\displaystyle M}$モデルです。${\displaystyle \mu }$は自由変数の評価であり、${\displaystyle \models }$つまり${\displaystyle \Phi }$は真実です${\displaystyle M}$下${\displaystyle \mu }$1 階モデルにはすべての関数記号の解釈が含まれているため、任意のスコレム関数は${\displaystyle \Phi }$contains は暗黙のうちに存在量化されている${\displaystyle \exists M}$その結果、式の先頭にある変数に対する存在量化子を関数に対する存在量化子に置き換えた後でも、これらの存在量化子を取り除くことで、式を依然として一階述語論理式として扱うことができる。${\displaystyle \exists f\forall xR(x,f(x))}$として${\displaystyle \forall xR(x,f(x))}$関数は暗黙的に存在量化されているため、完了する可能性があります。${\displaystyle \exists M}$一次充足可能性の定義において。

スコレム化の正しさは、以下の例式で示すことができる。${\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)}$以下のとおりです。この式はモデルによって満たされます。${\displaystyle M}$の場合に限り、各可能な値に対して${\displaystyle x_{1},\dots ,x_{n}}$モデルの領域には、次の値が存在する。${\displaystyle y}$モデルの領域において${\displaystyle R(x_{1},\dots ,x_{n},y)}$真。選択公理により、関数が存在する。${\displaystyle f}$そのため${\displaystyle y=f(x_{1},\dots ,x_{n})}$結果として、式は${\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$は、解釈を追加することによって得られるモデルを持つため、充足可能である。${\displaystyle f}$に${\displaystyle M}$これは、${\displaystyle F_{1}}$満たせるのは、${\displaystyle F_{2}}$も充足可能である。逆に、${\displaystyle F_{2}}$が充足可能であるならば、モデルが存在する。${\displaystyle M'}$それを満たすもの。このモデルには関数の解釈が含まれています。${\displaystyle f}$すべての値に対して${\displaystyle x_{1},\dots ,x_{n}}$式${\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$保持する。結果として、${\displaystyle F_{1}}$は、すべての値に対して選択できるため、同じモデルで満たされます。${\displaystyle x_{1},\ldots ,x_{n}}$値${\displaystyle y=f(x_{1},\dots ,x_{n})}$、 どこ${\displaystyle f}$は以下に基づいて評価されます${\displaystyle M'}$。

スコレム化の用途の一つは、自動定理証明におけるものです。例えば、解析タブロー法では、先頭の量化子が存在量化子である式が現れるたびに、スコレム化によってその量化子を取り除いた式を生成できます。例えば、${\displaystyle \exists x\Phi (x,y_{1},\ldots ,y_{n})}$場面の中で起こる、${\displaystyle x,y_{1},\ldots ,y_{n}}$は自由変数です${\displaystyle \Phi (x,y_{1},\ldots ,y_{n})}$、 それから${\displaystyle \Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})}$タブローの同じブランチに追加できます。この追加はタブローの充足可能性を変更しません。古い公式のすべてのモデルは、適切な解釈を追加することによって拡張できます。${\displaystyle f}$新しい公式のモデルへ。

この形式のスコレム化は、「古典的な」スコレム化よりも優れており、式の中で自由変数である変数のみがスコレム項に配置されます。これは、タブローのセマンティクスによって、式自体には含まれていない全称量化変数のスコープに式が暗黙的に含まれる可能性があるため、改善と言えます。これらの変数はスコレム項には含まれませんが、スコレム化の元の定義によれば、これらの変数はスコレム項に含まれるはずです。もう1つの改善策として、変数名の変更を除いて同一の式に同じスコレム関数記号を適用する方法があります。^{[ 2 ]}

もう一つの用途は、一階述語論理の分解法であり、そこでは論理式は全称量化されていると理解される節の集合として表現される。（例として、飲酒者のパラドックスを参照。）

モデル理論における重要な結果の一つに、レーヴェンハイム・スコレムの定理がある。これは、理論をスコレム化し、結果として得られるスコレム関数の下で閉じることで証明できる。^{[ 3 ]}

一般的に、もし${\displaystyle T}$これは理論であり、自由変数を含む各式について${\displaystyle x_{1},\dots ,x_{n},y}$n項関数の記号があります${\displaystyle F}$これは、証明可能なスコレム関数である。${\displaystyle y}$、 それから${\displaystyle T}$これはスコレム理論と呼ばれている。^{[ 4 ]}

すべてのスコレム理論はモデル完全である。すなわち、モデルのすべての部分構造は基本部分構造である。スコレム理論TのモデルMが与えられたとき、ある集合Aを含むMの最小の部分構造をAのスコレム包と呼ぶ。Aのスコレム包はA上の原子素モデルである。

スコレム標準形は、故ノルウェーの数学者トーラルフ・スコレムにちなんで名付けられました。

• ハーブランダイゼーション、スコレム化の双対
• 述語関数論理

• 「スコレム関数」、数学百科事典、EMS Press、2001年 [1994年]
• PlanetMath.org のスコーレム化
• ヘクター・ゼニルによるスコレム化、ウルフラム・デモンストレーション・プロジェクト。
• ワイススタイン、エリック W. 「スコレム化形式」 . MathWorld .