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.
