冠頭標準形
冠頭標準形（英: prenex normal form）とは、数理論理学において一階述語論理の論理式の形式であり、量化子が論理式の先頭部分に集められている形式を指す（残りの部分をマトリクスと呼び、先頭の各量化子はマトリクス全体にかかっている）。
古典論理では、あらゆる論理式には等価な冠頭標準形の論理式が存在する。例えば、量化子がなく自由変項を含む論理式 φ(y)、ψ(z)、ρ(x) があるとき、
- [math]\forall x \exists y \exists z (\phi \lor (\psi \rightarrow \rho))[/math]
は [math]\phi \lor (\psi \rightarrow \rho)[/math] をマトリクスとする冠頭標準形であり、
- [math]\forall x ((\exists y \phi) \lor ((\forall z\psi ) \rightarrow \rho))[/math]
は上と論理的に等価だが冠頭標準形でない論理式である。
冠頭形への変換
全ての一階述語論理の論理式には（古典論理では）論理的に等価な冠頭標準形の論理式が存在する。いくつかの変換規則を再帰的に適用することで、論理式を冠頭標準形に変換できる。規則は、論理式に出現する論理演算子の種類によって異なる。
論理積と論理和
- [math](\forall x \phi) \land \psi[/math] は [math]\forall x ( \phi \land \psi)[/math] と等価
- [math](\forall x \phi) \lor \psi[/math] は [math]\forall x ( \phi \lor \psi)[/math] と等価
および
- [math](\exists x \phi) \land \psi[/math] は [math]\exists x (\phi \land \psi)[/math] と等価
- [math](\exists x \phi) \lor \psi[/math] は [math]\exists x (\phi \lor \psi)[/math] と等価
である。これらの規則は、x が ψ の中で自由変項として現れない場合に妥当である。もし x が ψ の中に自由変項として現れた場合、他の自由変項と置き換える必要がある。
例えば、環の言語で、
- [math](\exists x (x^2 = 1)) \land (0 = y)[/math] は [math]\exists x ( x^2 = 1 \land 0 = y)[/math] と等価である。
しかし
- [math](\exists x (x^2 = 1)) \land (0 = x)[/math] は [math]\exists x ( x^2 = 1 \land 0 = x)[/math] と等価ではない。
左の式は、自由変項 x が 0 のとき任意の環で真だが、右の式には自由変項がなく、どんな環でも偽である。
否定
否定の規則は
- [math]\lnot \exists x \phi[/math] は [math]\forall x \lnot \phi[/math] と等価
および
- [math]\lnot \forall x \phi[/math] は [math]\exists x \lnot \phi[/math] と等価
である。
含意
含意には4つの規則がある。そのうち2つは仮説から量化子を除去するもので、残る2つは帰結から量化子を除去する。これらの規則は、含意 [math]\phi \rightarrow \psi[/math] を [math]\lnot \phi \lor \psi[/math] と書き換えた上で上述の論理和に関する規則を適用することで得られる。論理和の規則と同様、ある部分論理式に出現する量化された自由変項が他の部分論理式に出現しないことが条件になっている。
仮説部分から量化子を除去する規則は以下の通り。
- [math](\forall x \phi ) \rightarrow \psi[/math] は [math]\exists x (\phi \rightarrow \psi)[/math] と等価
- [math](\exists x \phi ) \rightarrow \psi[/math] は [math]\forall x (\phi \rightarrow \psi)[/math] と等価
帰結部分から量化子を除去する規則は以下の通り。
- [math]\phi \rightarrow (\exists x \psi)[/math] は [math]\exists x (\phi \rightarrow \psi)[/math] と等価
- [math]\phi \rightarrow (\forall x \psi)[/math] は [math]\forall x (\phi \rightarrow \psi)[/math] と等価
例
[math]\phi[/math]、[math]\psi[/math]、[math]\rho[/math] は量化子を含まない論理式であり、共通の自由変項を持たないものとする。次の論理式を考える。
- [math] (\phi \lor \exists x \psi) \rightarrow \forall z \rho[/math]
上述の規則群を最も内側の部分論理式から再帰的に適用していく。すると、以下のような一連の論理的に等価な論理式が得られる。
- [math] ( \exists x (\phi \lor \psi)) \rightarrow \forall z \rho[/math]
- [math] \forall x (( \phi \lor \psi) \rightarrow \forall z \rho)[/math]
- [math]\forall z \forall x ( ( \phi \lor \psi) \rightarrow \rho)[/math]
なお、元の論理式と等価な冠頭標準形は唯一ではない。例えば、上の例で仮説部ではなく帰結部を先に変換すると、次の冠頭標準形が得られる。
- [math]\forall x \forall z ( ( \phi \lor \psi) \rightarrow \rho)[/math]
直観論理
冠頭形への変換規則は古典論理であることに依存している。直観論理では、全ての論理式に等価な冠頭標準形があるわけではない。例えば否定が問題になるが、それだけではない。含意も直観論理と古典論理では扱いが異なる。直観論理では、含意を論理和と否定を使った形式に置き換えられない。
BHK解釈は、なぜ一部の論理式が直観論理で等価な冠頭標準形を持たないのかを示している。この解釈では、次の論理式
- [math](\exists x \phi) \rightarrow \exists y \psi \qquad (1)[/math]
を証明は、特定の x と φ(x) の証明を与えられたとき、特定の y と ψ(y) の証明を生成する関数と考える。この場合、与えられた x の値から y の値を計算することは可能である。しかし、次の論理式
- [math]\exists y ( \exists x \phi \rightarrow \psi), \qquad (2)[/math]
の証明は、y の特定の値を生成し、[math]\exists x \phi[/math] の証明を ψ(y) の証明に変換する関数である。φ を満足する任意の x を使って ψ を満足する y を構築できるが、そのような x の知識なしに y を構築できないなら、論理式 (1) は論理式 (2) と等価ではないことになる。
冠頭標準形への変換規則のうち、直観論理では成り立たないものは以下の通りである。
- (1) [math]\forall x (\phi \lor \psi)[/math] なら [math](\forall x \phi) \lor \psi[/math]
- (2) [math]\forall x (\phi \lor \psi)[/math] なら [math]\phi \lor (\forall x \psi)[/math]
- (3) [math](\forall x \phi) \rightarrow \psi[/math] なら [math]\exists x (\phi \rightarrow \psi)[/math]
- (4) [math]\phi \rightarrow (\exists x \psi)[/math] なら [math]\exists x (\phi \rightarrow \psi)[/math]
- (5) [math]\lnot \forall x \phi[/math] なら [math]\exists x \lnot \phi[/math]
なお、(1)と(3)の [math]\,\psi[/math] では x が自由変項として出現しない。また、(2)と(4)の [math]\,\phi[/math] では x が自由変項として出現しない。
用途
一部の証明計算は、冠頭標準形の論理式しか扱わない。また、冠頭標準形は算術的階層および解析的階層の構築の基盤である。
ゲーデルによる一階述語論理の完全性定理の証明では、全ての論理式を冠頭標準形に変換することが前提になっている。
関連項目
参考文献
- Hinman, P. (2005年), Fundamentals of Mathematical Logic, A K Peters, ISBN 978-1-56881-262-5