Module 03

冠頭標準形とスコーレム化

量化子を式の先頭にまとめる冠頭標準形（Prenex Normal Form）と、 存在量化子 ∃\exists を関数記号に置き換えて消去するスコーレム化を体験する。

冠頭標準形 (PNF)

任意の一階論理式は、量化子をすべて先頭に追い出した次の形に同値変形できる:

Q1x1 Q2x2 ⋯ Qnxn  Matrix(x1,…,xn)Q_1 x_1\, Q_2 x_2\, \cdots\, Q_n x_n\; \mathit{Matrix}(x_1, \ldots, x_n)

変数の衝突が起きる場合は、束縛変数をα変換（リネーム）して衝突を回避する。

量化子の並べ替えパズル

量化子をドラッグして並べ替え、PNF を作る。同じ変数が並ぶとリネームの提案が出る。

初期式
∀x ∃y ∀z P(x,y,z)\forall x\, \exists y\, \forall z\, P(x, y, z)
冠頭部（ドラッグして並べ替え）
現在の冠頭標準形候補
∀x ∃y ∀z P(x,y,z)\forall x\, \exists y\, \forall z\, P(x, y, z)

スコーレム化クイズ

∃y\exists y を消去するとき、その前に全称量化子があればyy はそれらに依存するため関数記号で消去する。 なければ単なる定数で消去できる。

前に全称量化子がない ∃y。スコーレム化はどうする？

∃y P(y)\exists y\, P(y)