This is an old revision of the document!

Simple QE for Dense Linear Orders

Example of dense linear order: rational numbers with less-than relation. (It works in the same way for real numbers with less-than relation.)

Theory of Dense Linear Orders

Language ${\cal L} = \{ < \}$ . Atomic formulas are of two forms:

$x=y$
$x < y$

Literals are either atomic formulas or their negations.

Formulas $T$ are the formulas that are closed formulas that are true in the structure $(\mathbb{Q},<)$ or rational numbers.

Normal form of Formulas

We have seen that it suffices to eliminate quantifiers from conjunctions of literals.

Can we assume that literals are of a special form?

Example: simplify these formulas:

$x < y\ \land\ \lnot (y < z) \ \land\ (x \neq z)$
$x < y\ \land y < x$

If we have three concrete values for $x,y,z$ , what is the form of the strongest type of a formula that we could write about them in this language? (atomic type formula)

Theorem: every quantifier-free formula in a language with only relational symbols is a disjunction of atomic type formulas

if we know the set $T$ of axioms, we may be able to show that the atomic type formulas have a simple form

Quantifier Elimination Step

Quantifier elimination from atomic type formulas:

Quantifier elimination from more general formulas: