The tag has no usage guidance.

learn more… | top users | synonyms

0
votes
1answer
12 views

Decidability of quantifier-free formulae in Peano- and True Arithmetic

It is well-known that validity in Peano Arithmetic is undecidable. It is less well-known that validity is already undecidable in True Arithmetic (the theory of the standard model of Peano Arithmetic). ...
0
votes
1answer
25 views

Concerning substitution and existential elimination in classic natural deduction using sequents

I am trying to prove $\exists x(P\lor Q)\vdash \exists x P \lor \exists x Q$, so I have: $$\begin{array}{r l l} (1) ~&~~ \exists x (P \lor Q) ~&~ \mbox{[premise]} \\ (2) ~&~ \quad (P \...
1
vote
1answer
59 views

Elimination of quantifiers for the theory of equivalence relations with two infinite classes by back-and-forth

As I said in an earlier question, I'm trying to understand how to obtain elimination sets by way of back-and-forth arguments. Since I'm not totally sure I understood how it works, I wanted to check my ...
3
votes
1answer
64 views

Does the theory of equivalence relations have quantifier elimination?

I am aware that the theory of equivalence relations with infinitely many classes, all of which infinite, has quantifier elimination, as can be seen from the answer to this question. However, does the ...
1
vote
0answers
38 views

Quantifier Elimination Tree

I found this example in "A Course in Model Theory", but don't seem to figure out why it is true. Let $L$ be a language having a unary predicate $P_s$ for each (finite) binary string $s \in \{0,1\}^*$ ...
5
votes
0answers
49 views

Are algorithms for elimination of quantifiers over the reals practical?

I wanted to find the semialgebraic set in the $(a_0,a_1,a_2,a_3)$ space that guarantees that there exists at least one real root of the general polynomial equation of degree 4. For that purpose, ...
0
votes
0answers
19 views

Composing relation with identity yields original relation

Let $\phi: F\rightarrow G$ be a relation and $id_F$ be the identity relation on $F$. Then $\phi\circ id_F = \phi$ . Attempted proof: $$\phi\ \circ id_F = \{(f,g)\in F\times G: \exists f_2\in F((f_1,...
0
votes
0answers
33 views

Did I correctly translate 'Whoever loves Myfanwy, loves a philosopher only if the latter loves Myfanwy too.' into quantificational logic?

There is an exercise in my textbook. Suppose ‘$m$’ denotes Myfanwy, ‘$n$’ denotes Ninian, ‘$o$’ denotes Olwen, ‘$Fx$’ means x is a philosopher, ‘$Gx$’ means x speaks Welsh, ‘$Lxy$’ means $x$ loves ...
1
vote
1answer
54 views

A test for quantifier eliumination

In David Marker's "Model Theory: An Introduction" book I was trying to prove Corollary 3.1.12 which is left for the reader, but I couldn't reach any solution. The aforementioned corollary states: ...
4
votes
1answer
51 views

If $\mathcal{T}_1$ and $\mathcal{T}_2$ admit quantifier elimination, does $\mathcal{T}$ admit quantifier elimination?

Let $\mathcal{T}_1$ and $\mathcal{T}_2$ be theories with disjoint signatures $\mathcal{L}_1, \mathcal{L}_2$. Form a new language $\mathcal{L} = \mathcal{L}_1 \cup \mathcal{L}_2 \cup \{P_1, P_2\}$, ...
3
votes
1answer
48 views

Hodges exercise 2.7.1: Quantifier elimination in dense linear orderings

In Hodges' A Shorter Model Theory, exercise 2.7.1 tells you to prove theorem 2.7.1, which says that the following five formulas are an elimination $\Phi$ set for the class of all dense linear ...
4
votes
1answer
90 views

Elimination of quantifiers

What does it mean that a theory admits constructive elimination of quantifiers? A theory admits elimination of quantifiers when each formula of the theory is equivalent to a quanifier-free formula, ...
1
vote
1answer
62 views

Simplifying theories with quantifier elimination

Let $\Sigma$ be a theory that has quantifier elimination. I'm trying to show that there is then an equivalent theory $\Sigma^*$, with each $\sigma\in\Sigma^*$ of the form $\forall x\psi(x)$ or $\...
4
votes
1answer
110 views

Quantifier elimination for theory of equivalence relations

Let $\mathcal{L}=\{\sim\}$ and $\Sigma_\infty$ be the set of axioms stating that: (i) $\sim$ is an equivalence relation (ii) Every equivalence class is infinite (iii) there are infinitely many ...
0
votes
0answers
45 views

Quantifier elimination in the structure of exponential sums

We consider the language $L=\{+, -, ' , T, 0, 1\}$ Let $\text{Exp}(\mathbb{C})$ (the exponential sums) be the structure in that we interpret $L$. We define $\text{Exp}(\mathbb{C})$ as the set of ...
1
vote
1answer
90 views

I don't understand how the theory of algebraically closed fields admits quantifier elimination

I was reading the wiki page about quantifier elimination and it says that the theory of algebraically closed fields is decidable using quantifier elimination, what I understand by this is that all ...
3
votes
1answer
57 views

Elimination of quantifiers in the strucure of polynomials and in the structure of exponentials

I am looking at the elimination of quantifiers. In my notes there is the following: $L=\{+, ' , T, 0, 1\}$ ($"="$ is meant to be included in $L$) First-order Logic: $Q_1 x_1 \dots Q_m x_m \ \ [\...
0
votes
0answers
40 views

Fourier-Motzkin elimination number of constraints

I have this question: Consider Fourier-Motzkin elimination algorithm. Let n = 2^p+p+2, where p is non-negative integer. Consider a polyhedron in R^n defined by the m = 8(n 3) constraints. +-xi+-xj+-...
1
vote
1answer
43 views

Real closed field with the restricted exponential function

Is the theory of real closed fields augmented with the restricted exponential function decidable? If so, can someone explain that decision procedure?
1
vote
1answer
121 views

About the proof of a test for quantifier elimination.

I've been reading D. Marker's book on Model theory. In the part dealing with quantifier elimination there's a corollary I've been trying to prove without any luck: Corollary 3.1.6 Let $T$ be an $L$...
1
vote
1answer
84 views

Show every boolean combination of $\mathcal{L}$-formula is equivalent one with quantifiers.

This is part 2 of a question I asked here: Prove this claim about language and structures. The setting is that suppose $\phi_1,\ldots,\phi_n$ are $\mathcal{L}$-formulas and $\psi$ is a Boolean ...
2
votes
1answer
150 views

Model complete theories without quantifier elimination

As we know, if a theory $T$ admits quantifier elimination, then $T$ is model complete. What are the simplest examples that show that the converse is not true?
2
votes
1answer
117 views

How is quantifier elimination accomplished in second and higher order logic?

In first order logic we can eliminate existential quantifiers using a second order equivalence relation: $\forall$x$\exists$y P(x, y) $\iff$ $\exists$f$\forall$x P(x, f(x)) Dropping the existential ...
3
votes
0answers
70 views

Ordering of $\mathbb{R}$ not quantifier-free definable in $L_{R}$

I'm reading David Marker's book "Model Theory: An Introduction" and I'm trying to solve Exercise 3.4.24 which is stated as follows: Let $x$ and $y$ be algebraically independent over $\mathbb{R}$. a) ...
2
votes
1answer
225 views

Why is Skolem normal form equisatisfiable while the second order form equivalent?

I asked in another question when is it appropriate to de-Skolemize a statement. The answer, I'm not sure I'm satisfied with yet, relies on a second order logical equivelance, but Skolem normal form ...
1
vote
2answers
75 views

Trying to understand negation of quantifiers

Trying to understand the negation of the following: For this: ∀x~P(x) I have this as negation: ~∃xP(x) For this: ~∃x(∀yP(y) Λ Q(x)) I have this: ∀x(~∃yP(y) V ~Q(x)) Are these correct? If not please ...
6
votes
2answers
236 views

Proper definition of quantifier elimination

I study Marker book "Model Theory, An Introduction". Definition 3.1.1 on page 72 defines "theory T has quantifier elimination". A theory $T$ has quantifier elimination if for every formula $\phi$ ...
4
votes
2answers
543 views

How is a quantifier-free formula actually interpreted?

My understanding is that a quantifier-free formula in FOL is simply a formula that contains no quantifiers, just possibly free variables. How is such a formula interpreted? My understanding is that if ...
2
votes
1answer
93 views

Why Quantifier Free Formulas define Linear Functions.

How do you prove that functions definable by quantifier-free formulas must be linear? I am interested for the structure $\langle Q,+,0\rangle$.
0
votes
2answers
41 views

Resultant$(f,g)$ says when there exist $\phi,\psi$ such that $\psi f + \phi g = 0$. How do I actually find them?

If $f$ and $g \in k[X]$ are two polynomials such that $\textrm{Res }(f,g)=0$ how do I find $\phi$ and $\psi$ with $\deg \phi < \deg f$ and $\deg \psi < \deg g$ such that $$\psi f +\phi g =0$$
7
votes
0answers
267 views

Characterization of the First Order Theory of Ordered Abelian Groups via Quantifier Elimination

In the paper "Elimination of Quantifiers in Algebraic Structures" Macintyre, McKenna and van den Dries, proved that every field (ordered field) whose theory admits quantifier elimination in the ...
1
vote
2answers
299 views

Herbrand Logic-Fitch System

Given $$\forall x.(p(x) \implies q(x))\quad and \quad p(a)$$ use the Fitch system to prove q(a) I have started: $$\\$$ $$1) \forall X.(p(X) \implies q(X)) \qquad (Premise)$$ $$2) p(a) \qquad (...
1
vote
1answer
230 views

Proof of Robinson's test

I have been working with Tent and Ziegler's Model Theory. I am on the Quantifier elimination chapter, and there they mention Robinson's test. It says that, for an $L$-theory $T$ three statements ...
3
votes
1answer
143 views

Quantifier Elimintion of $(\Bbb{Q},+,0)$

I want to prove that the structure $(\Bbb{Q},+,0)$ has Quantifier Elimination. I can prove it for some simple basic formulas, but what if i get a formula which says that i have a linear combination, ...
3
votes
1answer
776 views

How to prove that something is definable or not definable in a given structure?!

Hello friends of mathematics :) I have some problems with the topic "Is something definable in a structure". I can solve some problems for example the following questions: Is the relation definable ...
4
votes
3answers
282 views

Want to show Quantifier elimination and completeness of this set of axioms…

Let $\Sigma_\infty$ be a set of axioms in the language $\{\sim\}$ (where $\sim$ is a binary relation symbol) that states: (i) $\sim$ is an equivalence relation; (ii) every equivalence class ...
5
votes
2answers
116 views

Need a FOL derivation validated. Unclear on universal generalization restriction.

I'm currently working through Suppes' Introduction to Logic, and while the text is excellent, the lack of solutions to the exercises can be frustrating at times. This is one of those times. I've ...
2
votes
1answer
193 views

Reducing quantification to probability

I was thinking about some problem involving quantifiers (the existencial and universal quantifiers) and I noticed how it might resemble probability in a sense. They both assume a variable and its ...
12
votes
2answers
1k views

Software for solving geometry questions

When I used to compete in Olympiad Competitions back in high school, a decent number of the easier geometry questions were solvable by what we called a geometry bash. Basically, you'd label every ...