We study the connections between recognizable tree languages and rewrite systems. We investigate some decision problems. Particularly, let us consider the property (P): a rewrite system S is such that, for every recognizable tree language F, the set of S-normal forms of terms in F is recognizable too. We prove that the property (P) is undecidable. We prove that the existential fragment of the theory of ground term algebras modulo a congruence $$\mathop \leftrightarrow \limits^* E$$ generated by a set E of equations such that there exists a finite, noetherian, confluent rewrite system S satisfying (P) with $$\mathop \leftrightarrow \limits^* S = \mathop \leftrightarrow \limits^* E$$ is undecidable. Nevertheless, we develop a decision procedure for the validity of linear formulas in a fragment of such a theory.