THE QUANTIFIER ELIMINATION OF DENSE BINARY ORDERS THEORY(I)
Lei Chen · Journal of Beijing Normal University · 2008
This paper is the first in a series to prove the quantifier elimination of dense binary orders theory.The axioms of this theory were given in the language L={≤,R},and found that the theory does not have the property of quantifier elimination in this language,but rather the dense binary orders theory has the property of quantifier elimination in the language L={≤,R,*}.This is proven in the present paper by relating the quantifier elimination of conjunctions of the formulas in the basic set,and by paying attention to conjunctions of same type formulas.