On “simple” algorithmically undecidable fragments of elementary theory of an infinitely generated free semigroup

We prove algorithmic undecidability of $\exists \forall^2 \exists^3$-theory for a free semigroup of countable rank. This strengthens the classical Quine's (1946) result [1] on algorithmic undecidability of elementary theory of an arbitrary non-cyclic free semigroup.