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 (\overline{x})\in L$ there is some $\varphi (\overline{x})\in S$ so that $T⊢\forall \overline{x}(\psi (\overline{x}))\leftrightarrow \varphi (\overline{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 (\overline{x})\in L$ there is some quantifier free $\varphi (\overline{x})\in L$ so that $T⊢\forall \overline{x}(\psi (\overline{x}))\leftrightarrow \varphi (\overline{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