冠頭正規形

述語計算の式は、接頭辞と呼ばれる量指定子と束縛変数の文字列に、行列と呼ばれる量指定子のない部分が続く形で書かれる場合、冠頭^[1]正規形（PNF）である。^[2]命題論理の正規形（例えば、選言正規形や連言正規形）とともに、自動定理証明に有用な標準的な正規形を提供する。

古典論理におけるすべての式は、冠頭正規形の式と論理的に同等である。例えば、、、が量指定子のない式で、自由変数が以下の通りである 場合、${\displaystyle \phi (y)}$${\displaystyle \psi (z)}$${\displaystyle \rho (x)}$

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

は行列 の冠頭正規形であるが、 ${\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}$

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

論理的には同等ですが、冠頭正規形ではありません。

すべての一階述語論理式は、冠頭正規形のいくつかの式と論理的に同等です（古典論理）。^[3] 式を冠頭正規形に変換するために再帰的に適用できる変換規則がいくつかあります。規則は、式に どの論理接続子が現れるかどうかによって異なります。

連言と選言の規則は、

${\displaystyle (\forall x\phi )\land \psi }$は、（軽度の）追加条件と同等であり、または、同等に、（少なくとも1つの個体が存在することを意味する）${\displaystyle \forall x(\phi \land \psi )}$${\displaystyle \exists x\top }$${\displaystyle \lnot \forall x\bot }$

${\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 )}$${\displaystyle \exists x\top }$

