スコーレム化
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:09 UTC 版)
スコーレム化は、一階述語論理での充足可能性の定義に二階述語論理の等価性を適用するものである。その等価性によれば、存在量化子は全称量化子の前に移動できる。 ∀ x ( g ( x ) ∨ ∃ y R ( x , y ) ) ⟺ ∀ x ( g ( x ) ∨ R ( x , f ( x ) ) ) {\displaystyle \forall x{\Big (}g(x)\vee \exists yR(x,y){\Big )}\iff \forall x{\Big (}g(x)\vee R(x,f(x)){\Big )}} ここで f ( x ) {\displaystyle f(x)} は y を x でマッピングする関数である。 直観的に、「全ての x について、ある y が存在し、R(x,y) が成り立つ」とは、「ある関数 f が全ての x を y にマッピングし、全ての x について R(x,f(x)) が成り立つ」と書き換えても等価である。 一階述語論理の充足可能性は、関数シンボルの評価に対して暗黙のうちに存在量化を施すような定義になっているため、この等価性が役立つ。ここで、一階述語論理式 Φ {\displaystyle \Phi } は、モデル M {\displaystyle M} が存在し、その論理式を「真」であると評価させるような自由変項の評価の組合せ μ {\displaystyle \mu } があるとき、充足可能である。このモデルには、全関数シンボルの評価も含まれるので、スコーレム関数も暗黙のうちに存在量化される。上記の例 ∀ x . R ( x , f ( x ) ) {\displaystyle \forall x.R(x,f(x))} は、 ∀ x . R ( x , f ( x ) ) {\displaystyle \forall x.R(x,f(x))} が真となるような自由変項（この例では自由変項はない）の評価と f {\displaystyle f} の評価を含むモデル M {\displaystyle M} が存在するときのみ充足可能であると言える。これを二階述語論理で表すと ∃ f ∀ x . R ( x , f ( x ) ) {\displaystyle \exists f\forall x.R(x,f(x))} となる。上記の等価性により、これは ∀ x ∃ y . R ( x , y ) {\displaystyle \forall x\exists y.R(x,y)} の充足可能性と同じである。 メタレベルとしては、論理式 Φ {\displaystyle \Phi } の一階述語論理としての充足可能性は ∃ M ∃ μ . ( M , μ ⊨ Φ ) {\displaystyle \exists M\exists \mu ~.~(M,\mu \models \Phi )} と表され、ここで M {\displaystyle M} がモデル、 μ {\displaystyle \mu } が自由変項群の評価である。一階述語モデルは全関数シンボルの評価を含むので、任意のスコーレム関数 Φ {\displaystyle \Phi } は ∃ M {\displaystyle \exists M} によって暗黙のうちに存在量化される。結果として、ある変項への存在量化子を論理式の最初での関数群への存在量化子に置換し、それら存在量化子を除去することで、論理式を一階述語論理式のまま扱うことができる。この最後の段階での ∃ f ∀ x . R ( x , f ( x ) ) {\displaystyle \exists f\forall x.R(x,f(x))} を ∀ x . R ( x , f ( x ) ) {\displaystyle \forall x.R(x,f(x))} として扱うことは、関数が ∃ M {\displaystyle \exists M} によって暗黙に存在量化されるという一階述語の充足可能性の定義によるものである。 スコーレム化の正しさを示す例として、論理式 F 1 = ∀ x 1 … ∀ x n ∃ y R ( x 1 , … , x n , y ) {\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)} を考える。この論理式がモデル M {\displaystyle M} で充足されるのは、そのモデルのドメインにおいて x 1 , … , x n {\displaystyle x_{1},\dots ,x_{n}} がとりうる全ての値について、同じモデルのドメインにおいて y {\displaystyle y} の値が存在し、それらの値を適用して評価したとき R ( x 1 , … , x n , y ) {\displaystyle R(x_{1},\dots ,x_{n},y)} が真になる場合のみである。選択公理により、 y = f ( x 1 , … , x n ) {\displaystyle y=f(x_{1},\dots ,x_{n})} となる関数 f {\displaystyle f} が存在する。結果として、 M {\displaystyle M} に f {\displaystyle f} の評価を加えたモデルを使えば、論理式 F 2 = ∀ x 1 … ∀ x n R ( x 1 , … , x n , f ( x 1 , … , x n ) ) {\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))} は充足可能である。従って F 2 {\displaystyle F_{2}} が充足可能であるときのみ F 1 {\displaystyle F_{1}} も充足可能であると言える。これとは別に、 F 2 {\displaystyle F_{2}} が充足可能であるなら、それを充足させるモデル M ′ {\displaystyle M'} が存在し、関数 f {\displaystyle f} の評価が含まれ、全ての x 1 , … , x n {\displaystyle x_{1},\dots ,x_{n}} の値の組合せについて論理式 R ( x 1 , … , x n , f ( x 1 , … , x n ) ) {\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))} が成り立つ。結果として、 M ′ {\displaystyle M'} における f {\displaystyle f} の評価を使って、全ての x 1 , … , x n {\displaystyle x_{1},\ldots ,x_{n}} の値の組合せについて y = f ( x 1 , … , x n ) {\displaystyle y=f(x_{1},\dots ,x_{n})} となるような値を選択できるため、 F 1 {\displaystyle F_{1}} も同じモデルで充足可能となる。
※この「スコーレム化」の解説は、「スコーレム標準形」の解説の一部です。
「スコーレム化」を含む「スコーレム標準形」の記事については、「スコーレム標準形」の概要を参照ください。
- スコーレム化のページへのリンク
