Advances in Pure Mathematics
Vol.05 No.04(2015), Article ID:55221,19 pages
10.4236/apm.2015.54023
The Tarski Problems and Their Solutions
Benjamin Fine1, Anthony Gaglione2, Gerhard Rosenberger3, Dennis Spellman4
1Department of Mathematics Fairfield University, Fairfield, USA
2Department of Mathematics, United States Naval Academy, Annapolis, USA
3Department of Mathematics, University of Hamburg, Hamburg, Germany
4Department of Mathematics, Temple University, Philadelphis, USA
Email: fine@fairfield.edu, anthony.gaglione@usna.edu, gerhard.rosenberger@uni-math,hamburg.de, dennisspellman@aol.com
Copyright © 2015 by authors and Scientific Research Publishing Inc.
This work is licensed under the Creative Commons Attribution International License (CC BY).
http://creativecommons.org/licenses/by/4.0/



Received 19 January 2015; accepted 20 February 2015; published 31 March 2015
ABSTRACT
Around 1945, Alfred Tarski proposed several questions concerning the elementary theory of non- abelian free groups. These remained open for 60 years until they were proved by O. Kharlampovich and A. Myasnikov and independently by Z. Sela. The proofs, by both sets of authors, were monumental and involved the development of several new areas of infinite group theory. In this paper we explain precisely the Tarski problems and what has been actually proved. We then discuss the history of the solution as well as the components of the proof. We then provide the basic strategy for the proof. We finish this paper with a brief discussion of elementary free groups.
Keywords:
non-abelian free group, elementary theory, Tarski problems, elementary free groups, algebraic geometry over groups

1. Introduction
Around 1945, Alfred Tarski proposed several questions concerning the elementary theory of non-abelian free groups. These questions then became well-known conjectures but remained open for 60 years. They were proved in the period 1996-2006 independently by O. Kharlampovich and A. Myasnikov [1] -[5] , and by Z. Sela [6] -[10] . The proofs, by both sets of authors, were monumental, and involved the development of several new areas of infinite group theory. Because of the tremendous amount of material developed and used in the two different proofs, the details of the solution are largely unknown, even to the general group theory population. The book [11] presents an introductory guide through the material. In this paper we provide, for a general mathematical audience, who know some infinite group theory, an introduction to both the Tarksi conjectures and the vast new ideas that go into the proof. These ideas straddle the line between algebra and mathematical logic and hence most group theorists don’t know enough logic to fully understand the details while in the other direction most logicians don’t understand enough infinite group theory.
In the next section we define and explain both elementary and universal theory. With these in hand we can explain precisely the Tarski problems and what has been actually proved. We then in section 4 discuss the history of the solution as well as the components of the proof. This involves the development of several new areas of infinite group theory.
There are five essential parts of the overall proof: the structure theory of fully residually free groups, called limit groups in the Sela approach; the Makhanin-Razborov techniques for handling solutions of equations in free groups; the extension of classical algebraic geometry to algebraic geometry over groups, especially over free groups. Sela calls this diophantine geometry over groups, an elimination process that reduces the solution of systems of equations over free groups to solutions of certain special systems of quadratic equations, and an implicit function theorem that allows for quantifer elimination and then an induction on the number of quantifiers.
We then provide the basic strategy for the proof which utilizes all the components mentioned. In section 6 we give a very brief outline of the proof.
As part of the proof both sets of authors provide a complete characterization of finitely generated groups that have the same elementary theory as the class of non-abelian free groups. These are called elementary free or elementarily free groups. In the approach of Kharlampovich-Myasnikov these are called special NTQ-groups while Sela calls them w-residually free towers. The most prominent set of examples of non-free elementary free groups are the orientable surface groups
of genus
and the non-orientable surface groups
of genus
. In the final section, we finish this paper with a discussion of elementary free groups and what we call something for nothing results.
2. Elementary and Universal Theory
The original Tarski Problems or Tarski Conjectures asked, among other things, whether all non-abelian free groups satisfy the same first-order or elementary theory. Here we explain and review universal and elementary theory.
A first-order sentence in group theory has logical symbols
but no quantification over sets. A first-order theorem in a free group is a theorem that says a first-order sentence is true in all non-abelian free groups. We make this a bit more precise:
We start with a first-order language appropriate for group theory. This language, which we denote by
, is the first-order language with equality containing a binary operation symbol. a unary operation symbol−1 and a
constant symbol 1. A universal sentence of
is one of the form
where
is a tuple of distinct
variables,
is a formula of
containing no quantifiers and containing at most the variables of
.
Similarly an existential sentence is one of the form
where
and
are as above. A
universal-existential sentence is one of the form
. Similarly defined is an
existential-universal sentence. It is known that every sentence of 
where 




and 



If G is a group, then the universal theory of G consists of the set of all universal sentences of 


The set of all sentences of 

