The elementary theory of a non-commutative free group with a predicate for equality of length is proved hereditarily undecidable. This theory is shown to be ‘finitely axiomatizable’ modulo the second order stipulation that some centralizer be free cyclic. The theory of free groups in a weaker language using only a predecessor concept is investigated in the hope of shedding some light on Tarski's problems.