« Section 1.7: Problem 9 Solution

Section 1.7: Problem 11 Solution »

Section 1.7: 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
Let be an effectively enumerable set of wffs. Assume that for each wff , either or . Show that the set of tautological consequences of is decidable.
(a) Do this where “or” is interpreted in the exclusive sense: either or but not both.
(b) Do this where “or” is interpreted in the inclusive sense: either or or both.
Given , we may want to first check whether it is a wff (Theorem 17B tells us that this is decidable). So, assume it is (otherwise return “no”).
(a) Let be the first entries produced by the procedure that enumerates , including . Here we assume that ’s are defined as long as the procedure returns at least elements (it may run forever after all of the elements of are listed). is always defined. Starting from we test whether or . If the answer of the first test is “yes” then we know that , if the answer of the second test is “yes” then we know that , otherwise we increase by and continue testing. According to the compactness theorem, if , then there is a finite subset of that also tautologically implies , in particular, every such that will tautologically imply , hence, our procedure will eventually return either “yes” or “no” (once we have enumerated all the members of for either or ). Also, importantly enough, if does not imply either or , then there is at least one element of which was not yet enumerated, and, therefore, the procedure will not stuck at finding . In particular, the very first step tests whether or is a tautology, and if not, then there is at least one element in . Alternatively, we could have just shown that must be infinite based on the assumption of (a).
(b) For any truth assignment that satisfies , and are opposite, hence, cannot satisfy both and . Therefore, we can be in one of the two following cases: either is not satisfiable at all, in which case all wffs are tautological consequences of , or is satisfiable and we are in the case of (a).
At first, I thought that the procedure should check whether is satisfiable, and if not, then return “yes” for any wff, and if yes, then run the procedure of (a). However, I was not able to think of a way to decide whether an infinite set is satisfiable in a finite amount of time. If by listing all members of we, at some point, find that a finite subset of is unsatisfiable, then so is , but as long as we get all finite subsets satisfiable, there seems to be no way to be sure that the whole is satisfiable without considering every its member. The simplest example . Having listed the first elements of , we can never be sure that, for example, the next element is not . Therefore, it seems that the set of all unsatisfiable sets of wffs is effectively enumerable, but its complement, the set of all satisfiable sets of wffs is not.
But then, I realized that we don’t need this. The thing is, that itself is not an input to the procedure we are looking for. is decidable as long as there is a procedure that can decide whether any expression is in or it is not. We are not required to know the procedure. In our case, all ’s as stated in (b) fall into two classes. The first class contains all unsatisfiable ’s, and for each of them the procedure that always return “yes” (as long as the input expression is a wff, as noted in the beginning) is the one that will always decide whether a wff is in such . The second class contains all ’s that are satisfiable and (a) holds. For these ’s the procedure described in (a) will decide for any wff whether it belongs to such or not. Therefore, every satisfying (b) is decidable, we just don’t know which of the two procedures is the one that works for this particular .
P.S. Later, reading the book, I found a similar argument on page 144 (the very last paragraph).