We say that two groups G and H are elementarily equivalent (symbolically
same first-order theory, that is
Group monomorphisms which preserve the truth of first-order formulas are called elementary embeddings. Specifically, if H and G are groups and
is a monomorphism then 





In H if and only if
is true in G. If H is a subgroup of G and the inclusion map 
Two very important concepts in the elementary theory of groups, are completeness and decidability. Given a non-empty class of groups 











For more information on elementary theory in general see [11] -[13] .
3. The Tarski Problems
Tarski first asked the general question whether all non-abelian free groups share the same elementary theory. At the end of this section, we will present some motivation for this idea. Vaught, a student of Tarksi’s, proved almost immediately that all free groups of infinite rank do have the same elementary theory, and thus reduced the question to the class of non-abelian free groups of finite rank. After this, Tarski’s question was formalized into the following conjectures.
Tarski Conjecture 1 Any two non-abelian free groups are elementarily equivalent. That is any two non- abelian free groups satisfy exactly the same first-order theory.
Tarski Conjecture 2 If the non-abelian free group H is a free factor in the free group G then the inclusion map 
The second conjecture is stronger than the first and in fact implies the first. If true, then the theory of the non-abelian free groups would be complete, that is given a sentence 



After a long series of partial results, that we will describe in subsequent sections, the positive solution to the Tarksi conjectures was given by O. Kharlampovich and A. Myasnikov [1] -[5] and independently by Z. Sela [6] - [10] . The proofs by both sets of authors involved the development of whole new areas of mathematics, in particular an algebraic geometry (Sela calls this diophantimne geometry) over free groups. The basic theorems eventually proved were:
Theorem 1 (Tarski 1) Any two non-abelian free groups are elementarily equivalent. That is any two non- abelian free groups satisfy exactly the same first-order theory.
Theorem 2 (Tarski 2) If the non-abelian free group H is a free factor in the free group G then the inclusion map 
In addition to the completeness of the theory of the non-abelian free groups, the question of its decidability also arises. The decidability of the theory of non-abelian free groups means the question of whether there exists a recursive algorithm which, given a sentence 


Theorem 3 (Tarski 3) The elementary theory of the non-abelian free groups is decidable.
Although Tarksi was never explicit on the origin of the basic question, it is motivated by several basic results, and concepts, in the theory of free groups (see [11] [14] [15] for complete discussions of free groups). First is the observation that most free group properties, involving elements, are rank independent, that is, true for all free groups independent of rank. For example all non-abelian free groups are torsion-free and all abelian subgroups of non-abelian free groups are cyclic.
A second possible motivation, which also shows that all non-abelian free groups have the same universal theory, is the following. Let 





This shows that 

If 

vation combined with the observations above prove that all non-abelian free groups have the same universal theory and hence are universally equivalent.
Theorem 4 All non-abelian free groups are universally equivalent.
A group with the same universal theory as a non-abelian free group is called a universally free group. The above theorem then opens the question as to whether the class of universally free groups extends beyond the class of free groups. One of the initial steps toward the proof of the Tarksi problems was a group theoretical characterization of universally free groups. In the finitely generated case these turn out to be the non-abelian fully residually free groups. We will introduce this class of groups in the next section.
4. The History of the Solution
The final proof of the Tarski theorems was a monumental collection of work by both sets of authors. In addition to dealing with already existing ideas in group theory and logic, the solution involved the development of several new areas of group theory. In particular three areas of group theory had to be fully developed before the proof could be completed. These were:
1) The theory of fully residually free groups. In Sela’s approach these were called limit groups;
2) The Makhanin-Razborov technique for solving equations within free groups;
3) The development of algebraic geometry over groups. Sela calls this diophantine geometry.
We will discuss each of these in turn. First we look at the initial partial results that were done between the statement of the problem by Tarksi (in 1945) and the final proofs (1998-2006).
The first progress was due to Vaught, a student of Tarski, who showed that the Tarski Conjectures 1, 2 are true if G and H are both free groups of infinite rank. This reduced the problem to free groups of finite rank, that is, in showing that all non-abelian free groups of finite rank share the same elementary theory or even stronger that the embedding of a free group of rank m into a free group of rank n, with
The basic idea in Vaught’s proof is to use the following criteria for elementary embeddings; if 
subgroup of H and that to every finite subset 


automorphism 




The next significant progress was due to Merzljakov [16] . A positive sentence is a first-order sentence which is logically equivalent to a sentence constructed using (at most) the connectives
Merzljakov showed that the non-abelian free groups have the same positive theory.
Theorem 5 (Merzljakov) [16] All non-abelian free groups have the same positive theory.
Merzljakov’s proof used what are now called generalized equations and a quantifier elimination process. This was a precursor to the methods used in the eventual solution of the overall Tarksi problems.
As we pointed out in the previous section, two non-abelian free groups satisfy the same universal theory. Sacerdote [17] proved that this could be extended to universal-existential sentences. The set of universal- existential sentences true in a group G is called the 
Theorem 6 (Sacerdote) [17] All non-abelian free groups have the same 
That all non-abelian free groups have the same universal theory coupled with the fact that universally free is equivalent to existentially free says that Tarski Conjecture 1 is true if there is only one quantifier. Sacerdote’s extension to 
A first step to the initial proofs was to completely characterize those groups that are universally free. This was accomplished within the study of fully residually free groups. A group G is residually free if for each non- trivial 


A group G is fully residually free if for each finite subset of non-trivial elements 
is a homomorphism 


Fully residually free groups arise in Sela’s approach as limiting groups of homomorphisms from a group G into a free groups. Sela shows that such groups in the finitely generated case are equivalent to fully residually free groups. Hence. a finitely generated fully residually free group is also called a limit group. This has become the more common designation.
Two concepts are crucial in the study of limit groups. A group G is commutative transitive or CT if commutativity is transitive on the set of non-trivial elements of G. That is if 



maximal abelian subgroups are malnormal. A subgroup 

that
In 1967 Benjamin Baumslag [18] proved the following result who’s innocuous beginnings belied its much greater later importance. It was in this paper that the concept of full residual freeness was first explored.
Theorem 7 (Baumslag [18] ) Suppose G is residually free. Then the following are equivalent:
1) G is fully residually free;
2) G is commutative transitive.
Gaglione and Spellman [19] and independently Remeslennikov [20] extended B. Baumslag’s Theorem and this extension became one of the cornerstones of the proof of the Tarksi problems
Theorem 8 [19] [20] Suppose G is residually free. Then the following are equivalent:
1) G is fully residually free;
2) G is commutative transitive;
3) G is universally free if non-abelian.
Further the result can be extended to include the equivalence with CSA. In addition Remeslennikov and independently Chiswell (see [21] ) showed that if a group G is finitely generated then being fully residually free is equivalent to being universally free. Therefore the finitely generated universally free groups are precisely the finitely generated fully residually free groups which are non-abelian
Theorem 9 Let G be finitely generated and non-abelian. Then G is a limit group if and only if G is uni- versally free.
Ciobanu, Fine and Rosenberger [22] recently greatly extended the class of groups satisfying both B. Baumslag’s original theorem and the theorem of Gaglione, Spellman and Remeslennikov.
The solution of the Tarski Conjectures involved analyzing groups which have the same elementary theory as a free group. Clearly this includes the universally free groups and therefore the theory of limit groups became essential to the proof and to analyzing those groups which have the same elementary theory as a free group
It was clear from the beginning that to deal with the Tarski problems it was necessary to give a precise definition of solution sets of equations and inequations over free groups. In this direction Lyndon [23] introduced the concept of an exponential group, that is a group which allows parametric exponents in an associative unitary ring A. In particular he studied the free exponential group 




