Model-completeness for a dense linear order in weak monadic second order logic

TL;DR

This paper provides a simplified proof of model-completeness for a dense linear order in weak monadic second order logic and applies it to the lattice of finite unions of closed intervals in o-minimal structures.

Contribution

It offers a streamlined proof of model-completeness for a specific dense linear order and extends this to the lattice of closed definable subsets in o-minimal structures.

Findings

Proof of model-completeness for the weak monadic second order version of a dense linear order.

Establishment of model-completeness for the lattice of finite unions of closed intervals.

Simplification of the logical framework needed for these proofs.

Abstract

We present a streamlined and (hopefully) accessible proof of the model-completeness of the weak monadic second order version of a dense linear order with left-endpoint but no right-endpoint in a particular finite signature. We also show how this can be used to establish model-completeness of the lattice of finite unions of closed intervals of a dense linear order, i.e. the lattice of closed definable subsets in a (densely ordered) o-minimal structure, in a particularly simple signature (comprising binary functions for union and intersection together with two constant symbols and four unary function symbols).