Recall the logical predicates that were formed in Section
3.1. They will be used again here, but now they are defined
with a little more flexibility. For any
,
an *atom* is an expression of the form
, in which
may be any relation in the set
. In Section 3.1, such expressions were used to
define logical predicates. Here, we assume that relations other than
can be used and that the vector of polynomial variables lies
in
.

A *quantifier-free formula*,
, is a logical
predicate composed of atoms and logical connectives, ``and,'' ``or,''
and ``not,'' which are denoted by , , and ,
respectively. Each atom itself is considered as a logical predicate
that yields TRUE if and only if the relation is satisfied when the
polynomial is evaluated at the point
.

(6.8) |

The precedence order of the connectives follows the laws of Boolean algebra.

Let a *quantifier* be either of the symbols, ,
which means ``for all,'' or , which means ``there exists.''
A *Tarski sentence* is a logical predicate that may
additionally involve quantifiers on some or all of the variables. In
general, a Tarski sentence takes the form

in which the are the

is TRUE because for any , some can always be chosen so that . In the general notation of (6.9), this example becomes , , and .

Swapping the order of the quantifiers yields the Tarski sentence

which is FALSE because for any , there is always an such that .

Now consider a Tarski sentence that has a free variable:

This yields a function TRUEFALSE, in which

(6.13) |

An equivalent quantifier-free formula can be defined as , which takes on the same truth values as the Tarski sentence in (6.12). This might make you wonder whether it is always possible to make a simplification that eliminates the quantifiers. This is called the

Steven M LaValle 2012-04-20