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?



Satisfiability problem for FOL[<,R]
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.


