スコーレム標準形

スコーレム標準形（スコーレムひょうじゅんけい、英: Skolem normal form）とは、数理論理学において一階述語論理における存在記号がすべて全称記号の前にある冠頭標準形の論理式を言う。

トアルフ・スコーレムによるスコーレムの定理により、第一階述語論理における任意の論理式に対して、演繹的に等価（deductive equivalence）^[1]なスコーレム標準形の論理式が存在する^[2]。

第一階述語論理における任意の論理式は、論理式の一番前にすべて否定形でない前置記号を持ち、その作用域がどれも論理式の終わりまで及ぶような標準形に直すことができる。

このような標準形を冠頭標準形（prenex normal form）と呼ぶ^[3]。なお、冠頭標準形の一番前から数えて存在記号の前にある全称記号の数を、その冠頭標準形の次数（degree）と呼ぶ。

スコーレム化は、存在量化された変項 ${\displaystyle y}$ を新規の項 ${\displaystyle f(x_{1},\ldots ,x_{n})}$（シンボル ${\displaystyle f}$ は元の論理式には出現していない）に全て置き換えることでなされる。この項の各変項は、次のようなものである。もしその論理式が冠頭標準形なら、${\displaystyle x_{1},\ldots ,x_{n}}$ の各変項は全称量化されていて、その量化子は ${\displaystyle y}$ の量化子より前に置かれている。一般に、論理式には全称量化が行われていて、${\displaystyle \exists y}$ はその量化子のスコープ内にあると考えられる。ここで導入される関数 ${\displaystyle f}$ をスコーレム関数（Skolem function、アリティがゼロならスコーレム定項）と呼び、項全体をスコーレム項（Skolem term）と呼ぶ。

