Elementary Theory of Finite Linear QuasiOrders

2011-01-07T15:34:59Z

It is well known that the elementary theory $Q_{fin}$ of finite quasiorders is undecidable. To be more precise, it is undecidable whether a first-order sentence built using a binary relational symbol $R$ is valid in all finite structures where the interpretation of $R$ is reflexive and transitive. This was proved in

--- I. A. Lavrov. Effective inseparability of the sets of identically true formulae and finitely refutable formulae for certain theories. 1963. Algebra i Logika Sem. Vol 2, pp. 5-18. MR0157904 (28 #1132).

Indeed in this paper it is proved something stronger, namely, that the elementary theory $Q$ of quasiorders is effectively inseparable from $Q_{fin}$. This means that there is no recursive (i.e., decidable) set $X$ such that $Q \subseteq X \subseteq Q_{fin}$.
On the other hand, it is known in the literature that the elementary theory $L_{fin}$ of finite linear orders in decidable, and the same for the elementary theory $L$ of linear orders. The result concercing $L_{fin}$ can be proved using Ehrenfeucht–Fraïssé games.
The question I am interest on is about the (non-)decidability of the elementary theory $LQ_{fin}$ of finite linear quasiorders. Right now I am working on a completely different problem, and I have managed to get some reduction of my problem to $LQ_{fin}$ but I cannot find any information about this theory on the literature. To be more specific my question is.

Does anybody know whether $LQ_{fin}$ is undecidable? If this is case, is it known whether the elementary theory $LQ$ of linear quasiorders is effectively inseparable from $LQ_{fin}$?

Addendum: Let me clarify how finite linear quasiorders look like. They are exactly finite linear orders together with a function $f$ from this finite linear order into the set of positive (greater or equal than $1$) natural numbers. This number indicates the number of elements in the equivalence class corresponding to this point.

Answer by Mark Sapir for Elementary Theory of Finite Linear QuasiOrders

2011-01-07T16:50:53Z

A finite linear quasi-order is just a partition of $1,...,n$ into intervals? That elementary theory should be decidable. In general, the elementary theory of one equivalence relation on a finite set is decidable.

Update: A partition of ${1,...,n}$ into intervals is equivalent to the pair $(n,A)$ where $A$ is a subset of ${1,...,n}$ (the set of the initial numbers of the intervals). So it looks like your theory "embeds" into the theory of the linear orders with one nullary predicate. The solvability then should follow from Rabin's theorem of solvability of the first order monadic theory of trees ($\mathbb{N}$ can be considered as a "degenerate" tree): M. O. Rabin, Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc. 141 (1969), 1-35.

Elementary Theory of Finite Linear QuasiOrders - MathOverflow

Elementary Theory of Finite Linear QuasiOrders

Answer by Mark Sapir for Elementary Theory of Finite Linear QuasiOrders