Quantifier elimination — dense linear orders

In certain special theories, every assertion is equivalent to a simple combination of atomic facts. Proving this for a given theory typically both requires and exhibits a complete mastery of it.

A theory admits quantifier-elimination when every assertion is logically equivalent over the theory to a quantifier-free assertion, a Boolean combination of atomic assertions. This is quite a remarkable property when it occurs, because it reveals a severe limitation on the range of concepts that can be expressed in the theory—a quantifier-free assertion, after all, is able to express only combinations of the immediate atomic facts at hand. We are therefore generally able to prove quantifier-elimination results for a theory only when we already have a profound understanding of the theory and its models, and the quantifier-elimination result itself usually leads quickly to a classification of the definable objects, sets, and relations, as well as to a decision procedure for truth in the theory itself. In this way, quantifier-elimination results often showcase our mastery over a particular theory and its models. So let us present in these next few posts a few quantifier-elimination results, exhibiting our expertise over some natural theories.

We shall begin with the theory of dense linear orders.

Enjoy this installment from A Panorama of Logic, an introduction to topics in logic for philosophers, mathematicians, and computer scientists. Fresh content each week.

Please consider subscribing as a free or paid subscriber.

Endless dense linear orders

Consider first the theory of an endless dense linear order, such as the rational order ⟨ℚ,<⟩. In light of our work in an earlier post, including Cantor’s categoricity theorem that every two countable endless dense linear orders are isomorphic, we already have a fairly deep understanding of this theory and this particular model.

Consider any two rational numbers x, y in the structure ⟨ℚ,<⟩. What can one say about them? Well, we can certainly make the atomic assertions that x < y or that x = y or that y < x. Remarkably, however, this is all that can be said—every assertion φ(x,y) in the language of orders, I claim, is equivalent in ⟨ℚ,<⟩ to a Boolean combination of these assertions.

Theorem. The theory of the rational order ⟨ℚ,<⟩ admits elimination of quantifiers—every assertion φ(x,...) is logically equivalent in the rational order to a quantifier-free assertion.