Questions: Quantifier Elimination and Decidability

Question 1

Why is the first-order theory of the real numbers decidable, while the first-order theory of the integers (Peano arithmetic) is not?

• A. Real numbers are uncountable, giving more models for sentences to be true in
• B. The theory of real closed fields admits quantifier elimination, reducing decidability to quantifier-free polynomial arithmetic; Peano arithmetic does not admit QE
• C. Real-number sentences have no existential quantifiers, making them trivially decidable
• D. Tarski's axioms for real closed fields are simpler and fewer than Peano's axioms

Answer: (B)

Tarski proved that the theory of real closed fields (RCF) admits quantifier elimination: every first-order sentence about the reals is equivalent to a quantifier-free Boolean combination of polynomial equalities and inequalities, which is decidable. The integers lack this property — Gödel's incompleteness theorem shows that no consistent, recursively axiomatizable extension of Peano arithmetic can decide all first-order sentences. The presence or absence of QE is the precise diagnostic for this boundary between decidable and undecidable arithmetic.

Question 2

A logician applies quantifier elimination to the formula ∃y (y² = x ∧ y > 0) in the theory of real closed fields. The result is a quantifier-free formula equivalent to x > 0. What does this demonstrate?

• A. The formula is false whenever x > 0, so the existential quantifier is vacuous
• B. Every first-order formula about the reals, even one asking whether a positive square root exists, can be reduced to a Boolean combination of polynomial inequalities with no quantifiers
• C. Quantifier elimination only works when the formula contains exactly one existential quantifier
• D. The result x > 0 shows that quantifier elimination always produces simpler formulas than the original

Answer: (B)

The formula ∃y (y² = x ∧ y > 0) asks: 'does x have a positive square root?' The quantifier-free equivalent x > 0 captures exactly the same information — x has a positive square root iff x is positive. This illustrates the general claim: no matter how complex the quantifier structure, every RCF formula reduces to a quantifier-free one. The reduction converts a logical question (does such a y exist?) into a purely algebraic condition (is x positive?), making the whole theory decidable.

Question 3

A theory that admits quantifier elimination is automatically decidable.

• T. True
• F. False

Answer: False

QE reduces the decidability of the full first-order theory to the decidability of the quantifier-free fragment — it does not guarantee decidability on its own. The correct statement is: if T admits QE and the quantifier-free theory of T is decidable, then T is decidable. For real closed fields, the quantifier-free theory (polynomial equalities and inequalities) is indeed decidable, so the full theory is too. But a theory could in principle admit QE while having an undecidable quantifier-free fragment, in which case the full theory would still be undecidable.

Question 4

In the theory of real closed fields, the formula ∀x∃y (y² = x) is false (not every real number has a real square root), and quantifier elimination can produce the equivalent quantifier-free formula 'false' (or ⊥).

• T. True
• F. False

Answer: True

QE applies to all first-order formulas, including false sentences. ∀x∃y (y² = x) fails for negative x, so it is false in RCF. After quantifier elimination, the equivalent quantifier-free formula is the Boolean constant 'false' (⊥), which is a legitimate quantifier-free formula. This shows QE is not just a simplification technique — it is a complete decision procedure that can certify both truth and falsity of any first-order sentence about the reals.

Question 5

Explain why quantifier elimination converts a logic problem (is this sentence provable in T?) into an algebraic problem, and why this makes decidability achievable.

Model answer: QE eliminates all ∃ and ∀ quantifiers, reducing every formula to a Boolean combination of atomic formulas — in RCF, these are polynomial equalities and inequalities like p(x₁,…,xₙ) ≥ 0. Deciding these atomic formulas is an algebraic question (is this polynomial system satisfiable over the reals?) rather than a logical one. Algorithms like cylindrical algebraic decomposition solve this computably. So the decidability of the full first-order theory follows from the computability of real algebraic geometry, not from any general theorem about logic.

Without QE, deciding a first-order sentence might require searching through infinitely many models or proof sequences. QE collapses this search by providing a finite, syntactic translation to a quantifier-free form that can be evaluated algorithmically. The key insight is that the 'hard' part of logic — the quantifiers — can be removed for theories with sufficient algebraic structure.