この同値性は、が の自由変数として現れないときに有効です。 がで自由変数として現れる場合は、 の境界の名前を変更して、同等の を得ることができます。 ${\displaystyle x}$${\displaystyle \psi}$${\displaystyle x}$${\displaystyle \psi}$${\displaystyle x}$${\displaystyle (\exists x\phi )}$${\displaystyle (\exists x'\phi [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 (\exists x(x^{2}=1))\land (0=x)}$${\displaystyle (\exists x'(x'^{2}=1))\land (0=x)}$${\displaystyle \exists x'(x'^{2}=1\land 0=x)}$

否定のルールは、

${\displaystyle \lnot \exists x\phi }$は、${\displaystyle \forall x\lnot \phi }$

そして

${\displaystyle \lnot \forall x\phi }$は と同等です。${\displaystyle \exists x\lnot \phi }$

含意には 4 つの規則があります。2 つは前件から量指定子を削除し、2 つは後件から量指定子を削除します。これらの規則は、含意 を と書き直し、上記の選言と否定の規則を適用することで導き出せます。選言の規則と同様に、これらの規則では、1 つの部分式で量指定されている変数が、他の部分式で自由に現れないことが求められます。 ${\displaystyle \phi \rightarrow \psi }$${\displaystyle \lnot \phi \lor \psi }$

先行詞から量指定子を削除する規則は次のとおりです (量指定子の変更に注意してください)。

${\displaystyle (\forall x\phi )\rightarrow \psi }$は（ という仮定の下で）と同等である。${\displaystyle \exists x(\phi \rightarrow \psi )}$${\displaystyle \exists x\top }$

${\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 \exists x\top }$

${\displaystyle \phi \rightarrow (\forall x\psi )}$は と同等です。${\displaystyle \forall x(\phi \rightarrow \psi )}$

例えば、量化の範囲が非負の自然数（すなわち）である場合、次の文は ${\displaystyle n\in \mathbb {N} }$

${\displaystyle [\forall n\in \mathbb {N} (x<n)]\rightarrow (x<0)}$

は論理的に次の文 と同等である。

${\displaystyle \exists n\in \mathbb {N} [(x<n)\rightarrow (x<0)]}$

前者の文は、xが任意の自然数より小さい場合、x は0 より小さい、ということを述べています。後者の文は、 xがnより小さい場合、 x は 0 より小さいような自然数nが存在する、ということを述べています。どちらの文も真です。前者の文が真なのは、xが任意の自然数より小さい場合、 xは最小の自然数 (0) より小さくなければならないためです。後者の文が真なのは、n=0であるため、含意がトートロジーになるからです。

括弧の配置は定量化の範囲を意味し、これは式の意味にとって非常に重要であることに注意してください。次の 2 つのステートメントについて考えてみましょう。

${\displaystyle \forall n\in \mathbb {N} [(x<n)\rightarrow (x<0)]}$

そして、論理的に同等のステートメント

${\displaystyle [\exists n\in \mathbb {N} (x<n)]\rightarrow (x<0)}$

前者のステートメントは、任意の自然数nに対して、xがnより小さい場合、x は0 より小さいことを述べています。 後者のステートメントは、 x がnより小さいような自然数n が存在する場合、x は0 より小さいことを述べています。 どちらのステートメントも偽です。 前者のステートメントはn=2には当てはまりません。なぜなら、x=1はnより小さいが、 0 より小さくないからです。 後者のステートメントはx=1には当てはまりません。なぜなら、自然数n=2はx<n を満たしますが、x=1は 0 より小さくないからです。

、、が量指定子のない式であり、これらの式のうち2つが自由変数を共有していないと仮定する。次の式を考える。 ${\displaystyle \phi}$${\displaystyle \psi}$${\displaystyle \rho}$

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

最も内側の部分式から始めて規則を再帰的に適用することで、論理的に同等な次の一連の式が得られます。

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

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

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

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

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

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

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

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

これは元の式と等価な冠頭形式だけではありません。例えば、上の例で結果が先行詞の前にあるとすると、冠頭形式は

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

取得できます:

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

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

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

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

同じスコープを持つ 2 つの全称量指定子の順序によって、ステートメントの意味/真理値が変わることはありません。

式を冠頭形式に変換する規則では、古典論理が多用されます。直観主義論理では、すべての式が冠頭形式と論理的に同等であるとは限りません。否定接続子は 1 つの障害ですが、唯一の障害ではありません。直観主義論理では、含意演算子も古典論理とは扱いが異なります。直観主義論理では、含意演算子は選言と否定を使用して定義できません。

BHK解釈は、なぜいくつかの式が直観的に同値な冠頭形式を持たないのかを示している。この解釈では、

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

は、具体的なxと の証明が与えられると、具体的なyと の証明を生成する関数です。この場合、yの値はxの与えられた値から計算できます。 の証明 ${\displaystyle \phi (x)}$${\displaystyle \psi (y)}$

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

一方、はyの単一の具体的な値と、 の任意の証明を の証明に変換する関数を生成します。 を満たす各xを使用して を満たすyを構築できるが、そのようなx を知らずにそのようなy を構築できない場合、式 (1) は式 (2) と同等ではありません。 ${\displaystyle \exists x\phi }$${\displaystyle \psi (y)}$${\displaystyle \phi }$${\displaystyle \psi }$

直観主義論理では 失敗する式を冠頭形式に変換するための規則は次のとおりです。

（１）は、${\displaystyle \forall x(\phi \lor \psi )}$${\displaystyle (\forall x\phi )\lor \psi }$

（２）は、${\displaystyle \forall x(\phi \lor \psi )}$${\displaystyle \phi \lor (\forall x\psi )}$

（３）は、${\displaystyle (\forall x\phi )\rightarrow \psi }$${\displaystyle \exists x(\phi \rightarrow \psi )}$

（４）は、${\displaystyle \phi \rightarrow (\exists x\psi )}$${\displaystyle \exists x(\phi \rightarrow \psi )}$

（５）は、${\displaystyle \lnot \forall x\phi }$${\displaystyle \exists x\lnot \phi }$

（xは（1）と（3）では自由変数として現れない； xは（2）と（4）では自由変数として現れない）。 ${\displaystyle \,\psi }$${\displaystyle \,\phi }$

いくつかの証明計算は、式が冠頭正規形で記述された理論のみを扱います。この概念は、算術階層と解析階層を開発するために不可欠です。

ゲーデルによる一階述語論理の完全性定理の証明は、すべての式が冠頭正規形で書き直されていることを前提としています。

タルスキの幾何学の公理は、その文がすべて普遍存在形式で記述できる論理体系です。普遍存在形式は、あらゆる普遍量指定子があらゆる存在量指定子に先行する冠頭標準形の特殊なケースであり、そのためすべての文は という形式に書き直すことができます。ここで は量指定子を含まない文です。この事実により、タルスキはユークリッド幾何学が決定可能であることを証明できました。 ${\displaystyle \forall u}$ ${\displaystyle \forall v}$ ${\displaystyle \ldots }$ ${\displaystyle \exists a}$ ${\displaystyle \exists b}$ ${\displaystyle \phi }$${\displaystyle \phi }$

無料辞書『ウィクショナリー』でprenex を調べてください。

• 算術階層
• ハーブブランド化
• スコレム化

• リチャード・L・エプスタイン（2011年12月18日）。古典数学論理学：論理の意味論的基礎。プリンストン大学出版局。pp. 108– 。ISBN 978-1-4008-4155-4。
• ピーター・B・アンドリュース（2013年4月17日）。「数理論理学と型理論入門：証明を通して真実へ」Springer Science & Business Media。pp. 111– 。ISBN 978-94-015-9934-4。
• エリオット・メンデルソン（1997年6月1日）。『数学論理入門』第4版。CRC Press。pp. 109– 。ISBN 978-0-412-80830-2。
• ヒンマン、ピーター（2005）、数学論理の基礎、AKピーターズ、ISBN 978-1-56881-262-5