A. Tarski [4] has given a decision method for elementary algebra. In essence this comes to giving an algorithm for deciding whether a given finite set of polynomial inequalities has a solution. Below we offer another proof of this result of Tarski. The main point of our proof is accomplished upon showing how to decide whether a given polynomial f(x, y) in two variables, denned over the field R of rational numbers, has a zero in a real-closed field К containing R.1 This is done in §2, but for purposes of induction it is necessary to consider also the case that the coefficients of f(x, y) involve parameters; the remarks in §3 will be found sufficient for this point. In §1, the problem is reduced to a decision for equalities, but an induction (on the number of unknowns) could not possibly be carried out on equalities alone; we consider a simultaneous system consisting of one equality f(x, y) = 0 and one inequality F(x) ^ 0. Once the decision for this case is achieved, at least as in §3, the induction is immediate.
Entering into our considerations are the field R of rational numbers and an arbitrary real-closed field К: the argument proceeds uniformly for all K. Because of this, one gets for real-closed fields a principle analogous to the so-called "PrincipLe of Lefschetz." This principle asserts that results of a certain kind— the kind occurring, for example, in A. Weil's Foundations of Algebraic Geometry (see [6; pp. 242-245])—which are true for the field of eompLex numbers automatically hold also for an arbitrary algebraicaLly closed field of characteristic 0. The corresponding principle for real-closed fields, which we may call the "Principle of Tarski," says that any sentence of elementary algebra which holds in one real-closed fieLd also holds In every real-closed field. In particular it is true that any polynomial f(x\, • • ■ , xn) * K[xi, ■ • ■ , xn], К a real-closed fieLd, has on any /i-dimensional closed interval a maximum and a minimum. In §S(b) we illustrate the principle by showing that if an algebraic variety defined over a real-closed field carries any points with coordinates in K, then it also carries one such point which is nearest to the origin.
Our proof may have some bearing on the actual construction of a decision machine. Some remarks on this point are made in §S(e).
Thanks are due to Professor Tarski for valuable comments on the paper.
