First-order logic arity defines decidability?

Question

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.

Answer 1

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.

Answer 2

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.