Lyndon’s original motivation for introducing exponential groups was from the solution sets of equations over free groups. In [23] he found that the solution set of any equation with one variable over a free group F can be obtained from finitely many parametric words by specializing their parameters in the integers. A parametric
word with parameters in 
concatenations and exponentiations from


obtains an element of F. Lyndon proved that for any equation with one variable over a free group 
effectively find a finite set of parametric words with parameters from the ring 
solution of this equation can be obtained from some specialization of these words. Appel [34] refined Lyndon’s result and showed that the solution set of a one variable equation over a free group can be
parametrized by a finite set of words of the form 


A further detailed study of the structure of exponential groups was carried out by A. Myasnikov and V. Remeslennikov (see [11] ). They proved that the group 
is a free extension of the centralizer C by s. From the work of Myasnikov and Remeslennikov, to construct



Advances in a different direction were given by Makanin and Razborov (see [24] -[26] ). Makanin proved that there exists an algorithm to determine, given a finite system of equations over a free group, whether the system possesses at least one solution. Razborov working with the Makanin algorithm determined an algorithm to effectively describe the solution sets of a finite system of equations over a free group.
Kharlampovich and Myasnikov further refined the Makanin-Razborov method. Their technique allows one to transform arbitrary finite systems of equations in free groups to some canonical forms and describe precisely the irreducible components of algebraic sets in free groups.
These canonical forms consist of finitely many quadratic equations in a triangular form. The following result is a corollary of the decidability of the Diophantine problem
Theorem 10 (Makanin) [24] [25]
1) The existential (and hence the universal) theory of a free group is decidable;
2) The positive theory of a free group is decidable.
The final ingredient that was needed for the proof was the development of an algebraic geometry over groups. In analogy with the classical theory of equations over number fields, algebraic geometry over groups was developed by Baumslag, Myasnikov and Remeslennikov [27] [28] . The theory of algebraic geometry over groups translated the basic notions of the classical algebraic geometry: algebraic sets, the Zariski topology, Noetherian domains, irreducible varieties, radicals and coordinate groups to the setting of equations over groups.
This provided the necessary machinery to transcribe important geometric ideas into pure group theory. The proof of the Tarski Conjectures depends on the algebraic geometry of free groups. In particular it depends on the description of a fully residually free group as the coordinate group of an irreducible algebraic variety. We review some of the basic definitions from the algebraic geometry over groups. These mirror for the most part the standard definitions in classicial algebraic geometry.
Let G be a group generated by a finite set







can be written as a product of some elements from the basis 
elements from





A solution of the system 





such that





versa. By 


of the group



is called the radical of S, denoted by
is the coordinate group of the algebraic set

described as a G-homomorphism
To study the coordinate groups of equations in a given fixed group G it is convenient to consider the category of G-groups, that is groups which contain the group G as a distinguished subgroup. If H and K are
G-groups then a homomorphism 


category of G-groups morphisms are G-homomorphisms; subgroups are G-subgroups, etc. For most of our applications we consider the group G to be a CSA-group.
By 



A Zariski topology is defined on 

What did not translate immediately was the Noetherian property which is crucial in classicial algebraic geomerty. For the group based algebraic geometry, what had to be introduced was equationally Noetherian groups which is the group theoretic counterpart of the Noetherian condition. The Noetherian condition in rings is defined in terms of the ascending chain condition (see [29] ) and implies that every ideal is finitely generated. What is important about this condition in algebraic geometry is the Hilbert Basis theorem that asserts that every
algebraic set is finitely based. That is if S be a set of polynomials in 

some finite set of polynomials. This is what is recast in terms of group theory. First a G-group H is a group whcih has a distinguished subgroup isomorophic to G. If S is a set of equations over a group G then 
Definition 1 A G-group H is said to be G-equationally Noetherian if for every 
subset S of 
The first major examples of equationally Noetherian groups are linear groups over commutative Noetherian rings. This was proved originally by Bryant [30] in the one variable case and then extended by Guba [31] to the case of free groups. The general result is the following.
Theorem 11 Let H be a linear group over a commutative, Noetherian ring with unity and in particular a field. Then H is equationally Noetherian.
In particular, it follows that a finitely generated non-abelian free group is equationally noetherian.
Extremely important in the application of the algebraic geometry of groups to the proof of the Tarski problems is the description of the coordinate groups of systems of equations. Radicals of a system of equations and coordinate group are defined as in classical algebraic geometry. Examining the relationship between the coordinate groups and groups embeddable by a sequence of extensions of centralizers in the free exponential group
In addition to the Tarski problems themselves, the quest for a solution has inspired many other results in group theory. This is especially true concerning the theory of solutions of equations within groups. In 1959, Vaught asked the question whether the sentence
holds in all free groups. Lyndon [32] then proved that for each solution of 





The focus of study eventually turned to strictly quadratic equations over free groups, that is equations in which every variable x occurs exactly twice as either x or
Makanin in 1982 [24] proved that if a given equation over a free group F has a solution in F then this equation has a solution of bounded length and this bound can be effectively computed from the equation itself. Makanin’s work allowed Razborov [26] to describe the solution set of a system of equations over F. Makanin further extended his results [25] , proving that that the universal theory of a non-abelian free group F is algorithmically decidable.
5. Strategy for the Proof
All these components had to be combined and integrated to provide the final proofs. Here we outline the strategy that was followed. Recall that Vaught proved Tarski Conjecture 2 for all free groups of infinite rank and hence reduced the problem to non-abelian free groups of finite rank. Vaught’s main result was that if the infinite rank free group 





all free groups of finite rank have the same 

