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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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

Improve this answer
$\endgroup$
10
  • 3
    $\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
    Commented Jun 29, 2012 at 16:49
  • 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
    Commented Jun 30, 2012 at 10:01
  • 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
    Commented Jan 4, 2013 at 18:42
  • 1
    $\begingroup$ @D K: Decidability is not a property of a language, but of a theory. The theory of a binary predicate with no non-logical axioms is undecidable, whereas the theory of an empty binary predicate is decidable. The Wikipedia page is discussing the former, and no further requirements are needed there. $\endgroup$
    – Emil Jeřábek
    Commented Jan 4, 2013 at 18:55
  • 1
    $\begingroup$ In any case, Knuth–Bendix completion only deals with equations. The equational theory of groups is well-known to be decidable, using reduced words in usual descriptions of free groups. This does not imply anything about the first-order theory. $\endgroup$
    – Emil Jeřábek
    Commented Jan 4, 2013 at 18:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .