Skip to main content

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
3 votes
1 answer
22 views

Does any first-order formula have a quantifier-free consequence?

In David Marker's "Model Thoery: An Introduction", the author gives a criteria for quantifier elimination by common substructure as Theorem 3.1.4. In his proof, he defines a set $\Gamma(\...
YSouSerious's user avatar
4 votes
1 answer
80 views

Axiomatizing a QE theory by $\forall \bar{x}\exists{y}\phi(\bar{x},y)$

as a part of a model theory assignment I am asked to prove that if a theory T has quantiier elimination, then it can be axiomatized by sentences of the form $\forall\bar{x}\exists{y}\phi(\bar{x},y)$, ...
mercunicorn's user avatar
3 votes
0 answers
48 views

Quantifier elimination for Boolean algebras

Is there a reference in English for the proof that Boolean algebras admit quantifier elimination? I'm interested in how quantifier elimination can be performed. However, the result of Tarski is not ...
user1868607's user avatar
  • 5,801
0 votes
0 answers
61 views

Cardinalities of an extension to a theory

I have a universal first order universal theory T such that: -T is universal over a finite language L -T has a model completion T ⊆ T* -T* is countable, has quantifier elimination (QE) and is complete....
mercunicorn's user avatar
0 votes
0 answers
28 views

questions about proving ACF(Algebraically Closed Fields) has quantifier elimination

Hi I am trying to prove that ACF has quantifier elimination. A. Background: It uses the follow theory: First order theory $\mathcal{T}=\left<\mathcal{L}_\mathcal{A},\mathbb{L}_\mathcal{A},T,T^*\...
Shore's user avatar
  • 321
1 vote
2 answers
124 views

Modeling a formula with free variables for quantifier elimination, i.e. $\mathfrak{M} \models \phi (x) \leftrightarrow \psi (x)$

I am an undergrad doing an independent study with a professor on model theory using David Marker's Model Theory : An Introduction. I am new to the subject so this question may be naïve or misguided. I ...
August's user avatar
  • 134
1 vote
0 answers
66 views

Elimination set for the term algebra in A Shorter Model Theory