equivalently
The main technique Vaught used in proving the Tarksi conjecture for infinite rank and Sacerdote used for the 
Tarski-Vaught Test If H is a subgroup of G then H is an elementary subgroup of G if and only if for any
formula 





Roughly the Tarski-Vaught Test says that a subgroup H of G is an elementary subgroup if and only if H is algebraically closed in G. In analogy with commutative algebra if we consider first order sentences with variables as our equations then any equation with constants from H which has a solution in G already has a solution within H.
If we wish to apply the Tarksi-Vaught Test to the case of a free factor in a free group of finite rank we must then understand the nature of solving equations in free groups and over free groups. The work of Makanin and Razborov became crucial. Their work provided first a method to determine if an equation over a free group was solvable and hence provided a technique for Kharlampovich and Myasnikov to show that the elementary theory of non-abelian free groups was decidable.
Here is where, however, it was the introduction of algebraic geometry over free groups that led to the necessary understanding of groups that have the same elementary theory as a non-abelian free group of finite rank.
The proofs of Kharlampovich-Myasnikov and Sela show that a general system of equations, with a few special cases that must be handled separately, can be shown to be equivalent to what is called a quasi- trianglular system of quadratic equations.
The coordinate groups of such systems are called QT-groups and are limit groups. A special subclass of them, called special NTQ-groups, are precisely the groups that can be shown to have the same elementary theory as the non-abelian free groups.
The structure of the algebraic variety of a system of equations can be broken down by the Makanin-Razborov method and is tied to the group theoretic breakdown of the coordinate groups.
Since the coordinate groups are limit groups this breakdown is well-understood as the JSJ decomposition of limit groups. The JSJ decompositon of a finitely generated group was developed originally by Rips and Sela [39] . It is graph of groups decomposition with abelian edge groups that encodes all other amalgam decompositions of a group.
It is the JSJ decomposition of the coordinbate groups combined with a type of implicit function theorem that provides for a quantifier elimination process that permits an induction starting with Sacerdote’s 
After all these massive preliminaries the proof itself is then an induction on the number of quantifiers, based on a quantifer elimination process. In the Kharlampovich-Myasnikov approach the quantifier elimination is handled by an implicit function theorem for quadratic systems.
We now describe in a bit more detail how to use the Tarski-Vaught Test to prove Tarski Conjecture 2.
Let 





appropriate for group theory and for each 


non-trivial elements of 
Without assuming the Tarski Conjectures for each integer 
be the set of those sentences of 




universal-existential sentences of
To this end let 




Boolean combinations of


obtained from 







embeddings 
The quantifier elimination is handled by an implicit function theorem. Basically consider a universal-
existential sentence of

We wish to show that for 


direction is relatively simple. Suppose that (1) holds in
the sentence
is an existential sentence of 



subset 



Since 

must hold in


The other way, that (1) holding in 


From the implicit function theorem it is the case that whenever (1) holds in 


also holds in
is a universal sentence of


follows that 


Therefore if (1) holds in 
holds in 

The key idea is that systems of equations can be reduced to certain quadratic systems and further the coordinate groups of such systems are limit groups. Hence limit groups are fundamental. We next summarize all the important properties of fully residually free groups including their relation to the coordinate groups of algebraic varieties.
Theorem 12 Let G be a fully residually free group. Then G satisfies the following properties:
1) G is torsion-free and each subgroup is also fully resiudally free;
2) G is CSA and hence CT. Further if G is finitley generated each abelian subgroup of G is finitely generated and contained in a unique maximal abelian subgroup;
3) If G is finitely generated then G is finitely presented and has only finitely many conjugacy classes of maximal abelian subgroups;
4) G is linear and has a solvable word problem;
5) Every 2-generator subgroup of G is either free or abelian;
6) If 
The next result summarizes the important equivalences for finitely generated fully residually free groups. These characterize this class of groups in several different ways and then play a crucial role in the proof of the Tarski problems. Number (9) in the theorem is especially important since it ties the class of limit groups to solutions of equations over free groups. We note that fully residually free groups in general need not be finitely generated. For example an infinitely generated free group is certainly fully residually free. However for our applications and for many of the important properties finite generation is crucial.
Theorem 13 Let G be a finitely generated group. Then the following are equivalent:
1) G is fully residually free;
2) G is universally free if G is non-abelian;
3) G is a limit group;
4) G is a constructible limit group;
5) G is a limit of free groups in the Gromov-Hausdorf Topology;
7) G embeds into a non-standard free group, that is an ultrapower of a free group;
8) G embeds into the free Lyndon completion
9) G is the coordinate group of an irreducible variety over a free group.
We note that this theorem is a general result and can be considered as without constants or coefficients from any particular free group. Each statement has a correspsonding result if we allow coefficients. If F is a particular non-abelian free group then for example in (1) we can say that a finitely generated F-group G is F-discri- minated by F is equivalent to G being universally equivalent to F in the language 
The applications to equations over free groups and hence the solution to the Tarski problems especially uses (8) and (9) in the theorem and we look at these a bit more deeply. Kharlampovich and Myasnikov prove the following result that they call the embedding theorem. This result combined with the fact that the finitely generated subgroups of 
Theorem 14 (The Embedding Theorem) Given an irreducible system of equations 


Corollary 1 The coordinate groups of irreducible algebraic varieties over a free group F are precisely the finitely generated fully residually free groups.
The finitely generated subgroups of 
6. Quasi-triangular systems
The big breakthrough in doing applications of the algebraic geometry and particularly in the solution of the Tarski problem came with the discovery that to study the solution sets and hence the varieties of general equations over free groups it was only necessary to study quadratic equations. That is it was proved that not only are the fully residually free groups the coordinate groups of irreducible algebraic varieties but were embedded into the coordinate groups of special systems called NTQ-systems of quadratic equations. The solutions of quadratic equations over free groups were already extensively studied. Further implicit function theorems were developed for such NTQ-systems. Here we introduce the necessary material about quadratic equations and quadratic systems.
Definition 2 An equation 


A quadratic equation 
We now write X instead of 



We extend this to G-groups.
Let

Definition 3 A set 