例として、論理式 ${\displaystyle \forall x\exists y\forall z.P(x,y,z)}$ を考える。これには存在量化子 ${\displaystyle \exists y}$ があるので、スコーレム標準形ではない。スコーレム化では ${\displaystyle y}$ を ${\displaystyle f(x)}$ で置き換える。このとき、${\displaystyle f}$ は新たな関数シンボルであり、置換と同時に ${\displaystyle y}$ の量化子を除去する。結果として得られる論理式は ${\displaystyle \forall x\forall z.P(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}$ はそうではない、と言うこともできる。この変換で得られた論理式は、元の論理式が充足される場合のみ充足される。

スコーレム化は、一階述語論理での充足可能性の定義に二階述語論理の等価性を適用するものである。その等価性によれば、存在量化子は全称量化子の前に移動できる。

${\displaystyle \forall x{\Big (}g(x)\vee \exists yR(x,y){\Big )}\iff \forall x{\Big (}g(x)\vee R(x,f(x)){\Big )}}$

ここで

${\displaystyle f(x)}$ は y を x でマッピングする関数である。

直観的に、「全ての x について、ある y が存在し、R(x,y) が成り立つ」とは、「ある関数 f が全ての x を y にマッピングし、全ての x について R(x,f(x)) が成り立つ」と書き換えても等価である。

一階述語論理の充足可能性は、関数シンボルの評価に対して暗黙のうちに存在量化を施すような定義になっているため、この等価性が役立つ。ここで、一階述語論理式 ${\displaystyle \Phi }$ は、モデル ${\displaystyle M}$ が存在し、その論理式を「真」であると評価させるような自由変項の評価の組合せ ${\displaystyle \mu }$ があるとき、充足可能である。このモデルには、全関数シンボルの評価も含まれるので、スコーレム関数も暗黙のうちに存在量化される。上記の例 ${\displaystyle \forall x.R(x,f(x))}$ は、${\displaystyle \forall x.R(x,f(x))}$ が真となるような自由変項（この例では自由変項はない）の評価と ${\displaystyle f}$ の評価を含むモデル ${\displaystyle M}$ が存在するときのみ充足可能であると言える。これを二階述語論理で表すと ${\displaystyle \exists f\forall x.R(x,f(x))}$ となる。上記の等価性により、これは ${\displaystyle \forall x\exists y.R(x,y)}$ の充足可能性と同じである。

メタレベルとしては、論理式 ${\displaystyle \Phi }$ の一階述語論理としての充足可能性は ${\displaystyle \exists M\exists \mu ~.~(M,\mu \models \Phi )}$ と表され、ここで ${\displaystyle M}$ がモデル、${\displaystyle \mu }$ が自由変項群の評価である。一階述語モデルは全関数シンボルの評価を含むので、任意のスコーレム関数 ${\displaystyle \Phi }$ は ${\displaystyle \exists M}$ によって暗黙のうちに存在量化される。結果として、ある変項への存在量化子を論理式の最初での関数群への存在量化子に置換し、それら存在量化子を除去することで、論理式を一階述語論理式のまま扱うことができる。この最後の段階での ${\displaystyle \exists f\forall x.R(x,f(x))}$ を ${\displaystyle \forall x.R(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 y=f(x_{1},\dots ,x_{n})}$ となる関数 ${\displaystyle f}$ が存在する。結果として、${\displaystyle M}$ に ${\displaystyle f}$ の評価を加えたモデルを使えば、論理式 ${\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$ は充足可能である。従って ${\displaystyle F_{2}}$ が充足可能であるときのみ ${\displaystyle F_{1}}$ も充足可能であると言える。これとは別に、${\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 M'}$ における ${\displaystyle f}$ の評価を使って、全ての ${\displaystyle x_{1},\ldots ,x_{n}}$ の値の組合せについて ${\displaystyle y=f(x_{1},\dots ,x_{n})}$ となるような値を選択できるため、${\displaystyle F_{1}}$ も同じモデルで充足可能となる。

• 述語論理
• 一階述語論理

• D.ヒルベルト、W.アッケルマン 著、伊藤誠（訳） 編『記号論理学の基礎（第3版）』大阪教育図書社、1960年。NDLJP:2967702。 

• Skolemization on PlanetMath.org

表 話 編 歴 論理学
関連項目 学術的領域 議論学 価値論 批判的思考 再帰理論 形式意味論 論理史 非形式論理学 計算機科学における論理学（英語版） 数理論理学 数学 メタ論理学 メタ数学 モデル理論 哲学的論理学 哲学 論理学の哲学 数学の哲学 証明論 集合論 論理学の歴史 基本概念 アブダクション 分析的と総合的の区別（英語版） 二律背反 アプリオリ 演繹 定義(内包と外延) 記述 帰納 推論 論理的帰結 論理形式（英語版） 論理的含意（英語版） 論理的真理 名前 必要十分条件 意味 パラドックス 可能世界論 前提 確率 理性 推理 参考 意味論 命題 サブスティトゥーション（英語版） 統語論（英語版） 真理 真理値 妥当性 数学記号の表
哲学的論理学 批判的思考と非形式論理学 分析 曖昧 信念 信用性（英語版） 根拠 説明 説明力（英語版） 事実 誤謬 探究 意見 節約 根拠 プロパガンダ 思慮分別（英語版） 推理 関連 修辞学 厳格 漠然（英語版） 論理学の哲学 構成主義 真矛盾主義 虚構主義（英語版） 有限主義（英語版） 形式主義 直観主義 論理的原子論（英語版） 論理主義 唯名論 プラトニック実在論（英語版） プラグマティズム 実在論
メタ論理学と超数学 カントールの定理 決定問題 チャーチのテーゼ 無矛盾性 実効的方法（英語版） 数学基礎論 ゲーデルの完全性定理 ゲーデルの不完全性定理 健全性 完全性 決定可能性 解釈 レーヴェンハイム-スコーレムの定理 メタ定理（英語版） 充足可能性 独立性（英語版） 独立 タイプとトークンの区別 使用と言及の区別
数理論理学 基幹 形式言語 構成規則 形式体系 演繹システム（英語版） 形式的証明 形式意味論 論理式 集合 元 クラス 古典論理 公理 自然演繹 推論規則 有限関係（英語版） 定理 論理的帰結 公理系 型理論 記号 統語論（英語版） 理論（英語版） 名辞論理学（英語版） 命題 推論 論証 妥当性 三段論法 反対の正方形 ベン図 命題論理とブール論理 ブール関数 命題論理 論理演算 真理値表 原子論理式 リテラル 述語論理 量化 全称記号 存在記号 一階述語論理 二階述語論理 高階述語論理 単項述語計算（英語版） 標準形 連言標準形 選言標準形 否定標準形 冠頭標準形 スコーレム標準形 節標準形 集合論 集合 空集合 数え上げ 外延 有限集合 関数 部分集合 冪集合 可算集合 帰納的集合 定義域 値域 順序対 非可算集合 モデル理論 モデル（英語版） 解釈（英語版） 超準モデル 有限モデル理論 真理値 妥当性 証明論 形式的証明 演繹システム（英語版） 形式体系 定理 論理的帰結 推論規則 統語論（英語版） 再帰理論 再帰 帰納的集合 帰納的可算集合 決定問題 チャーチ＝チューリングのテーゼ 計算可能関数 原始再帰関数 表現 真理値表 クワイン・マクラスキー法 カルノー図 存在グラフ 概念地図 オイラー図 ベン図 スパイダー図 タブローの方法 Xバー理論 構文木 構文解析
非古典論理 様相論理学 真理様相（英語版） 価値様相（英語版） 義務論理 信念様相（英語版） 認識論理 時相論理 線形時相論理 直観主義 直観論理 構成的解析（英語版） ハイディング算術（英語版） 直観主義型理論 構成的集合論（英語版） ファジィ論理 真理の程度（英語版） ファジィルール（英語版） ファジィ集合 ファジィ有限要素（英語版） ファジィ集合演算（英語版） 部分構造論理 構造規則（英語版） 適切さの論理 線形論理 矛盾許容論理 真矛盾主義 様相記述論理（英語版） 存在論 オントロジー言語（英語版）
論理学者 アンダーソン アリストテレス イブン・ルシュド イブン・スィーナー ベイン（英語版） バーワイズ（英語版） ベルナイス ブール ブーロス（英語版） カントール カルナップ チャーチ クリュシッポス カリー ド・モルガン フレーゲ ギーチ ゲンツェン ゲーデル ヒルベルト クリーネ クリプキ ライプニッツ レーヴェンハイム（英語版） ペアノ パース パトナム クワイン ラッセル シュレーダー（英語版） スコトゥス スコーレム スマリヤン タルスキ チューリング ホワイトヘッド オッカムのウィリアム ウィトゲンシュタイン ツェルメロ
カテゴリ