A reduction of the decidability problem of the theory of a free group (Q1086673)

Let F be a non-abelian free group with free generators \(a_ 1,...,a_ n\) and L the first order language with non-logical symbols \(\cdot\), \(^{-1}\), 1, \(a_ 1,...,a_ n\). The author proves that for each L- sentence \(\phi\) a prenex L-sentence of the form \[ Q_ 1x_ 1...Q_ mx_ m\exists y(w(x_ 1,...,x_ m,y,a_ 1,...,a_ n)=1\quad \&\quad y\neq 1) \] that is F-equivalent to \(\phi\) can be effectively constructed. He believes that the result enables to concretize further investigations on Tarski's problem of decidability of the theory of a free group.