  Of the three programmes described here, this is the oldest, since it grew out of Tarski’s description of the complete theory of the field of real numbers (which he proved by the method of quantifier elimination).  In the course of giving this description, Tarski had shown that every first-order formula φ(x) in the relevant language, possibly with parameters, is satisfied by exactly the same assignments as some boolean combination of formulas of the form x &lt; s or t &lt; x where s, t are constant terms naming parameters. Another way of saying this is that 