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

105 questions
Filter by
Sorted by
Tagged with
74 views

• 363
115 views

### Counter-example of o-minimal structure but do not admit elimination of quantifiers

I want a counter-example of o-minimal structure but do not admit elimination of quantifiers, we know that the inverse is true as (R,<,+,×,0,1) Tarski's theorem
1 vote
283 views

### Theory of infinite vector spaces admits quantifier elimination

Definition. A formula is called simple if it is of the form $$\exists x(\psi_1\wedge\dots\wedge \psi_n\wedge\neg\chi_1\wedge\dots\wedge\neg\chi_m),$$ where $\psi_1,\dots,\psi_n,\chi_1,\dots,\chi_m$ ...
• 2,318
66 views

### Must skolem functions depend on unused variables?

When converting formulas to CNF, we replace existentially quantified variables with Skolem functions that depend on surrounding universally quantified variables. For example, in ∀x ∃y p(x,y) the value ...
• 217
1 vote
109 views

### Presburger arithmetic vs Linear Integer Arithmetic

I always work with these two and use it with no distinction, but I am probably wrong. I mean, are their signatures the same? And their axioms? I know that, for instance, the quantifier elimination ...
• 207
1 vote
397 views

### Example of a quantifier elimination procedure for a simple-but-nontrivial theory

Is there a simple-but-nontrivial example of a concrete quantifier elimination procedure with a concrete theory, especially one that's a standard example of what a constructive argument for quantifier ...
• 9,238
110 views

### Quantifier Elimination Pure Identity Language in Chang

In Chang & Keisler's Model Theory, quantifier elimination on the theory of the pure identity language is shown. However, I'm confused about the notion of "basic formula" for which any ...
106 views

### Why does skolemization just happen under the scope of universal?

I understand you can skolemize an existential under the scope of a universal and get : $\forall$x $\exists$y.P(x,y) $\Leftrightarrow$ $\forall$x. P(x, f(x)) what if the universal quantifier is under ...
224 views

### How to show that $\mathbb{R}$ in the language of rings does not admit quantifier elimination?

I am studying for an exam in an introductory mathematical logic course. Suppose we are working in the language of rings $\mathcal{L}=(+,-,\cdot,0,1)$. Then $\mathbb{R}$ does not admit quantifier ...
56 views

### Help understanding the result of a Cylindrical Algebraic Decomposition of $V\left( {x,y,z} \right) = {x^2} + {y^2} + {z^2} < 1$?

