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.


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.

| cite | improve this answer | |
  • $\begingroup$ It is not clear to me what you mean by a partition of 1,...,n into intervals. In case you just mean the same than a partition of 1, ..., n (i.e., an equivalence relation on this set of natural numbers), then the answer to your question is not (see the addendum to my question). If you mean something different, then it is not so clear to me what you claim in the second part of your answer. Why do you think that you can codify this using only one equivalence relation? $\endgroup$ – boumol Jan 7 '11 at 17:15
  • $\begingroup$ A finite linear quasi-order is a relation $\le$ on $\{1,...,n\}$, satisfying $a\le b \& b\le c\to a\le c$, and $a\le a$.The associated partition is $a\sim b$ iff $a\le b$ and $b\le a$.Up to isomorphism,(i.e.up to renaming elements of the set) we can always assume that the partition classes are of the form $\{i,i+1,...,j\}$,that is each equiv. class is an interval. Conversely,each partition of $\{1,...,n\}$ into intervals gives unique quasi−order.Thus the theories of linear quasi−orders of finite sets and partitions of $\{1,...,n\}$ into intervals are elementary equivalent. $\endgroup$ – user6976 Jan 7 '11 at 17:27
  • $\begingroup$ You are totally right, my question can be stated talking about "partitions of {1,...,n} into intervals". But it is not so clear to me that you can codify these partitions using just one equivalence relation: the trouble is that the notion of interval is implicitly carrying some extra order relation. $\endgroup$ – boumol Jan 7 '11 at 17:40
  • $\begingroup$ I have added an update. $\endgroup$ – user6976 Jan 7 '11 at 20:40
  • $\begingroup$ Thanks for the explanation. Now I see how to get the decidability. $\endgroup$ – boumol Jan 8 '11 at 0:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.