quantifier free

Let $L$ be a first order language. A formula $\psi$ is quantifier free iff it contains no quantifiers.

Let $T$ be a complete $L$-theory. Let $S\subseteq L$. Then $S$ is an elimination set for $T$ iff for every $\psi(\bar{x})\in L$ there is some $\phi(\bar{x})\in S$ so that $T\vdash\forall\bar{x}(\psi(\bar{x}))\leftrightarrow\phi(\bar{x})$.

In particular, $T$ has quantifier elimination iff the set of quantifier free formulas is an elimination set for $T$. In other $T$ has quantifier elimination iff for every $\psi(\bar{x})\in L$ there is some quantifier free $\phi(\bar{x})\in L$ so that $T\vdash\forall\bar{x}(\psi(\bar{x}))\leftrightarrow\phi(\bar{x})$.

 Title quantifier free Canonical name QuantifierFree Date of creation 2013-03-22 13:27:49 Last modified on 2013-03-22 13:27:49 Owner mathcam (2727) Last modified by mathcam (2727) Numerical id 7 Author mathcam (2727) Entry type Definition Classification msc 03C10 Classification msc 03C07 Classification msc 03B10 Related topic Quantifier Related topic LogicalLanguage Defines quantifier free formula Defines quantifier elimination Defines elimination set