冠頭標準形

冠頭標準形（英: prenex normal form）とは、数理論理学において一階述語論理の論理式の形式であり、量化子が論理式の先頭部分に集められている形式を指す（残りの部分をマトリクスと呼び、先頭の各量化子はマトリクス全体にかかっている）。

古典論理では、あらゆる論理式には等価な冠頭標準形の論理式が存在する。例えば、量化子がなく自由変項を含む論理式 φ(y)、ψ(z)、ρ(x) があるとき、

${\displaystyle \forall x\exists y\exists z(\phi \lor (\psi \rightarrow \rho ))}$

は ${\displaystyle \phi \lor (\psi \rightarrow \rho )}$ をマトリクスとする冠頭標準形であり、

${\displaystyle \forall x((\exists y\phi )\lor ((\forall z\psi )\rightarrow \rho ))}$

は上と論理的に等価だが冠頭標準形でない論理式である。

全ての一階述語論理の論理式には（古典論理では）論理的に等価な冠頭標準形の論理式が存在する。いくつかの変換規則を再帰的に適用することで、論理式を冠頭標準形に変換できる。規則は、論理式に出現する論理演算子の種類によって異なる。

論理積と論理和の規則は、

${\displaystyle (\forall x\phi )\land \psi }$ は ${\displaystyle \forall x(\phi \land \psi )}$ と等価

${\displaystyle (\forall x\phi )\lor \psi }$ は ${\displaystyle \forall x(\phi \lor \psi )}$ と等価

および

${\displaystyle (\exists x\phi )\land \psi }$ は ${\displaystyle \exists x(\phi \land \psi )}$ と等価

${\displaystyle (\exists x\phi )\lor \psi }$ は ${\displaystyle \exists x(\phi \lor \psi )}$ と等価

である。これらの規則は、x が ψ の中で自由変項として現れない場合に妥当である。もし x が ψ の中に自由変項として現れた場合、他の自由変項と置き換える必要がある。

例えば、環の言語で、

${\displaystyle (\exists x(x^{2}=1))\land (0=y)}$ は ${\displaystyle \exists x(x^{2}=1\land 0=y)}$ と等価である。

しかし

${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ は ${\displaystyle \exists x(x^{2}=1\land 0=x)}$ と等価ではない。

左の式は、自由変項 x が 0 のとき任意の環で真だが、右の式には自由変項がなく、どんな環でも偽である。

否定の規則は

${\displaystyle \lnot \exists x\phi }$ は ${\displaystyle \forall x\lnot \phi }$ と等価

および

${\displaystyle \lnot \forall x\phi }$ は ${\displaystyle \exists x\lnot \phi }$ と等価

である。

含意には4つの規則がある。そのうち2つは仮説から量化子を除去するもので、残る2つは帰結から量化子を除去する。これらの規則は、含意 ${\displaystyle \phi \rightarrow \psi }$ を ${\displaystyle \lnot \phi \lor \psi }$ と書き換えた上で上述の論理和に関する規則を適用することで得られる。論理和の規則と同様、ある部分論理式に出現する量化された自由変項が他の部分論理式に出現しないことが条件になっている。

仮説部分から量化子を除去する規則は以下の通り。

${\displaystyle (\forall x\phi )\rightarrow \psi }$ は ${\displaystyle \exists x(\phi \rightarrow \psi )}$ と等価

${\displaystyle (\exists x\phi )\rightarrow \psi }$ は ${\displaystyle \forall x(\phi \rightarrow \psi )}$ と等価

帰結部分から量化子を除去する規則は以下の通り。

${\displaystyle \phi \rightarrow (\exists x\psi )}$ は ${\displaystyle \exists x(\phi \rightarrow \psi )}$ と等価

${\displaystyle \phi \rightarrow (\forall x\psi )}$ は ${\displaystyle \forall x(\phi \rightarrow \psi )}$ と等価

${\displaystyle \phi }$、${\displaystyle \psi }$、${\displaystyle \rho }$ は量化子を含まない論理式であり、共通の自由変項を持たないものとする。次の論理式を考える。

${\displaystyle (\phi \lor \exists x\psi )\rightarrow \forall z\rho }$

上述の規則群を最も内側の部分論理式から再帰的に適用していく。すると、以下のような一連の論理的に等価な論理式が得られる。

${\displaystyle (\exists x(\phi \lor \psi ))\rightarrow \forall z\rho }$

${\displaystyle \forall x((\phi \lor \psi )\rightarrow \forall z\rho )}$

${\displaystyle \forall z\forall x((\phi \lor \psi )\rightarrow \rho )}$

なお、元の論理式と等価な冠頭標準形は唯一ではない。例えば、上の例で仮説部ではなく帰結部を先に変換すると、次の冠頭標準形が得られる。

${\displaystyle \forall x\forall z((\phi \lor \psi )\rightarrow \rho )}$

冠頭形への変換規則は古典論理であることに依存している。直観論理では、全ての論理式に等価な冠頭標準形があるわけではない。例えば否定が問題になるが、それだけではない。含意も直観論理と古典論理では扱いが異なる。直観論理では、含意を論理和と否定を使った形式に置き換えられない。

BHK解釈は、なぜ一部の論理式が直観論理で等価な冠頭標準形を持たないのかを示している。この解釈では、次の論理式

${\displaystyle (\exists x\phi )\rightarrow \exists y\psi \qquad (1)}$

を証明は、特定の x と φ(x) の証明を与えられたとき、特定の y と ψ(y) の証明を生成する関数と考える。この場合、与えられた x の値から y の値を計算することは可能である。しかし、次の論理式

${\displaystyle \exists y(\exists x\phi \rightarrow \psi ),\qquad (2)}$

の証明は、y の特定の値を生成し、${\displaystyle \exists x\phi }$ の証明を ψ(y) の証明に変換する関数である。φ を満足する任意の x を使って ψ を満足する y を構築できるが、そのような x の知識なしに y を構築できないなら、論理式 (1) は論理式 (2) と等価ではないことになる。

冠頭標準形への変換規則のうち、直観論理では成り立たないものは以下の通りである。

(1) ${\displaystyle \forall x(\phi \lor \psi )}$ なら ${\displaystyle (\forall x\phi )\lor \psi }$

(2) ${\displaystyle \forall x(\phi \lor \psi )}$ なら ${\displaystyle \phi \lor (\forall x\psi )}$

(3) ${\displaystyle (\forall x\phi )\rightarrow \psi }$ なら ${\displaystyle \exists x(\phi \rightarrow \psi )}$

(4) ${\displaystyle \phi \rightarrow (\exists x\psi )}$ なら ${\displaystyle \exists x(\phi \rightarrow \psi )}$

(5) ${\displaystyle \lnot \forall x\phi }$ なら ${\displaystyle \exists x\lnot \phi }$

なお、(1)と(3)の ${\displaystyle \,\psi }$ では x が自由変項として出現しない。また、(2)と(4)の ${\displaystyle \,\phi }$ では x が自由変項として出現しない。

一部の証明計算は、冠頭標準形の論理式しか扱わない。また、冠頭標準形は算術的階層および解析的階層の構築の基盤である。

ゲーデルによる一階述語論理の完全性定理の証明では、全ての論理式を冠頭標準形に変換することが前提になっている。

• スコーレム標準形

• Hinman, P. (2005年), Fundamentals of Mathematical Logic, A K Peters, ISBN 978-1-56881-262-5 

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