Effectively Propositional (EPR) fragment of the first-order logic is often defined as the set of prenex-quantified formulas of the form ∃X.∀Y.Φ(X,Y), where X and Y are (possibly empty) variable sequences. Does the order of quantification, i.e. ∃*∀*, matter for the decidability of EPR? Do we lose decidability if the order of quantification is switched?
In particular, I am interested in capturing the semantics of the set-monadic bind operation in decidable logic. Given as set S1 of elements of type T1 (i.e., S1 has type T1 Set), and a function f of type T1 -> T2 Set, set-monad's bind operation constructs a new set S2 of type T2 Set by applying f on each element of S1, and unioning the resultant sets. This behavior can be captured in the following SMT-LIB code/formula:
(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)))) ))
Observe that the second assert statement has quantification of the form ∀*∃*, which does not conform to the standard EPR definition. I however never faced time-out problems when working with such formulas on Z3, and I wonder if my formula above is indeed in some decidable fragment (while acknowledging that solvability in practice doesn't imply decidability in theory). Any observations are welcome.
It is no longer EPR if the order of quantifiers is different. EPR only covers formulas of the form EA Phi, where Phi has no functions (only predicates over the bound variables and maybe free constants). There are some decidable fragments of first order logic that are not EPR, but Z3 is not a decision procedure for such fragments. A comprehensive source that describes such fragments is Borger, Graedel, Gurevich, "The Classical Decision Problem".