存在形前束范式

感謝 ZRQ 學長教育我。

謂詞邏輯任意公式 A，都可化成相應的存在前束范式，並且 A 是普遍有效的當且僅當其存在簽署范式也是普遍有效的。

例子：\((\exist x)(\forall y)(\exist u)P(x, y, u)\) 轉化為存在前束范式：\((\exist x)(\exist y)(\exist u)(P(x, y, u) \and \neg S(x, y)) \or (\forall z)S(x, z))\) 然后進一步化為前束范式即可。

解釋：考慮直接將 \(\forall y\) 變成 \(\exist y\)，前面普遍有效則后面一定普遍有效，但反過來不是。考慮到任意的性質：一個集合全為 1 當且僅當對於任意一個非空子集，都存在一個元素為 1。

再看轉化后的式子，\(\neg S(x, y)\) 代表選擇一個子集，后面的 \(\or\) 代表不可以為空集。