## Return to Question

3 added 337 characters in body
1. 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}$.

2. 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.

3. 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.

2 edited body
1. 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}$.

2. 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.