EPR断片のプレノックス定量の順序は重要ですか？

Question

1次論理の効果的命題（EPR）フラグメントは、しばしば∃X.∀Y.Φ(X,Y)という形式のプレノックスで数量化された式のセットとして定義されます。XとYは（おそらくは空の）可変シーケンスです。定量化の順序、つまり∃*∀*はEPRの決定可能性に関係しますか？定量化の順序が入れ替わった場合、決定性を失うか？

特に、私は決定可能なロジックで集合モナドのバインド操作のセマンティクスをキャプチャすることに興味があります。タイプT1の要素のS1を設定する（すなわち、S1はT1 Set型を持つ）、および機能タイプT1 -> T2 Setのfは、セットモナドのバインド操作がS1の各要素に対してfを適用することにより、タイプT2 Setの新しいセットS2を構築し、合併すると考えます結果セット。この現象は、次のSMT-LIBコード/式に捕捉することができる。

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

は、第二のassert文は、標準的なEPR定義に準拠していない形態∀*∃*の定量を有していることを確認します。しかし、私はZ3でそのような公式を扱うときにタイムアウトの問題に直面したことはありませんでした。そして、上記の式が確かにいくつかの決定的な断片であるのだろうかと思います（実用的な解法は理論上の決定可能性を暗示しません。どんな観察も歓迎です。

Answer 1

限定子の順序が異なる場合、もはやEPRではありません。 EPRは、Phiが関数を持たないEA Phiの式のみをカバーします（結合された変数とおそらく自由定数に関する述語のみ）。 EPRではない一次論理のいくつかの決定可能な断片がありますが、Z3はそのような断片の決定手順ではありません。そのような断片を記述する包括的な情報源は、Borger、Graedel、Gurevich、 "The Classical Decision Problem"である。