Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
Isn't the theory of partial orderings undecidable by itself? And adding a second predicate only makes things worse? –  mjqxxxx Jun 29 '12 at 17:39

1 Answer 1

up vote 1 down vote accepted

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.

share|improve this answer
    
Thank you very much for your exhaustive answer. –  Alberto Jun 30 '12 at 8:04

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.