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
3
votes
1
answer
74
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 \...
- 2,323
1
vote
0
answers
25
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 ...
- 11
0
votes
0
answers
44
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$. ...
- 207
0
votes
0
answers
80
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 ...
- 363
0
votes
0
answers
39
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 ...
- 159
1
vote
0
answers
39
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
3
votes
2
answers
182
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 ...
user957499
3
votes
1
answer
67
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 ...
- 61
1
vote
0
answers
63
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=\...
- 363
2
votes
1
answer
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
- 61
1
vote
1
answer
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
2
votes
1
answer
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
1
answer
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
1
answer
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
2
votes
1
answer
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 ...
- 123
0
votes
1
answer
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 ...
- 3
7
votes
2
answers
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 ...
- 907
0
votes
1
answer
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 ...
3
votes
1
answer
136
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(...
- 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:
Cn$A_{L}$ is complete.
where $A_{L}=(\...
- 129
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{...
- 135
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&...
- 429
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, ...
- 305
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 = 0$$
$$b^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 ...
- 71
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 ...
- 165
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 ...
- 3,472
2
votes
1
answer
313
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 ...