My colleague Matthias Baaz is looking for a reference for the following question (or possibly theorem):
Let T be the "theory of pairs of finite linear orders". That is, consider all finite structures $(X, R, S)$ where $R$ and $S$ are linear orders on $X$. Let T be the set of all first order formulas (in the language $=, R, S$) which are valid in all those (finite) models.
Clearly T is $\Pi^0_1$. Is T undecidable (or even $\Pi^0_1$-complete, as in Trakhtenbrot's theorem)? This should be well known.
