# Questions tagged [quantifier-elimination]

Quantifier elimination is the removal of all quantifiers (universal and existential) from a quantified formula in order to produce an equivalent quantifier-free formula.

55 questions
Filter by
Sorted by
Tagged with
108 views

### Exercise 3.4.3 in David Marker's “Model Theory”

While studying Model Theory for my exam, I came across the following question: a) Show that the theory of $(\mathbb{Z}, s)$ has quantifier elimination where $s(x) = x + 1.$ b) Show that the ...
264 views

### Why is quantifier elimination desirable for a given theory?

We say that a given theory $T$ admits QE in a language $\mathcal{L}$ if for every $\mathcal{L}$-formula, there is an equivalent quantifier free $\mathcal{L}$-formula. That is for every $\mathcal{L}$-...
69 views

### How much arithmetic is required to formalize quantifier elimination in Presburger arithmetic?

As we know, Presburger arithmetic can be proved decidable by demonstrating that it admits quantifier elimination, i.e. that there is an algorithm that reduces any sentence in the language to some ...
31 views

### Quantificational formatting and going from using logic with words, to using it for math proofs

Background My grasp of propositional logic is pretty good, as is my ability to translate it to and from symbols. Quantificational logic however is a little more challenging. Mostly because I get ...
46 views

167 views

### Universal instantiation with universal quantifiers within scope

If I have a formula in FOL of this kind $\forall x, [[\forall y, \neg P(x) \vee \neg S(x, y)] \vee [\forall z, A(z) \wedge G(x,z)]]$ I want to remove the universal quantifiers. What's the intuition ...
62 views

### Is (o-)minimality preserved by elementary equivalence?

Consider two structures which are elementary equivalent. If one is minimal/o-minimal, can the same be said about the other? The pooint is that one cannot quantify over sets (in first-order logic), ...
72 views

### Can every theory $T$ be expanded to a theory with quantifier elimination in the same language?

Consider a theory $T$ in a language $L$. there are several examples of theories which expand to theories in the same language which admit quantifier elimination: ring theory to $ACF_0$, Boolean ...
149 views

### Elimination of quantifiers for $\exists x\ x^2=y$

Consider the formula $\exists x\ x^2=y$ with free variable $y$. We know that it is equivalent in $Th(\mathbb R,+,0,\cdot,1, \geq)$ (the complete theory of the ordered field $\mathbb R$) to $y\geq 0$. ...
198 views

### Quantifier Elimination in the quantifier free type [closed]

Show that if in the theory of $T$ every quantifier-free type has a unique extension to a complete type, then $T$ has quantifier elimination.
83 views

311 views

### Elimination of quantifiers for the theory of equivalence relations with two infinite classes by back-and-forth

As I said in an earlier question, I'm trying to understand how to obtain elimination sets by way of back-and-forth arguments. Since I'm not totally sure I understood how it works, I wanted to check my ...
371 views

### Does the theory of equivalence relations have quantifier elimination?

I am aware that the theory of equivalence relations with infinitely many classes, all of which infinite, has quantifier elimination, as can be seen from the answer to this question. However, does the ...
73 views

### Quantifier Elimination Tree

I found this example in "A Course in Model Theory", but don't seem to figure out why it is true. Let $L$ be a language having a unary predicate $P_s$ for each (finite) binary string $s \in \{0,1\}^*$ ...
268 views

### Are algorithms for elimination of quantifiers over the reals practical?

I wanted to find the semialgebraic set in the $(a_0,a_1,a_2,a_3)$ space that guarantees that there exists at least one real root of the general polynomial equation of degree 4. For that purpose, ...
22 views

