The first-order theory of one-step rewriting is undecidable

The theory of one-step rewriting for a given rewrite system R and signature Sigma is the first-order theory of the following structure: Its universe consists of all Sigma-ground terms, and its only predicate is the relation ''x rewrites to y in one step by R''. The structure contains no function symbols and no equality. We show that there is no algorithm deciding the There Exists*For All*-fragment of this theory for an arbitrary rewrite system. The proof uses both non-linear and non-shallow rewrite rules. As a refinement of the proof, we show that the There Exists*For All*-fragment of the first-order theory of encompassment (reducibility by rewrite rules) together with one-step rewriting by the rule f(x) --> g(x) is undecidable.