# 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.

102 questions
Filter by
Sorted by
Tagged with
11 views

### Composition and removal of quantifiers in predicate logic in PCNF (prenex conjunctive normal form) - resources

I am struggling in working with predicate logic proofs. The material I am using as reference is not very clear in the explanations, I feel there is an exceeding use of acronyms and symbols in ...
1 vote
34 views

### Quantifier elimination for non-polynomial functions

I lack much of the theoretical background for QE (my background is primarily optimization and control), but have stumbled across it in the process of learning about hybrid automata & decidability. ...
113 views

### Prove completeness from elimination of quantifiers

I have been asked to prove that DAG,the theory of non-trivial torsion-free divisible abelian groups, has quantifier elimination and deduce from that that it is complete. What are the conditions to ... 33 views

109 views

### Quantifier elimination for $\text{ACF0}$ over signature $(+,·)$.

We know that the complex field has quantifier elimination. This is usually in reference to the signature $(+,·,-,0,1)$. My question is, does it also have quantifier elimination with reference to the ...
1 vote
130 views

### Showing the natural numbers $(\Bbb{N},<)$ do not admit quantifier elimination

I have seen in lots of texts that the theory of $(\Bbb{N},<)$ does not admit quantifier elimination. I am trying to prove why, and although I can find hints in the literature, I am struggling to ...
1 vote
75 views

### An equivalence to quantifier elimination

So I am studying the theory of quantifer elimination and have come across the following equivalence. I am defining quantifier elimination as: a theory $T$ admits quantifier-elimination (QE) if every ...
165 views

1 vote
69 views

### Quantifier Elimination for the theory of hyperreals with a much less than relation

We define a binary predicate $\ll$ over hyperreals as follows: $x \ll y$ if for every positive standard real number $r$, we have that $0 \le rx < y$. Now consider the first-order theory of true ...
59 views

1 vote
286 views

121 views

### Around the Elimination of Quantifier

I-Does it true that having or not having elimination of quantifier property, say $EQ$, for structures depends on the language being used for describing the structure? If so, so one can "always&...
59 views

### Does a theory $(\sim, =)$ admit quantifier elimination?

We have $\sim$ relation of equivalence and $=$. We also know that there are infinite number of finite classes of equivalence. Does the theory with signature $(\sim, =)$ admits QE? My answer is no, ...
1 vote
52 views

488 views

1 vote
244 views

### Quantifier elimination exercise

Let $L$ be the language $\{c_n : n \in \mathbb{N} \}$, and $T$ the theory $\{c_i \neq c_j : i < j < \omega \}$. I want to show that $T$ has quantifier elimination (QE). It suffices to show QE ...
1 vote
391 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 theory of ...
553 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}$-...
96 views

### If $T$ admits quantifier elimination in $\mathcal{L}$, does it admit quantifier elimination in $\mathcal{L}(c)$?

I know this is true: If $T$ is an $\mathcal{L}$-theory and it admits quantifier elimination in $\mathcal{L}(c)=\mathcal{L}\cup\{c\}$, where $c$ is a constant symbol not in $\mathcal{L}$, then $T$ ...
125 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 ...
1 vote
60 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 ...
77 views

1 vote
118 views

### How quantifier elimination works

Wondering if you could take something like the transitive relation and rewrite it quantifier free. $$\forall a,b,c\in X:(aRb\wedge bRc)\Rightarrow aRc$$ The key questions are: If the transitive ...
280 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 ...
1 vote
104 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), ...
1 vote
### 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 ...
### 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$. ...