4.62 (1973)

Yes, there does; for example, $\mathfrak{A}^5$. Indeed, it is shown in (V. N. Remeslennikov, Algebra and Logic, 12, no. 5 (1975), 327–346) that there exists a finitely presented group $G = \langle x_1, \dots, x_n \mid w_1, \dots, w_m, \text{mod }\mathfrak{A}^5 \rangle$ in $\mathfrak{A}^5$ with undecidable word problem. We put $\Phi_w = (\forall x_1, \dots, x_n)((w_1 = 1) \wedge \dots \wedge (w_m = 1) \to (w = 1))$, where $w$ runs over all the words in $x_1, \dots, x_n$. Clearly, there is no algorithm to decide whether a formula $\Phi_w$ is true in $\mathfrak{A}^5$. (V. N. Remeslennikov, 1976.)