A theory has quantifier elimination when every first-order formula is equivalent modulo to a quantifier-free formula with the same free variables.
Use the partial-isomorphism criterion for quantifier elimination: it is enough that every finite partial embedding between sufficiently saturated models have the one-point extension property.
Let be a finite partial order isomorphism between models of the theory of dense linear order without endpoints, and take . The finite set partitions into the points of , the intervals between consecutive elements, and the two outer rays. The order relations between and identify one of those intervals or rays. The image determines the corresponding interval or ray in . Density supplies a point there when it is bounded, and the absence of endpoints supplies one in either outer ray. Choose such a point ; then remains a partial order isomorphism.
The same argument works in the reverse direction. A back-and-forth method therefore extends finite partial order isomorphisms, making them partial elementary. The criterion proves quantifier elimination for dense linear orders without endpoints.

Articles by others on the same topic (0)

There are currently no matching articles.