I struggle with understanding why the satisfiability in the first-order logic is undecidable. Could you explain it with some examples? I've also seen that satisfiability in some first-order formulas are decidable.

Please explain it with as much as many examples.

  • 1
    $\begingroup$ If you think any amount of example formulae can help you, you have not understood what "undecidable" means. I recommend you brush up on that first and revisit SAT on FO then. $\endgroup$ – Raphael Oct 6 '14 at 17:45

The fact that first-order logic (with some non-triviality constraints) is undecidable means that no algorithm can decide correctly whether a given first-order formula is true or not. However, for any single statement $\varphi$ it is easy to come up with an algorithm that decides $\varphi$ correctly (just hard-code the answer). So it is impossible to give examples of "undecidable statements", since there is no such thing.

What is possible is to give a restricted set of sentences whose truth value is already undecidable. In effect, this is what the proof of undecidability does. The proof shows that you can encode the statement "the Turing machine $T$ halts on empty input" in first-order logic (again, given some mild non-triviality constraints), so this infinite sequence of statement is already undecidable, that is, no algorithm can correctly decide whether such a formula is true or not.

  • $\begingroup$ so why is the propositional logic decidable? $\endgroup$ – Eliza Oct 6 '14 at 19:52
  • $\begingroup$ Because propositional logic doesnt have the power to encode such statement @Eliza $\endgroup$ – Jonas Gomes Oct 6 '14 at 21:14

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.