# Tagged Questions

The tag has no usage guidance.

14 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). ...
26 views

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 ...
55 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: ...
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\}$, ...
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 ...
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, ...
62 views

44 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+-...
44 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?
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$...
90 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 ...
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?
121 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 ...
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) ...
234 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 ...
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 ...
237 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$ ...
566 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 ...
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$.
42 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$$
269 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 ...
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 (...
234 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 ...
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, ...
785 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 ...
283 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 ...
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 ...