I'm reading Hodges' A Shorter Model Theory. In the section about quantifier elimination, theorem $2.7.5$ proves that some set of formulas is an elimination set of the term algebra (under a different ...
Frousse's user avatar
  • 434
1 vote
1 answer
128 views

Prove that divisibility between two natural numbers is not definable in arithmetic [duplicate]

Prove that there is no formula $\varphi(v,u)$ so that $(\mathbb N; 0, 1, +) \models \varphi[x,y]$ iff $x$ divides $y$. Here is what I have so far: assume on the contrary that we do have such $\varphi$...
Squirrel-Power's user avatar
1 vote
3 answers
256 views

Quantifier elimination in ACF from an example

The (first order) theory of algebraically closed field (ACF) admits quantifier elimination. That means that for each (possibly) quantified statement $\phi$ in the theory, we can construct a statement $...
Weier's user avatar
  • 581
3 votes
1 answer
123 views

Understanding some uses of the Separation Lemma

In my Model Theory course, the lecturer introduces the following Separation Lemma: For $\Sigma,\Pi$ $\mathscr{L}$-theories and $\Gamma\subseteq\text{Sent}(\mathscr{L})$ a set closed under conjunction ...
kazziG's user avatar
  • 61
1 vote
0 answers
15 views

Does quantifier elimination preserve equi-satisfiability or equivalence?

Does quantifier elimination (QE) preserve equi-satisfiability or equivalence? I always thought it preserves equi-satisfiability (and not equivalence) but in the book [Bradley, Manna], they say both ...
Theo Deep's user avatar
  • 247
1 vote
0 answers
37 views

Are there terminating methods to provide models of first-order theory formulae?

If a first-order theory is decidable on its existential fragment, does this imply that we have a method (that guarantees termination) to obtain models of existentially quantified formulae within this ...
Theo Deep's user avatar
  • 247
4 votes
1 answer
90 views

Why not add boolean constants to first order logic in model theory?

I'm working through Marker's (Model Theory: An Introduction) presentation of quantifier elimination. Things get a bit awkward with the use of formulas like $x_1 = x_1$ to represent truth, and $x_1 \...
TomKern's user avatar
  • 2,977
1 vote
0 answers
36 views

Effective algorithms for differentially closed fields

There are (many) model-theoretic proofs that $DCF_0$, the theory of differentially closed fields of characteristic zero admits quantifier elimination (see "Model Theory" by Marker, Chapter 4 ...
toghrul's user avatar
  • 41
0 votes
0 answers
65 views

Nelson-Oppen: Does 'quantifier-free' mean that is decidable?

Given two theories $T_1$ and $T_2$ with disjoint-signatures $Σ_1$ and $Σ_2$ respectively, and a conjunction of literals $φ$ over $Σ_1 \cup Σ_2$, we want to decide if $φ$ is satisfiable under $T1∪T2$. ...
Theo Deep's user avatar
  • 247
0 votes
0 answers
122 views

Proof in "A Mathematical Introduction to Logic » by Herbert Enderton

I’m studying section 3.2 in Herbet Enderton’s "A Mathematical Introduction to Logic" and I can’t seem to find a justification for something in a proof. The domain of the structures we are ...
davinci_07's user avatar
1 vote
0 answers
43 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. ...
Zach's user avatar
  • 48
4 votes
2 answers
363 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
3 votes
1 answer
82 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 ...
ccln's user avatar
  • 63
1 vote
0 answers
74 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=\...
davinci_07's user avatar
2 votes
1 answer
175 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
connaissant's user avatar
1 vote
1 answer
410 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$ ...
MyWorld's user avatar
  • 2,398
2 votes
1 answer
103 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 ...
rwallace's user avatar
  • 245
1 vote
1 answer
229 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 ...
Theo Deep's user avatar
  • 247
1 vote
1 answer
531 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 ...
Greg Nisbet's user avatar
  • 11.7k
2 votes
1 answer
130 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 ...
hunterboerner's user avatar
0 votes
1 answer
130 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 ...
zara_M's user avatar
  • 3
7 votes
2 answers
291 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 ...
Jarne Renders's user avatar
0 votes
1 answer
66 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 ...
Tuong Nguyen Minh's user avatar
3 votes
1 answer
147 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(...
defacto's user avatar
  • 623
3 votes
1 answer
160 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 ...
user107952's user avatar
  • 20.7k
1 vote
0 answers
308 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 ...
ta1234's user avatar
  • 35
1 vote
1 answer
152 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 ...
ta1234's user avatar
  • 35
0 votes
1 answer
179 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}=(\...
Magic Unicorn's user avatar
1 vote
1 answer
305 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 $...
user267839's user avatar
  • 7,399
1 vote
1 answer
82 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 ...
Christopher King's user avatar
-1 votes
1 answer
102 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) \...
Paulo Henrique L. Amorim's user avatar
1 vote
1 answer
176 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; ...
Thurmond's user avatar
  • 1,103
0 votes
1 answer
68 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 ...
Paulo Henrique L. Amorim's user avatar
1 vote
1 answer
131 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}, <,...
Кирилл Куценок's user avatar
1 vote
2 answers
411 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|...
RnHdw's user avatar
  • 47
2 votes
1 answer
491 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 ...
bluci's user avatar
  • 21
2 votes
1 answer
206 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{...
Binyamin Riahi's user avatar
0 votes
1 answer
189 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&...
Maryam Ajorlou's user avatar
3 votes
0 answers
64 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, ...
Ronald S Merritt's user avatar
1 vote
0 answers
58 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 ($\...
Malkoun's user avatar
  • 5,276
4 votes
1 answer
404 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}...
Lorenzo's user avatar
  • 2,601
8 votes
2 answers
781 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 $\...
tcamps's user avatar
  • 5,981
1 vote
1 answer
530 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 ...
Ibrahim's user avatar
  • 457
1 vote
1 answer
381 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\...
some1fromhell's user avatar