Let $\phi: F\rightarrow G$ be a relation and $id_F$ be the identity relation on $F$. Then $\phi\circ id_F = \phi$ . Attempted proof: $$\phi\ \circ id_F = \{(f,g)\in F\times G: \exists f_2\in F((f_1,... 1answer 87 views ### A test for quantifier eliumination In David Marker's "Model Theory: An Introduction" book I was trying to prove Corollary 3.1.12 which is left for the reader, but I couldn't reach any solution. The aforementioned corollary states: ... 1answer 105 views ### If \mathcal{T}_1 and \mathcal{T}_2 admit quantifier elimination, does \mathcal{T} admit quantifier elimination? Let \mathcal{T}_1 and \mathcal{T}_2 be theories with disjoint signatures \mathcal{L}_1, \mathcal{L}_2. Form a new language \mathcal{L} = \mathcal{L}_1 \cup \mathcal{L}_2 \cup \{P_1, P_2\}, ... 1answer 270 views ### Hodges exercise 2.7.1: Quantifier elimination in dense linear orderings In Hodges' A Shorter Model Theory, exercise 2.7.1 tells you to prove theorem 2.7.1, which says that the following five formulas are an elimination \Phi set for the class of all dense linear ... 1answer 237 views ### Elimination of quantifiers What does it mean that a theory admits constructive elimination of quantifiers? A theory admits elimination of quantifiers when each formula of the theory is equivalent to a quanifier-free formula, ... 1answer 185 views ### Simplifying theories with quantifier elimination Let \Sigma be a theory that has quantifier elimination. I'm trying to show that there is then an equivalent theory \Sigma^*, with each \sigma\in\Sigma^* of the form \forall x\psi(x) or \... 1answer 428 views ### Quantifier elimination for theory of equivalence relations Let \mathcal{L}=\{\sim\} and \Sigma_\infty be the set of axioms stating that: (i) \sim is an equivalence relation (ii) Every equivalence class is infinite (iii) there are infinitely many ... 0answers 62 views ### Quantifier elimination in the structure of exponential sums We consider the language L=\{+, -, ' , T, 0, 1\} Let \text{Exp}(\mathbb{C}) (the exponential sums) be the structure in that we interpret L. We define \text{Exp}(\mathbb{C}) as the set of ... 1answer 479 views ### I don't understand how the theory of algebraically closed fields admits quantifier elimination I was reading the wiki page about quantifier elimination and it says that the theory of algebraically closed fields is decidable using quantifier elimination, what I understand by this is that all ... 1answer 72 views ### Elimination of quantifiers in the strucure of polynomials and in the structure of exponentials I am looking at the elimination of quantifiers. In my notes there is the following: L=\{+, ' , T, 0, 1\} ("=" is meant to be included in L) First-order Logic: Q_1 x_1 \dots Q_m x_m \ \ [\... 2answers 98 views ### Real closed field with the restricted exponential function Is the theory of real closed fields augmented with the restricted exponential function decidable? If so, can someone explain that decision procedure? 1answer 334 views ### About the proof of a test for quantifier elimination. I've been reading D. Marker's book on Model theory. In the part dealing with quantifier elimination there's a corollary I've been trying to prove without any luck: Corollary 3.1.6 Let T be an L-... 1answer 209 views ### Show every boolean combination of \mathcal{L}-formula is equivalent one with quantifiers. This is part 2 of a question I asked here: Prove this claim about language and structures. The setting is that suppose \phi_1,\ldots,\phi_n are \mathcal{L}-formulas and \psi is a Boolean ... 1answer 385 views ### Model complete theories without quantifier elimination As we know, if a theory T admits quantifier elimination, then T is model complete. What are the simplest examples that show that the converse is not true? 1answer 295 views ### How is quantifier elimination accomplished in second and higher order logic? In first order logic we can eliminate existential quantifiers using a second order equivalence relation: \forallx\existsy P(x, y) \iff \existsf\forallx P(x, f(x)) Dropping the existential ... 0answers 94 views ### Ordering of \mathbb{R} not quantifier-free definable in L_{R} I'm reading David Marker's book "Model Theory: An Introduction" and I'm trying to solve Exercise 3.4.24 which is stated as follows: Let x and y be algebraically independent over \mathbb{R}. a) ... 1answer 930 views ### Why is Skolem normal form equisatisfiable while the second order form equivalent? I asked in another question when is it appropriate to de-Skolemize a statement. The answer, I'm not sure I'm satisfied with yet, relies on a second order logical equivelance, but Skolem normal form ... 2answers 140 views ### Trying to understand negation of quantifiers Trying to understand the negation of the following: For this: ∀x~P(x) I have this as negation: ~∃xP(x) For this: ~∃x(∀yP(y) Λ Q(x)) I have this: ∀x(~∃yP(y) V ~Q(x)) Are these correct? If not please ... 2answers 464 views ### Proper definition of quantifier elimination I study Marker book "Model Theory, An Introduction". Definition 3.1.1 on page 72 defines "theory T has quantifier elimination". A theory T has quantifier elimination if for every formula \phi ... 2answers 3k views ### How is a quantifier-free formula actually interpreted? My understanding is that a quantifier-free formula in FOL is simply a formula that contains no quantifiers, just possibly free variables. How is such a formula interpreted? My understanding is that if ... 1answer 101 views ### Why Quantifier Free Formulas define Linear Functions. How do you prove that functions definable by quantifier-free formulas must be linear? I am interested for the structure \langle Q,+,0\rangle. 2answers 52 views ### Resultant(f,g) says when there exist \phi,\psi such that \psi f + \phi g = 0. How do I actually find them? If f and g \in k[X] are two polynomials such that \textrm{Res }(f,g)=0 how do I find \phi and \psi with \deg \phi < \deg f and \deg \psi < \deg g such that$$\psi f +\phi g =0$$1answer 357 views ### Characterization of the First Order Theory of Ordered Abelian Groups via Quantifier Elimination In the paper "Elimination of Quantifiers in Algebraic Structures" Macintyre, McKenna and van den Dries, proved that every field (ordered field) whose theory admits quantifier elimination in the ... 2answers 444 views ### Herbrand Logic-Fitch System Given$$\forall x.(p(x) \implies q(x))\quad and \quad p(a)$$use the Fitch system to prove q(a) I have started:$$\\1) \forall X.(p(X) \implies q(X)) \qquad (Premise)2) p(a) \qquad (...
I have been working with Tent and Ziegler's Model Theory. I am on the Quantifier elimination chapter, and there they mention Robinson's test. It says that, for an $L$-theory $T$ three statements ...
### Quantifier Elimintion of $(\Bbb{Q},+,0)$
I want to prove that the structure $(\Bbb{Q},+,0)$ has Quantifier Elimination. I can prove it for some simple basic formulas, but what if i get a formula which says that i have a linear combination, ...