# Axiomatisation of the monadic second order theory of finite linear orders.

I am interested in whether there exists in the literature an axiomatisation of the (weak) monadic second order theory of finite linear orders, in the context of Henkin semantics.

There are various setups used to study the (weak) monadic second order theory of linear order, the most standard is probably to associate to each linear order $$\alpha$$ the $$\mathscr{L}=\{\in,<\}$$-structure $$M(\alpha) = (\mathcal{P}(\alpha),\alpha;\in,<)$$ (replacing $$\mathcal{P}(\alpha)$$ with the collection of finite subsets of $$\alpha$$ for the weak version), where $$\mathscr{L}$$ is a two-sorted language, $$\in$$ is the usual set-theoretic membership relation, and $$<$$ is the expected ordering on $$\alpha$$.

With this setup in mind, the theory I am interested in finding an axiomatisation for is $$\bigcap_{\alpha \in Fin} Th(M(\alpha))$$ where $$Fin$$ is the collection of finite linear orders. This theory is obviously not complete.

I already have in mind some candidate axioms, but proving that these generate the theory appears tricky. I would first like to see if this has been looked at in the literature. I am really only interested in an axiomatisation that works for Henkin semantics, rather than full/standard semantics. Note that under Henkin semantics this theory has non-standard models (i.e. models not of the form $$M(\alpha)$$ for some linear order $$\alpha$$, the proof is just by compactness), while under standard semantics there are no non-standard models (any non-standard model must be infinite, but then we have either the weak monadic or full monadic structure of an infinite linear order, and it is straightforward to give a sentence for each case, which is true in any non-standard model but false in any standard model).

Relevant is the result of Buchi and Siefkes. They gave an axiomatisation of the shared monadic second order theory of countable ordinals. The proof they use to justify their axiomatisation involves formalisation of a decision procedure which is grounded in automata theory. Since automata theory and its connection to the monadic second order logic of finite linear orders is so well studied, I feel like an axiomatisation must be somewhere in the literature, but I have not been able to find it.

Any references to this topic in the literature would be very helpful.