When less is more — simplifying the logical landscape
Some theories let you erase every "there exists" and "for all" and lose nothing. Watch formulas about orders and polynomials shrink to plain conditions you can check at a glance.
Pick a formula about the order, then press Next Step to eliminate its quantifier. Compare the original and current forms side by side until no quantifier is left.
Choose a formula about a dense linear order and step through the elimination process.
Start with the original formula
∃y (x < y ∧ y < z)
The quantifier ∃y asks: is there an element between x and z?
∃y (x < y ∧ y < z)
By density of DLO: between any two ordered elements, there exists another
x < z → ∃y (x < y ∧ y < z)
The existential is equivalent to the order condition on the free variables
x < z
A theory T has quantifier elimination (QE) if every first-order formula is equivalent, modulo T, to a quantifier-free formula. This is an extraordinarily powerful property: it means that every definable set is a Boolean combination of atomic formulas, making the "geometry" of the theory completely transparent.
The theory of dense linear orders without endpoints (DLO) has QE: the key idea is that between any two elements there is always another, and there is no first or last element. These axioms are strong enough to eliminate every quantifier. The theory of algebraically closed fields (ACF) of a given characteristic also has QE, by Chevalley's theorem. Tarski proved that real closed fields have QE as well.
When a theory has QE, questions about arbitrary first-order definable sets reduce to questions about atomic formulas -- equalities, inequalities, and polynomial conditions. This makes decidability, definability, and geometric reasoning dramatically simpler.
Key insight: In DLO, every quantifier can be eliminated because the density axiom (between any two elements there is another) and the no-endpoints axiom provide enough flexibility to rewrite quantified formulas as quantifier-free conditions on the remaining variables.
Choose a linear, quadratic, or cubic equation, set its coefficients with the sliders, and step through the elimination. Notice that the final condition mentions only the coefficients.
Choose a polynomial equation and watch the quantifier elimination process. Then experiment with coefficients to see which parameter values yield solutions.
Start with the existential formula
∃x (ax² + bx + c = 0)
Case split on leading coefficient a
(a ≠ 0 ∧ ∃x(...)) ∨ (a = 0 ∧ ∃x(bx + c = 0))
If a ≠ 0: polynomial is quadratic, so in ACF it always has a root
(a ≠ 0) ∨ (a = 0 ∧ ∃x(bx + c = 0))
If a = 0 and b ≠ 0: linear, has root x = -c/b
(a ≠ 0) ∨ (a = 0 ∧ b ≠ 0) ∨ (a = 0 ∧ b = 0 ∧ c = 0)
Final quantifier-free form
a ≠ 0 ∨ b ≠ 0 ∨ c = 0
QE result: a ≠ 0 ∨ b ≠ 0 ∨ c = 0 → 1 ≠ 0 ∨ 0 ≠ 0 ∨ -1 = 0 → True
Key insight: In ACF, the existence of roots is guaranteed by the axioms. The formula ∃x(ax² + bx + c = 0) does not need a discriminant test -- it simplifies to the condition that the polynomial is non-trivial, because every non-constant polynomial over an algebraically closed field has a root.
Switch between Quantifier-Free Definable and First-Order Definable for each theory. Highlighted sets need quantifiers; in theories with QE, the two lists match.
Compare quantifier-free definable sets with first-order definable sets across theories. For theories with QE, these classes are identical.
The theory of dense linear orders without endpoints, such as (ℚ, <).
The theory of algebraically closed fields (e.g., ℂ), in a given characteristic.
The theory of real closed fields, such as (ℝ, +, ×, <, 0, 1).
The theory of (ℤ, +, 0, 1, <) -- integers with addition but not multiplication.
Key insight: Quantifier elimination collapses the hierarchy of definable sets. Without QE, adding quantifiers can define genuinely new sets. With QE, the quantifier-free formulas already capture everything first-order logic can express, making the definable sets transparent and tractable.
Spot a mistake or have an idea?