10
votes
Accepted
Elimination of quantifiers for $\exists x\ x^2=y$
A quantifier-free assertion about $y$ in the language of $\{0,1,+,\cdot\}$ is a Boolean combination of polynomial equations in $y$ with natural number coefficients. Since every such equation has ...
- 44.6k
10
votes
Why is quantifier elimination desirable for a given theory?
You're quite right that we can "shoehorn in" quantifier elimination to any theory we want, by adding new predicates for all old formulas (this is called Morleyization if I recall correctly). So ...
- 251k
10
votes
How to show that $\mathbb{R}$ in the language of rings does not admit quantifier elimination?
Your idea of using a formula defining $\leq$ is a good one, but it will be easier to work with a similar formula that has only one free variable; I suggest $\exists x\,(x^2=y)$. I also think it's ...
- 73.3k
8
votes
Accepted
Quantifier elimination for $\mathbb Z$ as a group?
The complete theory of the structure $(\mathbb{Z}; 0,+,-,(n|)_{n\in \mathbb{Z}})$ , which is a definitional expansion of $(\mathbb{Z};+)$, has quantifier elimination. Of course, it already suffices to ...
- 80.1k
7
votes
Accepted
uniformity in quantifier elimination
No, it is not. Every completion of the empty theory in the empty language has quantifier elimination, but the empty theory itself doesn't.
Why? Well, note that the only data missing from the empty ...
- 251k
7
votes
Counter-example of o-minimal structure but do not admit elimination of quantifiers
The classic example is $\mathbb{R}_{\text{exp}} = (\mathbb{R};<,+,-,\times,0,1,e^x)$. Wilkie showed that the complete theory of this structure is o-minimal and model complete, but does not admit ...
- 80.1k
6
votes
Accepted
How to show that $\mathbb{R}$ in the language of rings does not admit quantifier elimination?
I agree with Andreas Blass that the argument suggested in his answer is the most straightforward way to see that the theory of the real field does not have QE. But here's a way to see this using the ...
- 80.1k
5
votes
Quantifier elimination for $\mathbb Z$ as a group?
In his answer, Alex Kruckman points out the excellent reference: Eklof and Fischer, The elementary theory of abelian groups. Let me just spell out what can be gleaned from this. They recover Szmielew'...
4
votes
Can every theory $T$ be expanded to a theory with quantifier elimination in the same language?
Well, if $T$ is complete, then there's no nontrivial way to expand it, so any complete theory without quantifier elimination is a counterexample. Complete theories which have quantifier elimination ...
- 335k
4
votes
Can every theory $T$ be expanded to a theory with quantifier elimination in the same language?
No - there are theories $T$ with a formula $\varphi(x)$ such that for every quantifier-free $\psi(x)$, $T$ proves $$\exists x(\neg(\varphi(x)\iff\psi(x)).$$ For a natural example, PA does this: take $\...
- 251k
4
votes
Accepted
$\Sigma_{(\mathbb{N},<)}$ does not admit elimination of quantifiers
Your argument is correct. More directly, you can just observe that any quantifier-free formula is a Boolean combination of atomic formulas, and the only atomic formulas in one variable are $x<x$ ...
- 335k
4
votes
Accepted
Exercise 3.4.3 in David Marker's "Model Theory"
Let me explain what the question is asking, and then give a hint as to how to approach it.
The theories in question are the theories of the structures. A theory in a language $\Sigma$ is, as you say, ...
- 251k
4
votes
Accepted
Consider theory T = Th(M, ~, =). Show that T has quantifier elimination
Alternatively, you can just check it directly.
To prove quantifier elimination, it is enough to show that every formula of the form $\exists x \varphi(x,\bar y)$, where $\varphi$ is quantifier-free, ...
- 36.2k
4
votes
Accepted
Primitive recursive predicates for exponentiation and multiplication
Your claims $(1), (2)$, and $(3)$ are each correct. Claim $(4)$, however, is incorrect; indeed, if multiplication were definable over $(\mathbb{N};\max,+)$ then the theory $Th(\mathbb{N};\max,+)$ ...
- 251k
4
votes
Accepted
Theory in $(\mathbb{N};0,S,<)$ is complete?
You don't have to use Theorem 31G (which states theory of natural numbers with successor admits elimination of quantifiers), but you have to develop an argument similar to the one explained after (the ...
- 17.4k
4
votes
Accepted
Quantifier elimination for $\text{ACF0}$ over signature $(+,·)$.
Yes, it does. To prove this, it suffices to check that every atomic quantifier-free formula in the signature $(+,\cdot,-,0,1)$ is equivalent to one in the signature $(+,\cdot)$. Such an atomic ...
- 335k
4
votes
Accepted
Quantifier elimination of $\exists x\bigwedge \Delta$
Given $0 < n < m$, $S^n(x) = S^m(y)$ is equivalent to $x = S^{m-n}(y)$ (by using $S2$ $n$ times). But then $\exists x \phi$, where $\phi$ is a conjunction including the formula $S^n(x) = S^m(y)$ ...
- 49.7k
4
votes
Accepted
Example of a quantifier elimination procedure for a simple-but-nontrivial theory
This theory does have quantifier elimination, and here's a proof of that fact.
First, here's the definition of a theory having quantifier elimination from Marker's Model Theory: An Introduction.
...
- 12k
4
votes
Why not add boolean constants to first order logic in model theory?
You're exactly right: nothing breaks if we include "true" and "false" as formulas (usually denoted $\top$ and $\bot$), and I think a number of things are simpler with this ...
- 80.1k
3
votes
Accepted
Questions regarding the proof of quantifier elimination of DLO
Re: your first question, the issue is that different models of a theory might behave differently. Remember that "$\Gamma\models\chi$" means "every model of $\Gamma$ satisfies $\chi$" - this is an easy ...
- 251k
3
votes
Accepted
Complete theory with quantifier elimination has finite boolean algebra
You are correct that completeness is unnecessary. In fact, it is almost certainly an error that completeness was included in the problem statement, since it makes the problem rather trivial: modulo ...
- 335k
3
votes
Accepted
Is (o-)minimality preserved by elementary equivalence?
O-minimality is preserved by elementary equivalence (it is in "Definable sets in ordered structures II" by Knight, Pillay and Steinhorn, thanks to Alex Kruckman for the reference).
Minimality however ...
- 4,886
3
votes
Accepted
Must skolem functions depend on unused variables?
Basically yes, but as sticklers for details we shouldn't literally refer to $p({\bf a})$ as the Skolemization of $\forall x\exists y(p(y))$. Rather, we should say that $\forall x\exists y(p(y))$ is ...
- 251k
3
votes
Prove completeness from elimination of quantifiers
A theory with QE is complete iff it decides all sentences in $L_{\rm qf}$.
Examples:
the theory of dense linear orders and the theory of the random graph are complete because $L_{\rm qf}$ is empty (...
- 5,264
3
votes
Accepted
Prove completeness from elimination of quantifiers
Let me add a bit to Primo Petri's answer.
Let $T$ be a consistent theory with quantifier elimination. The following are equivalent:
$T$ is complete.
For every quantifier-free sentence $\varphi$, $T\...
- 80.1k
3
votes
Modeling a formula with free variables for quantifier elimination, i.e. $\mathfrak{M} \models \phi (x) \leftrightarrow \psi (x)$
Some authors adopt the convention that ${\cal M} \models \gamma(x_1, \ldots, x_n)$ is allowed when $\gamma(x_1, \ldots, x_n)$ has free variables $x_1, \ldots, x_n$ and serves as a short-hand for ${\...
- 49.7k
3
votes
Accepted
Modeling a formula with free variables for quantifier elimination, i.e. $\mathfrak{M} \models \phi (x) \leftrightarrow \psi (x)$
A theory $T$ eliminates quantifiers if, for every formula $\varphi(x)$ (with free variables from $x = (x_1,\dots,x_n)$, where $n\geq 0$), there exists a quantifier-free formula $\psi(x)$ (with free ...
- 80.1k
2
votes
Universal instantiation with universal quantifiers within scope
Consider the statement $\forall x P(x) \rightarrow
Q$. This statement has a universal inside the statement in the sense that the statement is a conditional, the antecedent of which is a universal. As ...
- 102k
Only top scored, non community-wiki answers of a minimum length are eligible