Quantifier elimination for infinite terms (Q1812980)

We consider the theory \({\mathcal T}_{IT}\) of infinite terms. The axioms for the theory \({\mathcal T}_{IT}\) are analogous to the Mal'cev's axioms for the theory \({\mathcal T}_{FT}\) of finite terms whose models are the locally free algebras. Recently M. J. Maher has proved that the theory \({\mathcal T}_{IT}\) in a finite non-singular signature plus the Domain Closure Axiom is complete. In this paper, a description of all the complete extensions of \({\mathcal T}_{IT}\) is given and hence an effective decision procedure for \({\mathcal T}_{IT}\) is obtained. The approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theory \({\mathcal T}_{IT}\) can be carried out in analogy with Mal'cev's analysis of \({\mathcal T}_{FT}\). The results follow from an effective quantifier elimination procedure for formulas with pointers.