Elementary theory of free non-abelian groups

We prove that any two non-abelian free groups have the same elementary theory and that this theory is decidable. These results solve two questions that were raised by Tarski in 1945.