Satisfiability problem for FOL[<,R]

Let FOL[<,R] be the fragment of first-order logic enriched with two relational symbols < and R and the first-order axioms that say:

< is a strict partial order and R is an irreflexive and symmetric binary relation

Does anyone know whether the satisfiability problem is undecidable in this case? Any similar result?

The satisfiability problem is not decidable in your case, even if you restrict to have only one of those relations (either one). This amounts basically to the fact that both the theory of partial orders and the theory of graphs are undecidable. A sketch of the proof of these facts would follow the outline: (1) the standard model of arithmetic is what is called a strongly undecidable structure, meaning that every theory that it satisfies is undecidable; (2) if $N$ is strongly undecidable and definable inside another structure $M$, then $M$ is also strongly undecidable; and (3) the standard model of arithmetic is definable inside a partial order, and also inside a graph. Thus, the theory of partial orders is not decidable, and neither is the theory of graphs.
One can think about it like this: if you could decide the theory of graphs, then you could decide the consequences of Robinson's theory $Q$, by interpreting arithmetic inside graph theory via the encoding. But you can't decide the consequences of $Q$, contradiction.
• The theory of partial orders is the theory whose axioms state that $\lt$ is a partial order. This theory is undecidable, meaning that there is no computable algorithm to decide whether $\varphi$ is a theorem, or equivalently, whether $\neg\varphi$ is satisfiable. I'd have to think more about it to determine whether you need $=$ in the language for this, but I believe that you don't. The concept of a strongly undecidable structure seems to be treated in many of the usual logic books. This is the easiest way to show that group theory is undecidable, ring theory, theory of graphs, etc. etc. – Joel David Hamkins Jun 30 '12 at 10:01
• Group theory is as incomplete as it gets. To begin with, any two nonisomorphic finite groups have a different first-order theory. In fact, it has a plenty of equationally axiomatized proper extensions, such as abelian groups, or class $k$ nilpotent groups for a fixed $k$. Moreover, since Tarski has shown that the standard model of arithmetic is interpretable in a group, group theory has a finitely axiomatized essentially undecidable extension. On the other hand, it also has nontrivial decidable extensions, such as abelian groups. – Emil Jeřábek Jan 4 '13 at 18:42