Section 2.6: Problem 10 Solution
Working problems is a crucial part of learning mathematics. No one can learn... merely by poring over the definitions, theorems, and examples that are worked out in the text. One must work part of it out for oneself. To provide that opportunity is the purpose of the exercises.
James R. Munkres
Assume we have a finite language without function symbols.
(a) Show that the set of satisfiable sentences is decidable. (See Exercise 19 in Section 2.2 for terminology and background.) Suggestion: Apply the preceding exercise.
(b) Show that the set of valid sentences is decidable. (A formula is one of the form where is quantifier-free.)
Remarks: In first-order logic, the “decision problem” (Entscheidungsproblem) is the problem of deciding, given a formula, whether or not it is valid. By Church’s theorem (Section 3.5), this problem in general is unsolvable. This exercise gives a solvable subcase of the decision problem.
(a) By Exercise 19 of Section 2.2, we know that an sentence is satisfiable iff it is satisfiable in a finite model. And by the preceding exercise, for any sentence we can decide whether it has any models at all, i.e. whether it is satisfiable.
(b) is a valid sentence iff , which is an sentence, is not satisfiable. By (a), we can decide whether it is the case, or not.