4
$\begingroup$

I've read first-order logic is in general undecidable, and that could be decidable only when working with unary operators. (I think that's propositional logic, correct me if I am wrong)

The question is why arity leads to undecidable problems?

I would like to see some reference material, or at least some simple example of it, as a way to think in this passage from unary to n-ary and why it leads to undecidable problems.

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ I am pretty sure any sort of logic is decidable; they are usually even context-free. I guess you mean the satisfiability or validity problem? $\endgroup$ – Raphael♦ Nov 5 '12 at 17:17
12
$\begingroup$

Logic with unary predicates (not operators), is called monadic. The thing that is called propositional logic only has nullary predicates, i.e., constants true and false, and no quantifiers.

The undecidability of predicate logic follows because predicate logic (with at least one binary predicate) is powerful enough to describe how a Turing machine works, and so we can express in the logic sufficiently complicated statements about Turing machines to get undecidability. In contrast, in monadic logic, where we only have unary predicates, we cannot describe the working of a Turing machine. I am being deliberately vague here to give an idea without getting bogged down in technicalities.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ thanks! +1, it's clearer now, I would like you to extend a little the "technicalities", to know if besides unary restriction there is another one about nesting or recursion, perhaps I still would like to see some examples of unary predicates versus n-ary ones. $\endgroup$ – Hernan_eche Nov 5 '12 at 18:13
  • 1
    $\begingroup$ No restriction regarding nesting or recursion. This is first-order logic, so you cannot "recurse" in any reasonable way. As far as unary examples go: "$n$ is a prime number", "$x$ is positive". Binary examples: "$x$ is less than $y$", "$n$ and $m$ are relatively prime", "$A$ is the mother of $B$". Ternary examples: "$A$ is between $B$ and $C$", "$A$ is a child of $B$ and $C$". $\endgroup$ – Andrej Bauer Nov 5 '12 at 18:56
1
$\begingroup$

As Raphael pointed in a comment you are probably asking about the decidability of the classical decision problem for fragments of first order logic with unary predicates.

The search of syntactically restricted fragments of first-order logic where validity of formulas is decidable was an active field of research for over 100 years. It was understood very early that it is the dependencies between variables that make the decision problem difficult. And dependencies are best expressed when two variables occur within the arguments of a predicate. Therefore binary predicates or functional symbols (if you allow functional symbols) are essential for undecidability.

It was Löwenheim who in 1915 gave a decision procedure for first-order logic with unary predicates. If you are interested, you might find intriguing an exposition paper titled "On the Classical Decision Problem" written by Yuri Gurevich in the form of a dialog of two fictitious characters. The paper was first published in the Bulletin of EATCS.

The paper not only introduces the problem but explains how the search developed into finding a complete classification of decidable and undecidable fragments in terms of quantifier prefixes.

|cite|improve this answer
$\endgroup$

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.