On decidability of the decomposability problem for finite theories

We consider the decomposability problem for elementary theories, i.e. the problem of deciding whether a theory has a nontrivial representation as a union of two (or several) theories in disjoint signatures. For finite universal Horn theories, we prove that the decomposability problem is $ \sum _1^0 $ \sum _1^0 -complete and, thus, undecidable. We also demonstrate that the decomposability problem is decidable for finite theories in signatures consisting only of monadic predicates and constants.