冠頭正規形

述語計算の式は、接頭辞と呼ばれる量指定子と束縛変数の文字列と、それに続く行列と呼ばれる量指定子のない部分として書かれた場合、冠頭[ 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つです。これらの規則は、含意 を と書き直し、上記の論理和と否定の規則を適用することで導出できます。論理和の規則と同様に、これらの規則では、一方の部分式で量化された変数が、もう一方の部分式では自由出現しないことが求められます。 ${\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はゼロより小さいと述べています。後者は、xがnより小さい自然数nが存在する場合、xはゼロより小さいと述べています。どちらの記述も誤りです。前者はn=2 の場合に成り立ちません。なぜなら、x=1はnより小さいが、ゼロより小さくないからです。後者はx=1の場合に成り立ちません。なぜなら、自然数n=2はx<nを満たしますが、x=1はゼロより小さくないからです。

例

、、が量指定子を含まない式であり、これらの式のうち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 つの全称量指定子の順序は、ステートメントの意味/真理値を変更しません。

直観主義論理

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

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 )}$

（4）は、${\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 }$

参照

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

注記

1. 「prenex」という用語はラテン語の praenexus（前で縛られた、または縛られた）に由来し、praenectereの過去分詞である[1]（2011年5月27日アーカイブ[2]）
2. ヒンマン、P.（2005）、110ページ
3. ヒンマン、P.（2005）、111ページ

参考文献

• リチャード・L・エプスタイン（2011年12月18日）. 『古典数理論理学：論理の意味論的基礎』. プリンストン大学出版局. pp. 108–. ISBN 978-1-4008-4155-4。
• ピーター・B・アンドリュース（2013年4月17日）『数理論理学と型理論入門：証明を通して真理へ』シュプリンガー・サイエンス＆ビジネス・メディア、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