A system 
Quadratic equations can be placed into several standard forms.
Definition 4 A standard quadratic equation over the group G is an equation of one of the following forms (below 




Lemma 1 Let S be a strictly quadratic word over G. Then there is a G-automorphism 

The proof of this is in [36] .
Definition 5 A standard quadratic equation 
the type

not an equation of the type


In what follows we usually write just 

Theorem 15 (Implicit function theorem) Let 
non-abelian free group F and let 

any solution 


tuple of words


The implicit function theorem hence allows for a type of quantifier elimination.
What is next of importance are special types of systems of quadratic equations. First we define quasi- triangular systems.
Definition 6 Let 

coefficients from a free group F of the following form
is said to be triangular quasi-quadratic if for every i the equation
is quadratic in the variables from
Denote by 





The coordinate group of an NTQ-system is called an NTQ-group. In Sela’s terminology this is called an 



Kharlampovich and Myasnikov [1] use these ideas of algebraic geometry to prove that every finitely generated fully residually free group embeds into Lyndon’s group
Theorem 16 For every finite system 

such that for every 


and all sets 

the closure of 
Theorem 17 For a system 

for a non-degenerate triangular quasi-quadratic system
From the previous two theorems it follows that to consider the coordinate group of a general equation over a free group it can be reduced to looking at the coordinate group of an NTQ-system.
The final necessary component of the proof of the Tarski problems is the elimination process, abbreviated EP by Kharlampovich and Myasnikov. This is the most technical and difficult portion of the program and is based on initial work of Makanin and then improved upon by Razborov.
In general a quantifier elimination is a concept of simplification used in mathematical logic and model theory. First order formulas with fewer quantifiers are considered simpler with quantifier-free formulas as the simplest. A theory has quantifier elimination if for every formula in the theory there is another formula with fewer quantifiers logically equivalent to it relative to the theory.
Quantifier elimination permits an induction on the number of quantifiers. A first order theory L has quantifier elimination if and only if for any two models B and C of the theory with a common substructure A, B and C are elementarily equivalent in the language of L augmented with constants from A. To prove the elementary equivalence of B and C under quantifier elimination it suffices to prove the equivalence of the existential theory.
The proofs of the Tarksi theorems by Kharlampovich and Myasnikov use an elimination process originally introduced by Makanin. This elimination process, that is abbreviated EP, is a symbolic rewriting process that transforms formal systems of equations in groups. Makanin in 1982 introduced the initial version of the EP. His method provides a decision algorithm to verify consistency of a given system of equations, that is he handles the decidability of the Diophantine problem over free groups. To accomplish this, Makanin estimates the length of the minimal solution (if it exists). As part of this EP, Makanin introduced the fundamental notions of generalized equations and elementary and entire transformations. In 1987, Razborov [26] extended the EP much further. Razborov?s version of the EP produces all solutions of a given system in a free group F. He used special groups of automorphisms, and fundamental sequences to encode solutions.
In 1996 Kharlampovich and Myasnikov, building on the above, found an effective description of solutions of equations over free and fully residually free groups in terms of NTQ systems . In particular they represented a solution set of a system of equations canonically as a union of solutions of a finite family of NTQ groups.
Theorem 18 (see [5] ) One can effectively construct the EP that starts with an arbitrary system 
such that
for some word mappings
The word mapping 








The elimination process in this case can be viewed as a non-commutative analog of the classical elimination process in algebraic geometry. Hence, going from the bottom to the top, every solution of the subsystem 

The crux of the elimination process as applied to systems of equations over a free group F is the following chain of ideas. The precise details can be found in [5] .
Given a system 

such that:
1) Given a solution of 

in the free semigroup with basis
2) Given a solution of some 



3) Given a generalized equation 





4) The elimination process is a sequence of elementary transformations, applied according to some precise rules to an initial pair
5) The EP is a branching process such that on each step one of the finite number of elementary transfor- mations is applied according to some precise set of rules to form the sequence above;
6) From a group theoretic point of view the elimination process provides information about the coordinate groups of the systems involved. This allows the transformation of the pure combinatorial and algorithmic results obtained in the elimination process into statements about the coordinate groups.
7. The Proof Itself
In [5] in the Kharlampovich-Myasnikov proof, these various ingredients, the reduction to NTQ systems, the description of the breakup of the coordinate groups of equations in terms of the JSJ decomposition of the groups and the corresponding breakup of the algebraic varieties and finally the implicit funciton theorem and quantifier elimination given by the elimination process, was put together to give the final proof that if a free group 

As pointed out, the basic strategy is an induction on the number of quantifiers. The starting off point for the induction is Sacerdote’s theorem which says that if 



Recall that Merzlyakov proved that all non-abelian free groups satisfy exactly the positive sentences. Sacerdote, in his proof for the 


Thus Sacerdote’s theorem on 
where U and V are non-trivial elements in the free grup


In order to arrive at this reduction, the following ideas, that we have introduced in the previous sections, must be interwoven.
1) The solution set of a systems of equations 


2) Finitely generated fully residually free groups can be embedded into the coordinate groups of NTQ- systems. This allows us in trying to solve our general system to concentrate on NTQ-systems. As we have seen these systems are constructed inductively from quadratic equations and we can then apply the techniques developed for quadratic equations to the study of these systems;
3) The implicit function theorem for algebraic varieties corresponding to regular quadratic and NTQ-systems over free groups. As a by-product of placing these ideas together in the proof it will follow that the coordinate groups or special NTQ-systems turn out to form the class of finitely generated elementary free groups, that is the class of finitely generated groups elementarily equivalent to a non-abelian free group. We note that any non- standard free group, that is a proper ultrapower 
4) The variation and extension of the Makanin-Razborov process for solving equations over free groups. This extension provides a description of the solution set of a system of equations in a free group as a diagram of homomorphisms tied together with a decomposition of the coordinate group. This leads to what are called generalized equations and an elimination process.
Now consider the general sentence above, and we assume that there are more than two alternations of quantifiers so that it is not a 
If this sentence is positive then it is true or false in every non-abelian free group independent of rank by Merzljakov’s result. If not consider the algebraic variety of this equation and the corresponding system given by the irreducible algebraic components. Call this resulting system 

