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?


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.


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

  • 2
    $\begingroup$ +1. But this doesn't actually answer the question, since the OP asked not about naked binary relations, but about binary relations that satisfied some additional properties. In general, this can affect the answer, because one could ask about decidability of a binary relation satisfying a property that makes it trivial (for example, perhaps it always holds, or never), and the corresponding theory will be decidable. $\endgroup$ – Joel David Hamkins Jun 29 '12 at 16:49
  • $\begingroup$ Thank you very much Joel. Your answer holds also if I don't have equality but only the two relational symbols I mentioned? I.e. what do you mean by "theory of partial orders"? Any reference for the proofs in detail? I actually have to modify the argument because in my case I want to consider a further restriction of FOL[<,R]. $\endgroup$ – Alberto Jun 30 '12 at 8:12
  • 2
    $\begingroup$ The theory of partial orders is the theory whose axioms state that $\lt$ is a partial order. This theory is undecidable, meaning that there is no computable algorithm to decide whether $\varphi$ is a theorem, or equivalently, whether $\neg\varphi$ is satisfiable. I'd have to think more about it to determine whether you need $=$ in the language for this, but I believe that you don't. The concept of a strongly undecidable structure seems to be treated in many of the usual logic books. This is the easiest way to show that group theory is undecidable, ring theory, theory of graphs, etc. etc. $\endgroup$ – Joel David Hamkins Jun 30 '12 at 10:01
  • $\begingroup$ I thought the wikipedia quotation was sufficient, because it states that as long as the binary predicate is not equality, it renders the theory undecidable. But you're right, the trivial empty predicate does not have this property, so there should be another requirement of "non-triviality" on the wikipedia page. $\endgroup$ – Denis Jul 3 '12 at 14:24
  • 1
    $\begingroup$ Group theory is as incomplete as it gets. To begin with, any two nonisomorphic finite groups have a different first-order theory. In fact, it has a plenty of equationally axiomatized proper extensions, such as abelian groups, or class $k$ nilpotent groups for a fixed $k$. Moreover, since Tarski has shown that the standard model of arithmetic is interpretable in a group, group theory has a finitely axiomatized essentially undecidable extension. On the other hand, it also has nontrivial decidable extensions, such as abelian groups. $\endgroup$ – Emil Jeřábek Jan 4 '13 at 18:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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