From https://mathworld.wolfram.com/CylindricalAlgebraicDecomposition.html it is said that: Define a cell in ${\mathbb{R}^1}$ as an open interval or a point. A cell in ${\mathbb{R}^{k + 1}}$ then has ...
I'm currently studying logic and theory of computation (right now I'm concerned with quantifier elimination). Consider the successor theory generated by the following axioms $$(S1)\,\forall\, x\neg S(... • 517 3 votes 1 answer 129 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 ... • 16.8k 1 vote 0 answers 205 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 ... • 35 1 vote 1 answer 109 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 ... • 35 0 votes 1 answer 172 views ### Theory in (\mathbb{N};0,S,<) is complete? [closed] My question is how I show the corollary 32B(a) from the book A mathematical introduction to logic by Herbert Enderton. Corollary 32B(a) on page 196 says that: CnA_{L} is complete. where A_{L}=(\... 1 vote 1 answer 220 views ### 'Classical' proof of Main Theorem of elimination theory by Mumford I despair on a argument in the in proof of the Main Theorem of elimination theory (pges 33-35) in Mumford's Algebraic Geometry I: Complex Algebraic Varieties. The MToet states that the projection ... 1 vote 1 answer 77 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 ... • 9,827 -1 votes 1 answer 70 views ### What is the correct way to apply contrapositive law in a proposition using universal quantifiers? Its possible to eliminate the quantifier? I reach the following conclusion during a proof: (\forall x)(\forall y)([y < x \Rightarrow H(y) < H(x)]), the contrapositive of this statment is (\forall x)(\forall y)([H(x) \leq H(y) \... 1 vote 1 answer 146 views ### Primitive recursive predicates for exponentiation and multiplication I have the following informally stated and weakly held beliefs, some of which seem inconsistent to me upon further reflection. I'm wondering where the source of the error(s) in my thinking might be; ... • 1,103 0 votes 1 answer 36 views ### How can i prove that if some set is a subset of every set in a family of sets, then it is a subset of the intersection of family too. The question is stated as: Prove: (\forall B)(B \in F \Rightarrow C \subseteq B) \Rightarrow C \subseteq \bigcap_{A \in F}A Thats what i thinked in a textual way: If we assume that for every B, if ... 1 vote 1 answer 118 views ### Is it possible to use quantifier elimination theorem in the structure \langle\mathbb{Z}, <, = \rangle? I need to solve the problem: is it possible to use quantifier elimination theorem in the structure \langle\mathbb{Z}, <, = \rangle. I have a proof that it is possible for \langle\mathbb{R}, <,... 1 vote 2 answers 332 views ### Consider theory T = Th(M, ~, =). Show that T has quantifier elimination Consider theory \tau = Th(M,\sim, =), where M is an infinite set, = is the equality relation, and \sim is an equivalence relation over M with infinitely many equivalence classes (i.e. \{\{n|... • 37 2 votes 1 answer 343 views ### Exercise 3.4.1 Markers model theory I am working through some exercises from Marker's Model Theory in self-study and I am stuck at Exercise 3.4.1 as I do not know how to formally prove that a theory has quantifier elimination. I am ... • 21 2 votes 1 answer 155 views ### Quantifier elimination and extending quantifier free types I am trying to prove the following theorem : Let T be some L-theory. Suppose that for any n, every type p(\bar{x})\in S_n(T) is the only type extending \{\varphi(\bar{x})\in p |\varphi(\bar{... 0 votes 1 answer 146 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&... 3 votes 0 answers 60 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 0 answers 54 views ### Is Quantifier Elimination possible in this convexity problem? Given a, b and c real numbers, the following statements are equivalent:$$\exists x \in \mathbb{R}; ax^2 + bx + c = 0b^2-4ac \geq 0$$Note that the first statement has a quantifier (\... • 5,104 4 votes 1 answer 298 views ### \Sigma_{(\mathbb{N},<)} does not admit elimination of quantifiers I'm beginning to study mathematical logic from a sort of book my professor wrote for his classes, and when talking about the theory of natural numbers with the ordering, i.e. the structure (\mathbb{N}... • 2,469 6 votes 2 answers 611 views ### Quantifier elimination for \mathbb Z as a group? Question 1: What definable sets should one add to the language to obtain quantifier elimination for the theory of (\mathbb Z, +), i.e. the integers as a group (short of simply Morleyizing)? An \... • 5,545 1 vote 1 answer 407 views ### The theory of (Z, s) has quantifier elimination Let T = \text{Th}(\mathbb{Z}, s) where s is the successor function. I want to show quantifier elimination (QE) for T and construct a concrete \omega-saturated model. However, I am unsure ... • 457 1 vote 1 answer 270 views ### Questions regarding the proof of quantifier elimination of DLO So this is the proof in David Marker's Model theory book, Theorem 3.1.3. I am a bit confused over the first line of the proof. It reads : "First suppose \phi is a sentence. If \mathbb{Q}\models\... • 2,097 1 vote 2 answers 282 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 ... • 151 1 vote 1 answer 441 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 ... 8 votes 2 answers 631 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}-... • 1,604 2 votes 1 answer 125 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 ... • 1,604 5 votes 0 answers 141 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 1 answer 87 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 ... • 161 2 votes 1 answer 89 views ### Complete theory with quantifier elimination has finite boolean algebra I have the following problem written down: If \mathcal{L} has a finite signature, with no functions, and T is a complete theory with quantifier elimination, then the boolean algebra of \mathcal{... • 1,047 1 vote 0 answers 288 views ### Show that the theory of  (\mathbb{Z}, s) has quantifier elimination. I am trying to solve Exercise 3.4.3 from Marker's Model Theory: An introduction which states a) Show that the Theory of (\mathbb{Z},s) has quantifier elimination, where s(x)=x+1. Show that this ... 1 vote 1 answer 176 views ### Proof concerning quantifier elimination and substructures I'm new to everything involving languages and I'm having trouble proving properties with quantifier elimination. In particular what's below. Suppose we know the following: Lemma (L1): Let N \leq ... • 704 1 vote 1 answer 131 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 ...
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 ...