patternModerate
First-order logic arity defines decidability?
Viewed 0 times
orderdefineslogicfirstdecidabilityarity
Problem
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.
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.
Solution
Logic with unary predicates (not operators), is called monadic. The thing that is called propositional logic only has nullary predicates, i.e., constants
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.
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.
Context
StackExchange Computer Science Q#6488, answer score: 12
Revisions (0)
No revisions yet.