1
$\begingroup$

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?

  • 0
    Isn't the theory of partial orderings undecidable by itself? And adding a second predicate only makes things worse?2012-06-29

1 Answers 1

1

Take a model $\mathfrak M$ for NBG set theory, and interpret your new symbols as:

  • $a 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.

Therefore you can express any sentence in the language of set theory in your language by representing each $a\in b$ as $(a. 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 and there is no $c$ such that $b.
  • 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.

  • 0
    Thank $y$ou very much for your exhaustive answer.2012-06-30