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?
 A: 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.
A: According to Wikipedia, it is undecidable : 
"Unlike propositional logic, first-order logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no decision procedure that determines whether arbitrary formulas are logically valid. This result was established independently by Alonzo Church and Alan Turing in 1936 and 1937, respectively, giving a negative answer to the Entscheidungsproblem posed by David Hilbert in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the halting problem."
From http://en.wikipedia.org/wiki/First-order_logic
