存在形前束范式

感谢 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\) 代表不可以为空集。