As is well-known, the Beraays-Schönfinkel-Ramsey class of all prenex ∃∀ -sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are € and =. no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the wellfoundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper. © 2010. Association for Symbolic Logic.