Satisfaction of existential theories in finitely presented groups and some embedding theorems

The main result is that for every recursively enumerable existential consistent theory Γ (in the usual language of group theory), there exists a finitely presented SQ-universal group H such that Γ is satisfied in every nontrivial quotient of H. Furthermore if Γ is satisfied in some group with a soluble word problem, then H can be taken with a soluble word problem. We characterize the finitely generated groups with soluble word problem as the finitely generated groups G for which there exists a finitely presented group H all of the nontrivial quotients of which embed G. We prove also that for every countable group G, there exists a 2-finitely generated SQ-universal group H such that every nontrivial quotient of H embeds G.