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.

Filter by
Sorted by
Tagged with
0 votes
0 answers
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 ...
user avatar
1 vote
0 answers
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. ...
user avatar
  • 48
3 votes
2 answers
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 ...
user avatar
0 votes
0 answers
33 views

Skolem Normal Form solution

I need to transform following formula to Skolem Normal Form: $$F_1:= \exists A \forall B \exists C \exists D \big(p(A,D) \wedge q(B,C)\big)$$ After changing: $$C \rightarrow C_c(B) \\D \rightarrow C_D(...
user avatar
3 votes
1 answer
49 views

Relation between quantifier elimination, elimination theory and model theory

I am interested in quantifier elimination over the field of real numbers (as in Tarski-Seidenberg theorem), particularly from an algorithmic approach (e.g. Cylindrical Algebraic Decomposition). While ...
user avatar
  • 61
1 vote
0 answers
52 views

Show a theory $\Theta$ is complete.

I'm taking a introduction to Logic course and came across the following result: Let $\Theta$ be a theory over a decidable signature $\Sigma$. Assume $\Theta$ has quantifier elimination and $F_0=\...
user avatar
2 votes
1 answer
87 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
user avatar
1 vote
1 answer
167 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$ ...
user avatar
  • 2,180
2 votes
1 answer
54 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 ...
user avatar
  • 217
0 votes
1 answer
47 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 ...
user avatar
  • 141
1 vote
1 answer
243 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 ...
user avatar
  • 6,514
2 votes
1 answer
78 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 ...
user avatar
0 votes
1 answer
68 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 ...
user avatar
  • 3
7 votes
2 answers
170 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 ...
user avatar
0 votes
1 answer
44 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 ...
user avatar
3 votes
1 answer
112 views

Quantifier elimination of $\exists x\bigwedge \Delta$

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(...
user avatar
3 votes
1 answer
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 ...
user avatar
  • 13.3k
1 vote
0 answers
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 ...
user avatar
  • 35
1 vote
1 answer
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 ...
user avatar
  • 35
0 votes
1 answer
165 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: Cn$A_{L}$ is complete. where $A_{L}=(\...
user avatar
1 vote
1 answer
164 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 $...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 9,520
-1 votes
1 answer
59 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) \...
user avatar
1 vote
1 answer
119 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; ...
user avatar
  • 1,085
0 votes
1 answer
25 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 ...
user avatar
1 vote
1 answer
104 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}, <,...
user avatar
1 vote
2 answers
286 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|...
user avatar
  • 37
2 votes
1 answer
273 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 ...
user avatar
  • 21
2 votes
1 answer
123 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{...
user avatar
0 votes
1 answer
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&...
user avatar
3 votes
0 answers
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, ...
user avatar
1 vote
0 answers
52 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 = 0$$ $$b^2-4ac \geq 0$$ Note that the first statement has a quantifier ($\...
user avatar
  • 4,892
4 votes
1 answer
212 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}...
user avatar
  • 2,041
6 votes
2 answers
488 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 $\...
user avatar
  • 5,275
1 vote
1 answer
349 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 ...
user avatar
  • 447
1 vote
1 answer
204 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\...
user avatar
1 vote
2 answers
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 ...
user avatar
  • 151
1 vote
1 answer
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 ...
user avatar
7 votes
2 answers
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}$-...
user avatar
  • 1,506
2 votes
1 answer
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$ ...
user avatar
  • 1,506
5 votes
0 answers
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 ...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 161
2 votes
1 answer
77 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{...
user avatar
  • 1,038
1 vote
0 answers
254 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 ...
user avatar
1 vote
1 answer
143 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 ...
user avatar
  • 684
1 vote
1 answer
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 ...
user avatar
  • 3,166
2 votes
1 answer
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 ...
user avatar
1 vote
1 answer
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), ...
user avatar
  • 2,950
1 vote
2 answers
100 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 ...
user avatar
  • 2,950
7 votes
1 answer
198 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$. ...
user avatar
  • 2,950