quantifier freeQuantifierFree2003-02-12 08:52:192007-01-11 21:26:34Definitionquantifier free formulaquantifier eliminationelimination set% this is the default PlanetMath preamble. as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.
% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}
% there are many more packages, add them here as you need them
% define commands hereLet $L$ be a first order language.
A formula $\psi$ is {\em quantifier free} iff it contains no quantifiers.
\medskip
Let $T$ be a complete $L$-theory. Let $S \subseteq L$. Then $S$ is an {\em 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})$.
\medskip
In particular, $T$ has {\em quantifier elimination} iff the set of quantifier free formulas is an elimination set for $T$.
In other \PMlinkescapetext{words} $T$ has {\em 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})$.