Use the finite-partial-isomorphism criterion for quantifier elimination. Let and let be an isomorphism between finite suborders. For , its position relative to is one of the finitely many open intervals determined by , or one of the two exterior rays. The corresponding interval or ray determined by is nonempty because the orders are dense and have no endpoints. Choose there. Then remains a partial order isomorphism.
The same argument extends in the other direction. The back-and-forth method criterion therefore applies, proving quantifier elimination for dense linear orders without endpoints. Hence DLO eliminates quantifiers.
Articles by others on the same topic
There are currently no matching articles.