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: Take a model $\mathfrak M$ for NBG set theory, and interpret your new symbols as:


*

*$a<b$ iff there is a chain $a=x_1\in x_2\in\cdots\in x_n=b$ with $n\ge 2$.

*$a\mathrel R b$ iff $a\in b$ or $b\in a$.


Then $(|\mathfrak M|,{<},R)$ is automatically a model for your theory, and $a\in b$ exactly when $(a<b) \land (a\mathrel R b)$.
Therefore you can express any sentence in the language of set theory in your language by representing each $a\in b$ as $(a<b)\land (a\mathrel R b)$. Now, since NBG is finitely axiomatizable, you can find out whether some set-theoretical sentence $\phi$ is provable from NBG by asking whether $NBG \land \neg \phi$ is satisfiable. But it is well known that provability in set theory is undecidable.

Edit: As mjqxxxx points out, simply having $<$ is enough to establish undecidability. One can see this by a slightly more involved translation from the language of set theory to the language of partial orders:


*

*"$a$ is an immediate successor of $b$" means that $b<a$ and there is no $c$ such that $b<c<a$.

*Define a "link" to mean an element that has exactly one immediate successor.

*Let "$a\in b$" mean that there exists a link $c$ such that $c$ is an immediate successor of $a$ and $b$ is the immediate successor of $c$.

*When translating a set-theoretic sentence, restrict all quantifiers to range over elements that are not links.


In the other direction, if we start from a model of set theory, every set/class becomes an element of the partial order, and every pair $(a\in b)$ in the membership relation becomes a link element. (An element that represents a set is not a "link" because every set is a member of more than one other set, so the element has more than one immediate successor, and an element that represents a proper class is not a "link" because it will have no successors at all).
Edit even more: The above constructions depend on the fact that the axioms of set theory guarantee that $\in$ is acyclic (and thus its transitive closure is a strict partial order). However, using more of the same techniques one can also represent an arbitrary predicate calculus as statements about a partial order. Then we don't need to depend on specific knowledge of axiomatic set theory, only that predicate calculus in general is undecidable.
