# Is the validity of some instance of an equational problem decidable?

Is the following FOL-problem (equality is a logical symbol) effectively decidable?

Given. A finite equation system $E$ and an equation $s = t$.

Question. Is there a substitution $\sigma$, such that $\sigma(E) \models \sigma(s = t)$?

Some useful information.

1. Obviously one can restrict $\sigma$ to be a ground substitution.

2. This problem is decidable: Given a finite system $E$ of
ground equations and a ground equation $s = t$, does $E \models s = t$
hold? (c.f. [1: Corollary 4.3.6])

References

[1] Franz Baader, Tobias Nipkow: Term Rewriting and All That, © 1998 Cambridge University Press.