NTQ-systems we can look at the equivalent NTQ-system. Now using the extended Makanin-Razborov elimination process combined with the implicit function theorem we can reduce the NTQ-system to a system with a fewer number of quantifiers. The elimination process is a branching process and hence grows in size. A difficult portion of the analysis is to show that this process is finite, that is, it will terminate in a finite number of steps (see [5] ).
Ultimately we get that our original system is equivalent to a system that can be written as a boolean combination of sentences with less alternations of quantifiers. Further this reduction does not depend on the particular coordinate group 
This argument proves the Tarski Conjecture in the strong second form and hence also proves the first Tarski Conjecture. The argument also proves the following three results. The first was originally formulated and proved by Sela [9] .
Theorem 19 Every formula in the language of a free group is equivalent to a boolean combination of 
Theorem 20 A coordinate group of a special regular NTQ-system has the same elementary theory as a non-abelian free group.
In [4] it was proved that any finitely generated group which is 
Theorem 21 A finitely generated group G is an elementary free group if and only G is isomorphic to the coordinate group of a regular NTQ-system. We call such groups NTQ-groups.
We note that Sela of course comes up with the same characterization. In his language the NTQ-groups are called w-residually free towers. Therefore from Sela the finitely generated elementary free groups are the hyperbolic-w-residually free towers.
In the final section we will look in more detail at elementary free groups.
Above we have outlined the proof of the first two Tarski Conjectures in the strongest possible form. That is,
the free group 

for every 

Recall that a theory of a group G, Th(G), is decidable if there exists a recursive algorithm which, given a sentence 





exists a recursive algorithm which, given a sentence 



The starting off point for the proof of the decidability of the theory of non-abelian free groups was the work of Makanin. Makanin [24] proved the algorithmic decidability of the Diophantine problem over free groups. He combined this with Merzjlakov’s proof that all non-abelian free groups share the same positive theory to prove the algorithmic decidability of the positive theory of non-abelian free groups. He further proved the algorithmic decidability of the universal theory. This then implies, although it was not relevant at the time, the algorithmic decidability of the universal theory of limit groups. Makanin developed a powerful machinery, which is now called the Makanin elimination process, to deal with equations over free groups. Razborov extended Makanin’s method and described the solution set of an arbitary system of equations over a free group in terms of Makanin-Razborov diagrams. As we have seen the Makanin-Razborov process for describing the solution sets of arbitrary systems of equations can be reduced to examining the solution sets of NTQ systems and hence the solution of quadratic equations.
Kharlampovich and Myasnikov combined the same type of induction process outlined in section 6, together with Makanin’s technique to obtain the decidability of the elementary theory of a non-abelian free group.
What is done, although as in the previous section the details are complicated, is to show the decidability of the 
effectiveness have been simplified by using the description of limit groups in terms of infinite words in
Further some of the reductions are handled by an extended implicit function theorem.
8. Elementary Free Groups
As a by-product of the proof of the Tarski theorems it is possible to give complete characterizations of those finitely generated groups that have exactly the same first order theory as the non-abelian free groups. Such groups are called elementary free groups (or elementarily free groups) and extend beyond the class of purely non- abelian free groups. In the Kharlampovich-Myasnikov approach these are the special NTQ-groups and in the Sela approach the hyperbolic 




Magnus proved the following theorem about the normal closures of elements in non-abelian free groups:
Theorem 22 (Magnus) Let F be a non-abelian free group and

that R is conjugate to either S or

Howie [40] and independently Bogopolski [41] and Bogopolski and Sviridov [42] gave a proof of this for surface groups. Howie’s proof was for orientable surface groups while Bogopolski and Sviridov also handled the non-orientable case. Their proofs were non-trivial and Howie’s proof used the topological properties of surface groups. Howie further developed, as part of his proof of Magnus’ theorem for surface groups, a theory of one- relator surface groups. These are surface groups modulo a single additional relator. Bogopolski and Sviridov proved in addition that Magnus’s Theorem held in even a wider class of groups. In [43] (see also [44] and [45] ) Magnus’ result is actually a first-order theorem on non-abelian free groups and hence from the theorems con- cerning the solution of the Tarski problems it holds automatically in all elementary free groups. In particular, Magnus’ theorem will hold in surface groups, both orientable and non-orientable of appropriate genus. If G is a group and

Theorem 23 Let G be an elementary free group and


As corollaries we recover the results of Howie [40] , Bogopolski [41] and Bogopolski-Sviridov [42] which extend Magnus’s Theorem to surface groups
Corollary 2 ([40] [41] ) Let 






Corollary 3 ([42] ) Let 







In [43] a collection of results about elementary free groups and surface groups was presented, their proofs being consequences of the Tarski theorem. We mention one such result that is not obvious in a surface group. The following theorem can be easily proved in free groups.
Theorem 24 Let F be a free group and n, k non-zero integers. For all 

either 

The first part of the result that either 

sentences, one for each 
Therefore this part of the result must hold in any elementary free group. Further if the elementary free group is finitely generated the second part must also hold.
Corollary 4 Let G be an elementary free group. If 



Since surface groups are finitely generated we have the following.
Corollary 5 Let G be either an orientable surface group of genus 
group of genus



both x and y are powers of a single element
In another direction in [44] properties of all elementary free groups, which may not be first order were explored. A finitely generated elementary free group G must be a limit group and many of its properties follow from from the structure theory of limit groups. Hence such a group must be CSA and any 2-generator subgroup is either free or abelian.
In [44] it was proved that a finitely generated elementary free group has cyclic centralizers. This is not a first order statement, however from this we get that if two elements commute in a finitely generated elementary free group then they are both powers of a single element. This is not true in a general elementary free group. An example where it does not hold in the infinitely generated case is given in [44] . From the cyclic centralizer property we can obtain that a finitely generated elementary free group must be hyperbolic, stably hyperbolic and a Turner group, that is the test elements, if there are any, in any finitely generated elementary free group are precisely those elements that do not lie in any proper retract. It was also proved in [44] that any finitely generated elementary free group is conjugacy separable and hence has a solvable conjugacy problem. In [46] (see also [47] ) is was shown the automorphism group of a finitely generated elementary free group is tame.
The next theorem summarizes many of these results. The proofs can be found [44] .
Theorem 25 Let 
1) (Magnus’s Theorem) if 




