How to show a theory eliminates quantifiers?

Question

Definition(1). Let $\mathscr{L}$ be a first-order language. An $\mathscr{L}$-theory $T$ is said to have quantifier-elimination whenever if for all $\mathscr{L}$-formula $\phi(\bar{x})$ there exists a quantifier-free $\mathscr{L}$-formula $\psi_\phi(\bar{x})$ such that $$T\models \forall \bar{x}\left(\phi(\bar{x})\leftrightarrow\psi_\phi(\bar{x}) \right) $$

Definition(2). Let $\mathcal{C}$ be a class of $\mathscr{L}$-structures, for a first-order language $\mathscr{L}$. We say $\mathcal{C}$ eliminates quantifiers if for every $\mathscr{L}$-formula $\phi (\bar{x}) $ there is a quantifier-free formula $\psi_\phi(\bar{x})$ such that $\phi(\bar{x})$ is equivalent to $\psi_\phi(\bar{x})$ in every structure in $\mathcal{C}$.

Definition(3). Let $\mathscr{L}$ be a first-order language, and let $\mathcal{C}$ be a class of finite $\mathscr{L}$-structures. $\mathcal{C}$ is called a Fraisse class if it satisfies the heriditary property (HP), the joint embedding property (JEP), and the amalgamation property (AP).

By Fraisse Theorem, any Fraisse class has a generec model $\mathcal{M}_\mathcal{C}$ such that it is homogeneous and its theory is $\omega$-categorical (i.e. up to isomorphism there is exactly one model of size $\aleph_0$.)

Question(1). Let $\mathcal{C}$ be a Fraisse calss with generic model $\mathcal{M}$ and generic theory $T$ (i.e. $T=Th(\mathcal{M})$). Is it always true that $T$ eliminates quantifiers? If no, what is the counterexample? and under what conditions we can conclude $T$ has quantifier elimination?

Question(2). In general, how can we prove a class of $\mathscr{L}$-structures has quantifier elimination? There are some techniques in Marker's book, but they usually are used to show a theory has quantifier-elimination not a class. In Hodges's book there is a theorm which says who a class eliminates quantifiers but the theorem is clearly equivalent to the definition and it does not give us any tool.

Question(3). Is it true that there is not general ways to show a theory has quantifier elimination? I mean for each theory we need to find a specific way related to our theory? (If this is correct, that's so bad!)

Any refrences whould be helpful.

Answer 1

(1) Let me first correct something. You wrote:

By Fraisse Theorem, any Fraisse class has a generec model $\mathcal{M}_{\mathcal{C}}$ such that it is homogeneous and its theory is $\omega$-categorical.

This is not quite true - your definition of Fraïssé class is too general to prove this theorem. Suppose $\mathcal{C}$ is a class of finite $\mathcal{L}$-structures with HP, JEP, and AP. Then:

• In order for a countable Fraïssé limit to exist, you also need to assume that $\mathcal{C}$ is countable up to isomorphism. So I would also include this condition in the definition of Fraïssé class. (This condition is automatically satisfied if the language $\mathcal{L}$ is finite.)

• Under the conditions above, it's true that $\mathcal{C}$ has a countable Fraïssé limit $\mathcal{M}_{\mathcal{C}}$, which is unique up to isomorphism. But you can't prove that its complete theory $\text{Th}(\mathcal{M}_{\mathcal{C}})$ is $\omega$-categorical without additionally assuming one more thing abut $\mathcal{C}$: for every natural number $n$, there are only finitely many structures in $\mathcal{C}$ up to isomorphism that admit a generating set of size $n$. (This condition is automatically satisfied if the language $\mathcal{L}$ is finite and relational - no function or constant symbols. So Fraïssé's theorem is often stated in the special case of finite relational languages. It is also satisfied if $\mathcal{L}$ is finite and $\mathcal{C}$ is uniformly locally finite, meaning that for any natural number $n$, there is a bound $f(n)$ such that any structure in $\mathcal{C}$ which admits a generating set of size $n$ has size at most $f(n)$. This applies, for example, to the class of vector spaces over a fixed finite field $\mathbb{F}_q$: a structure generated by $n$ elements has size at most $f(n) = q^n$.)

Now whenever $\text{Th}(\mathcal{M}_{\mathcal{C}})$ exists and is $\omega$-categorical, this theory also eliminates quantifiers (I gave a proof in my answer here). For example, in the book by Hodges, he proves that if $\mathcal{C}$ is a uniformly locally finite Fraïssé class in a finite language, then $\text{Th}(\mathcal{M}_{\mathcal{C}})$ is $\omega$-categorical and eliminates quantifiers.

On the other hand, there are Fraïssé classes with Fraïssé limits whose theories are not $\omega$-categorical and do not eliminate quantifiers. For examples in an infinite relational language and in a finite language with function symbols, see my answer here (the Fraïssé classes are the classes of finite substructures of the ultrahomogeneous structures described in my answer).

(2) Another possible misconception to correct: If $\mathcal{C}$ is a Fraïssé class, the statements "$\mathcal{C}$ has quantifier elimination" and "$\text{Th}(\mathcal{M}_\mathcal{C})$ has quantifier elimination" are totally different. It is extremely unusual for a class of finite structures to have quantifier elimination. So I don't really see the connection between questions (1) and (2). You probably should have asked them as separate questions.

If you're interested in a class $\mathcal{C}$ of $\mathcal{L}$-structures which is not the class of models of some first-order theory $T$, then proving quantifier elimination is not going to be easy! The main tool for understanding formulas up to equivalence is the compactness theorem, and for an arbitrary class $\mathcal{C}$, the compactness theorem doesn't apply. I think the best approach would be to try to use Ehrenfeucht-Fraïssé games.

(3) This question honestly mystifies me. Of course you'll have to use specific features of a theory to prove it has quantifier elimination!

There are many general tests for quantifier elimination, most of which are stated as equivalences ($T$ eliminates quantifiers if and only if ...), so if you're given a theory $T$ with quantifier elimination, you can in principle use any of these tests to verify it. Now of course for any given theory, some tests will be easier to apply to it than others. So you'll see many different approaches to proving quantifier elimination applied to different theories in the literature and in textbooks. But if anything, it's good to have lots of different approaches you can pick from!