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

116 questions
Filter by
Sorted by
Tagged with
22 views

• 321
1 vote
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 ...
• 134
1 vote
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 ...
• 434
1 vote
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$...
• 3,638
1 vote
256 views

• 2,977
1 vote
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 ...
• 41
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$. ...
• 247
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 ...
• 373
1 vote
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. ...
• 48
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 ...
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 ...
• 63
1 vote
74 views

• 5,276
404 views

• 5,981
1 vote
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 ...
• 457
1 vote
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\...