2) G has cyclic centralizers of non-trivial elements. It follows that if 

3) if 




conjugate to a power of 









4) G is conjugacy separable;
5) G is hyperbolic and stably hyperbolic;
6) G is a Turner group, that is the test elements in G are precisely those elements that do not fall in a proper retract;
7) if G is freely indecomposable then the automorphism group of G is tame;
8) G has a faithful representation in
For more information on elementary theory in general, see [11] -[13] . For further information on the structure of limit groups and hyperbolic groups see [21] [48] -[51] [52] [53] .
References
- Kharlamapovich, O. and Myasnikov, A. (1998) Irreducible Affine Varieties over a Free Group: I. Irreducibility of Quadratic Equations and Nullstellensatz. Journal of Algebra, 200, 472-516. http://dx.doi.org/10.1006/jabr.1997.7183
- Kharlamapovich, O. and Myasnikov, A. (1998) Irreducible Affine Varieties over a Free Group: II. Systems in Triangular Quasi-Quadratic Form and Description of Residually Free Groups. Journal of Algebra, 200, 517-570.
- Kharlamapovich, O. and Myasnikov, A. (2005) Implicit Function Theorem over Free Groups. Journal of Algebra, 290, 1-203. http://dx.doi.org/10.1016/j.jalgebra.2005.04.001
- Kharlamapovich, O. and Myasnikov, A. (2005) Effective JSJ Decompositions. Contemporary Mathematics, 378, 87- 212. http://dx.doi.org/10.1090/conm/378/07012
- Kharlamapovich, O. and Myasnikov, A. (2006) Elementary Theory of Free Non-Abelian Groups. Journal of Algebra, 302, 451-552. http://dx.doi.org/10.1016/j.jalgebra.2006.03.033
- Sela, Z. (2001) Diophantine Geometry over Groups I: Makanin-Razborov Diagrams. Publications Mathématiques de l’Institut des Hautes Études Scientifiques, 93, 31-106. http://dx.doi.org/10.1007/s10240-001-8188-y
- Sela, Z. (2003) Diophantine Geometry over Groups II: Completions, Closures and Formal Solutions. Israel Journal of Mathematics, 134, 173-254. http://dx.doi.org/10.1007/BF02787407
- Sela, Z. (2005) Diophantine Geometry over Groups III: Rigid and Solid Solutions. Israel Journal of Mathematics, 147, 1-73. http://dx.doi.org/10.1007/BF02785359
- Sela, Z. (2004) Diophantine Geometry over Groups IV: An Iterative Procedure for Validation of a Sentence. Israel Journal of Mathematics, 143, 1-130. http://dx.doi.org/10.1007/BF02803494
- Sela, Z. (2005) Diophantine Geometry over Groups V: Quantifier Elimination. Israel Journal of Mathematics, 150, 1-197.
- Fine, B., Gaglione, A., Myasnikov, A., Rosenberger, G. and Spellman, D. (2014) The Elementary Theory of Groups. Walter de Gruyter, Berlin. http://dx.doi.org/10.1515/9783110342031
- Bell, J.L. and Slomson, A.B. (1971) Models and Ultraproducts: An Introduction. 2nd Revised Printing, North-Holland, Amsterdam.
- Chang, C.C. and Keisler, H.J. (1977) Model Theory. 2nd Edition, North-Holland, Amsterdam.
- Magnus, W., Karrass, A. and Solitar, D. (1966) Combinatorial Group Theory: Presentations of Groups in Terms of Generators and Relations. Interscience Publishers, John Wiley and Sons, Inc., New York, London, Sydney.
- Lyndon, R.C. and Schupp, P.E. (1977) Combinatorial Group Theory. Springer-Verlag, Berlin. http://dx.doi.org/10.1007/978-3-642-61896-3
- Merzlyakov, Y.I. (1966) Positive Formulas on Free Groups. Algebra i Logika, 5, 25-42.
- Sacerdote, G.S. (1972) Elementary Properties of Free Groups. Transactions of the American Mathematical Society, 178, 127-138. http://dx.doi.org/10.1090/S0002-9947-1973-0320146-4
- Baumslag, B. (1967) Residually Free Groups. Proceedings of the London Mathematical Society, 17, 635-645.
- Gaglione, A. and Spellman, D. (1993) Even More Model Theory of Free Groups. In: Corson, J., Dixon, M., Evans, M. and Rohl, F., Eds., Infinite Groups and Group Rings, World Scientific Press, Singapore City, 37-40. http://dx.doi.org/10.1142/9789814503723_0004
- Remeslennikov, V.N. (1989) ∃-Free Groups. Siberian Mathematical Journal, 30, 998-1001. http://dx.doi.org/10.1007/BF00970922
- Chiswell, I. (1976) Abstract Length Functions in Groups. Mathematical Proceedings of the Cambridge Philosophical Society, 80, 451-463. http://dx.doi.org/10.1017/S0305004100053093
- Ciobanu, L., Fine, B. and Rosenberger, G. (2015) Classes of Groups Generalizing a Theorem of Benjamin Baumslag. To Appear-Comm. in Alg.
- Lyndon, R.C. (1960) Groups with Parametric Exponents. Transactions of the American Mathematical Society, 96, 518- 533. http://dx.doi.org/10.1090/S0002-9947-1960-0151502-6
- Makanin, G.S. (1982) Equations in a Free Group (Russian). Izv. Akad. Nauk SSSR, Ser. Mat., 46, 1199-1273. Transl. in Math. USSR Izv., V. 21, 1983, MR 84m:20040.
- Makanin, G.S. (1985) Decidability of the Universal and Positive Theories of a Free Group. Mathematics of the USSR-Izvestiya, 25, 75-88. http://dx.doi.org/10.1070/IM1985v025n01ABEH001269
- Razborov, A.A. (1984) On Systems of Equations in Free Groups. Izv.Akad. Nauk SSSR, 48, 779-832. Englisg transl: Math, USSR Izv., 25, 115-162.
- Baumslag, G., Myasnikov, A. and Remeslennikov, V. (2002) Discriminating Completions of Hyperbolic Groups. Geometriae Dedicata, 92, 115-143. http://dx.doi.org/10.1023/A:1019687202544
- Baumslag, G., Myasnikov, A. and Remeslennikov, V. (1999) Algebraic Geometry over Groups I. Algebraic Sets and Ideal Theory. Journal of Algebra, 219, 16-79. http://dx.doi.org/10.1006/jabr.1999.7881
- Carstensen, C., Fine, B. and Rosenberger, G. (2012) Abstract Algebra. De Gruyter, Berlin.
- Bryant, R. (1977) The Verbal Topology of a Group. Journal of Algebra, 48, 340-346. http://dx.doi.org/10.1016/0021-8693(77)90312-X
- Guba, V. (1986) Equivalence of Infinite Systems of Equations in Free Groups and Semigroups to Finite Subsystems. Mat. Zametki, 40, 321-324.
- Lyndon, R.C. (1959) The Equation
in Free Groups. Michigan Mathematical Journal, 6, 155-164.>http://html.scirp.org/file/7-5300834x515.png" class="200" /> in Free Groups. Michigan Mathematical Journal, 6, 155-164.
- Lorenc, A.A. (1963) The Solution of Systems of Equations in One Unknown in Free Groups. Dokl. Akad. Nauk SSSR, 148, 262-266.
- Appel, K.I. (1968) One-Variable Equations in Free Groups. Proceedings of the American Mathematical Society, 19, 912-918. http://dx.doi.org/10.1090/S0002-9939-1968-0232826-3
- Csorgo, P., Fine, B. and Rosenberger, G. (2002) On Certain Equations in Free Groups. Acta Sci. Math., 68, 95-105.
- Comerford, L. and Edmonds, C. (1989) Solutions of Equations in Free Groups. Proceedings of Conference in Group Theory Singapore 1987, Springer-Verlag, Berlin, 347-355.
- Grigorchuk, R.I. and Kurchanov, P.F. (1992) On Quadratic Equations in Free Groups. Contemporary Mathematics, 131, 159-171. http://dx.doi.org/10.1090/conm/131.1/1175769
- Grigorchuk, R. and Kurchanov, P. (1990) Some Questions of Group Theory Related to Geometry. In Itogi Nauki i Techniki, Sovremennye problemy matematiki. Fundamental’nye napravlenia, VINITI, 58. Encyclopedia of math. sciences, English Translation in 1993.
- Rips, E. and Sela, Z. (1997) Cyclic Splittings of Finitely Presented Groups and the Canonical JSJ Decomposition. Annals of Mathematics, 146, 53-109. http://dx.doi.org/10.2307/2951832
- Howie, J. (2004) Some Results on One-Relator Surface Groups. Boletín de la Sociedad Matemática Mexicana, 10, 255-262.
- Bogopolski, O. (2005) A Surface Groups Analogue of a Theorem of Magnus. Cont. Math, 352, 55-89.
- Bogopolski, O. and Sviridov, K. (2008) A Magnus Theorem for Some One-Relator Groups. The Zieschang Gedenkschrift, 14, 63-73.
- Fine, B., Gaglione, A., Rosenberger, G. and Spellman, D. (2013) Something for Nothing: Some Consequences of the Solution of the Tarski Problems. To Appear Proc. of Groups St Andrews.
- Fine, B., Gaglione, A., Rosenberger, G. and Spellman, D. (2015) On Elementary Free Groups. To Appear Cont. Math.
- Gaglione, A., Lipschutz, S. and Spellman, D. (2009) Almost Locally Free Groups and a Theorem of Magnus. Journal of Groups, Complexity, Cryptology, 1, 181-198.
- Bumagin, I., Kharlampovich, O. and Myasnikov, A. (2007) The Isomorphism Problem for Finitely Generated Fully Residually Free Groups. Journal of Pure and Applied Algebra, 208, 961-977. http://dx.doi.org/10.1016/j.jpaa.2006.03.025
- Fine, B., Kharlampovich, O., Myasnikov, A., Remeslennikov, V. and Rosenberger, G. (2012) Tame Automorphisms of Elementary Free Groups. Communications in Algebra, 1, 1-15.
- Fine, B., Gaglione, A., Myasnikov, A., Rosenberger, G. and Spellman, D. (1998) A Classification of Fully Residually Free Groups of Rank Three or Less. Journal of Algebra, 200, 571-605. http://dx.doi.org/10.1006/jabr.1997.7205
- Kharlamapovich, O. and Myasnikov, A. (1998) Hyperbolic Groups and Free Constructions. Transactions of the American Mathematical Society, 350, 571-613. http://dx.doi.org/10.1090/S0002-9947-98-01773-5
- Sela, Z. (1995) The Isomorphism Problem for Hyperbolic Groups I. Annals of Mathematics, 141, 217-283. http://dx.doi.org/10.2307/2118520
- Gildenhuys, D., Kharlampovich, O. and Myasnikov, A. (1995) CSA Groups and Separated Free Constructions. Bulletin of the Australian Mathematical Society, 52, 63-84. http://dx.doi.org/10.1017/S0004972700014453
- Fine, B. and Rosenberger, G. (2011) Faithful Representations of Hyperbolic Limit Groups. Groups Complexity Cryptology, 3, 349-355.
- Fine, B. and Rosenberger, G. (2013) Faithful Representations of Limit Groups II. Groups Complexity Cryptology, 5, 91-96. http://dx.doi.org/10.1515/gcc-2013-0005



































in Free Groups. Michigan Mathematical Journal, 6, 155-164.>http://html.scirp.org/file/7-5300834x515.png" class="200" /> in Free Groups. Michigan Mathematical Journal, 6, 155-164.