EPR 片段中 prenex 定量的顺序重要吗？

Question

一阶逻辑的有效命题 (EPR) 片段通常被定义为以下形式的 prenex 量化公式集\xe2\x88\x83X.\xe2\x88\x80Y.\xce\xa6(X,Y)，其中X和Y是（可能为空）变量序列。量化的顺序（即 ）\xe2\x88\x83*\xe2\x88\x80*对于 EPR 的可判定性重要吗？如果改变量化顺序，我们会失去可判定性吗？

\n\n

特别是，我对捕获可判定逻辑中的 set-monadic 绑定操作的语义感兴趣。给定S1类型的元素集T1（即S1具有类型）和类型的T1 Set函数，set-monad 的绑定操作通过应用于每个元素来构造一个新的类型集fT1 -> T2 SetS2T2 SetfS1并联合结果集可以在以下 SMT-LIB 代码/公式中捕获此行为：

\n\n

(declare-sort T1)\n(declare-sort T2)\n;; We encode T1 Set as a boolean function on T1\n(declare-fun S1 (T1) Bool)\n(declare-fun S2 (T2) Bool)\n;; Thus, f becomes a binary predicate on (T1,T2)\n(declare-fun f (T1 T2) Bool)\n(assert (forall ((x T1)(y T2)) (=> (and (S1 x) (f x y)) \n                                   (S2 y))))\n(assert (forall ((y T2)) (exists ((x T1)) (=> (S2 y) \n                                              (and (S1 x) (f x y)))) ))\n

\n\n

观察第二个断言语句具有以下形式的量化\xe2\x88\x80*\xe2\x88\x83*，这不符合标准 EPR 定义。然而，在 Z3 上使用此类公式时，我从未遇到过超时问题，并且我想知道上面的公式是否确实处于某些可判定的片段中（同时承认实践中的可解性并不意味着理论上的可判定性）。欢迎任何意见。

\n

Answer 1

如果量词的顺序不同，则不再是 EPR。EPR 仅涵盖 EA Phi 形式的公式，其中 Phi 没有函数（仅对绑定变量以及可能的自由常量进行谓词）。有一些一阶逻辑的可判定片段不是 EPR，但 Z3 不是此类片段的判定过程。描述此类片段的综合资料来源是 Borger、Graedel、Gurevich 的“经典决策问题”。