|
|
|
|
quantifier free
|
(Definition)
|
|
|
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 words $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})$ .
|
"quantifier free" is owned by mathcam. [ full author list (2) | owner history (1) ]
|
|
(view preamble | get metadata)
Cross-references: complete, quantifiers, contains, iff, formula, first order language
There are 7 references to this entry.
This is version 4 of quantifier free, born on 2003-02-12, modified 2007-01-11.
Object id is 4031, canonical name is QuantifierFree.
Accessed 6931 times total.
Classification:
| AMS MSC: | 03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic) | | | 03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures) | | | 03C10 (Mathematical logic and foundations :: Model theory :: Quantifier elimination, model completeness and related topics) |
|
|
|
|
|
|
Pending Errata and Addenda
|
|
|
|
|
|
|
|
|
|
|
