Forever Undecided

by Raymond M. Smullyan

  Thus we have proved that every reasoner x of U2 believes (Np&N(p⊃q))⊃Nq, and so this proposition is established.

  (3) Last, we must show that if p is established, so is Np. (This does not mean that every reasoner who believes p will also believe Np, but only that if all reasoners believe p, then they all believe Np.) This is really quite obvious. Suppose all reasoners believe p. Take any reasoner x. Then his parents believe p (because all the reasoners do), hence x believes Np.

  2. The importance of the change from “parents” to “ancestors” is this: If y is a parent of x, and z is a parent of y, we can hardly conclude that z is a parent of x. But if y is an ancestor of x, and z is an ancestor of y, then z is an ancestor of x. (In mathematical terminology, the relation of being an ancestor is transitive.)

  The proof that the set of established propositions of the universe U2 is of type 3 is the same as for the last universe U1 (just changing the word “parent” to “ancestor”). But now we can prove the additional fact that every reasoner of this universe believes Np⊃NNp, and hence that the set of established propositions is of type 4.

  Suppose x believes Np. We are to show that he must also believe NNp. Well, let x′ be any ancestor of x and let x″ be any ancestor of x′. Then x″ is also an ancestor of x. Since x believes Np and x″ is an ancestor of x, then x″ must believe p. Thus every ancestor x″ of x′ believes p, hence x′ believes Np. This shows that every ancestor x′ of x believes Np, and so x must believe NNp.

  3. First, to prove the lemma, suppose x disbelieves Np. Then he must have at least one ancestor x′ who disbelieves p (because if all his ancestors believed p, he would believe Np, which he doesn’t). Now, if x′ believes Np, we are done—we take y to be x′. But if x′ doesn’t believe Np, then he disbelieves Np, hence x′ must have at least one ancestor x″ who disbelieves p. If x″ believes Np, we are done (we take y to be x″). But if not, then we take some ancestor x″′ of x″ who disbelieves p, and we keep on going in this manner until we finally must reach some ancestor y of x who disbelieves p and who either has no ancestors at all (in which case y believes Np by Fact 1), or who does have ancestors all of whom believe p—and hence y must believe Np. (The reason we must finally reach such an ancestor y is because the universe U3 had a definite beginning in time—a fact not given for the universe U2!)

  Now we can prove that all reasoners of this universe must believe N(Np⊃p)⊃Np (and hence that the set of established propositions is of type G). To prove this, it suffices to show that every reasoner who believes N(Np⊃p) will believe Np; or, what is the same thing, any reasoner who disbelieves Np will also disbelieve N(Np⊃p).

  And so suppose that x disbelieves Np. Then by the lemma, x has an ancestor y who disbelieves p and believes Np. Then he believes Np true and p false, so he must disbelieve Np⊃p. Therefore x has an ancestor y who disbelieves Np⊃p, hence not all of x’s ancestors believe Np⊃p, so x must disbelieve N(Np⊃p).

  This proves that if x disbelieves Np, he disbelieves N(Np⊃p), hence if x believes N(Np⊃p), he must believe Np, and therefore x must believe N(Np⊃p)⊃Np.

  • 23 •

  Possible Worlds

  THE SUBJECT of modal logic is an ancient one—it goes back at least to Aristotle. The principal notions are that of a proposition being necessarily true and a proposition being possibly true. Either notion can be defined in terms of the other. If we start with the notion of necessary truth, we would define a proposition to be possibly true if it is not necessarily false. Alternatively, we could start out with the notion of a proposition being possibly true, and then define a proposition to be necessarily true if it is not possible that it is false.

  Model logic exercised considerable interest among the medieval philosophers and theologians and was later fundamental in the philosophy of Leibniz. It was Leibniz’s thought that inspired the contemporary philosopher Saul Kripke to invent the field known today as possible world semantics, also called Kripke semantics (which is what we worked on in the last chapter, using a different terminology).

  Leibniz had the idea that we inhabit a place called the actual world, which is only one of a number of possible worlds. According to Leibniz’s theology, God first looked over all possible worlds and then actualized the one he thought best—this world. Hence his dictum: “This is the best of all possible worlds.” (In Candide, Voltaire continually poked fun at this idea. After describing just about every possible catastrophe, Voltaire would always add “—in this best of all possible worlds.”)

  To continue with Leibniz, a proposition p was to be thought of as true for or in a given world x (whether actual or possible) if it correctly described that world, and false for that world if it didn’t. If p was called true without qualification, it was to be understood as meaning true for this (the actual) world. He called p necessarily true if it was true for all possible worlds, and possibly true if it was true for at least one possible world. Such—in brief—was the “possible world” philosophy of Leibniz. (If some other possible world had been actualized, I wonder if Leibniz would have had the same philosophy?)

  Prior to 1910, the treatment of modal logic lacked the precision of other branches of logic. Even Aristotle, who was eminently clear in his theory of the syllogism, did not give an equally clear account of modal logic. It was the American philosopher C. I. Lewis who, in a series of papers published between 1910 and 1920, described a sequence of axiom systems of different strengths and investigated what propositions are provable in each. In each of these systems, all tautologies are among the axioms (or at least provable from them), and for any propositions p and q, Lewis took it as a rule that if p and p⊃q are both provable in the system, so is q. Thus all of Lewis’s systems are at least of type 1. Next, Lewis reasoned that if p and p⊃q are both necessarily true, so is q. Hence all propositions of the form (Np&N(p⊃q))⊃Nq (or alternatively, all propositions of the form N(p⊃q)⊃(Np⊃Nq)) were taken as axioms. Next, it seemed reasonable that anything that could be proved purely on the basis of necessarily true axioms must be necessarily true, and today most modal systems (the so-called normal ones) take it as a rule of inference that if a proposition X has been proved, then we are justified in concluding NX. (This does not mean that X⊃NX is necessarily true, but that if X has been proved—purely on the basis of axioms that themselves are necessarily true—then we are justified in claiming NX.)

  The system that we have described so far is of type 3 and has a standard name these days. It is called the modal system K, and is the basis of a wide class of modal systems.

  Now, what about NX⊃NNX? (If X is necessarily true, is it necessary that it is necessarily true?) Well, propositions of this form are taken as axioms in some modal systems and not in others. The modal system whose axioms are those of K together with all propositions of the form NX⊃NNX is a very important one and is these days called the modal system K4. It is obviously of type 4.

  The modal system G—which consists of K4 with the addition of all propositions of the form N(Np⊃p)⊃Np as axioms—came only decades later (in the mid-seventies) and did not arise out of any philosophical considerations of the notion of logical necessity, but out of Gödel’s Second Theorem and Löb’s Theorem. More about that in the next chapter.

  Kripke Models. In the late 1950s, Saul Kripke published his famous paper, A Completeness Theorem in Modal Logic, which ushered in a new era for modal logic. For the first time a precise model theory was given for modal systems, which was not only of mathematical interest but which has led to a whole branch of philosophy known today as possible world semantics.

  Kripke first raised a basic question about Leibniz’s system that Leibniz evidently did not consider. According to Leibniz, we inhabit the actual world. Are the so-called possible worlds all the worlds that there are, or are they only those that are possible relative to this world? In other words, from the viewpoint of another world, is the class of possible worlds different from the class of worlds that are possible relative to this one? Or,
to put the matter still another way, suppose we give a description of some world x, and we consider the proposition “x is a possible world.” Is the truth or falsity of that proposition something absolute, or could it be that that very proposition is true in some world y but false in some other world z? Of particular importance here is the transitivity question: If world y is possible relative to world x and if world z is possible relative to world y, does it follow that world z must be possible relative to world x? The answer to that question determines which system of modal logic is appropriate.

  Following Kripke, we shall say that world y is accessible to world x if y is possible relative to x. And now let us consider a “super-universe” of possible worlds. Given any worlds x and y, either y is accessible to x or it isn’t. Once it is determined which worlds are accessible to which, we have what is technically called a frame. Given any proposition p and any world x, p is either true in x or false in x. And once it is determined which propositions are true in which worlds of the frame, we have what is called a Kripke model. It is to be understood that ⊥ is false in each of the worlds and that p⊃q is true in world x if and only if it is not the case that p is true in x and q is false in x. Thus, for each world x, the set of all propositions true in x is of type 1. To complete the description, a proposition Np is declared true in world x if and only if p is true in all worlds accessible to x. We will say that p is established in a model, or holds in a model, if p is true in all the worlds of the model.

  The setup we now have is really the same as that of the last chapter, except for terminology. Instead of the elements of the universe being called reasoners, they are now called worlds. In place of the relation “y is a parent of x,” or “y is an ancestor of x,” we now say “y is accessible to x.” Finally, in place of “p is believed by reasoner x,” we now have “p is true in world x.” With these transformations, all the results of the last chapter carry over. The set of all propositions that hold in a Kripke model must be of type 3 (Problem 1, Chapter 22), and hence the modal system K is applicable to all Kripke models.

  Suppose we now add the transitivity condition—for any worlds x, y, and z, if y is accessible to x and z is accessible to y, then z is accessible to x. We then have what is called a transitive Kripke model. Well, for any transitive Kripke model, the set of all propositions that are true for all worlds of the model must be of type 4 (Problem 2, Chapter 22), and so the appropriate modal system is then applicable.

  Thus the modal system K is applicable for all Kripke models, and the modal system K4 is applicable to all transitive Kripke models. These two results are known as the semantical soundness theorems for K and K4. Kripke also proved their converses: (1) If p holds in all Kripke models, then p is actually provable in the modal system K. (2) If p holds in all transitive Kripke models, then p is provable in K4. (We will later explain exactly what is meant by provability in a modal system.) These two results are known as the completeness theorems for K and K4.

  Let us say that a Kripke model is terminal if the following condition holds: Given any world x of the model, if we pass to a world x′ accessible to x and then to a world x″ accessible to x′, and keep going, we must finally reach a world y to which no worlds are accessible (so-called terminal worlds, which behave like the parentless reasoners of the last chapter). We shall say that a model is of type G if it is transitive and terminal. By the same reasoning as that of the last chapter, we see that the class of propositions that hold in a model of type G must be of type G, and hence the appropriate modal system is the modal system G. We thus get the so-called soundness theorem for the modal system G: Every proposition provable in G holds in all transitive terminal models. The converse of this—the completeness theorem for G—has also been established by the logician Krister Segerberg. It says that all propositions that hold in all models of type G are provable in the modal system G.†

  As a philosophical analysis of the notion of necessity, the modal system G seems most inappropriate. Its real importance lies in the provability interpretation, which we will discuss in the next chapter.

  Lewis’s System S4. Lewis had several other systems of modal logic, one of which we will briefly mention. Lewis reasoned that any proposition that is necessarily true must also be true. (In Leibniz’s terms, if a proposition is true in all possible worlds, it should certainly be true in this one!) And so Lewis added as axioms to K4 all propositions of the form NX⊃X. This is known as the modal system S4.

  The appropriate model theory for S4 is a transitive Kripke model (but not a terminal one!) with the added condition that every world is accessible to itself. It is then easy to see that NX⊃X holds in such a model.

  The modal systems S4 and G form a genuine parting of the ways. It is impossible to combine the two systems into a single system without getting an inconsistent system (can the reader see why?). And so we must make a choice, depending on our purpose. As a philosophical analysis of the notion of necessary truth, the system S4 seems the appropriate one. For proof theory, the system G is the important one. But more of this in the next chapter.

  Exercise 1. Why is it impossible to combine the systems G and S4 without getting an inconsistency?

  Exercise 2. In a model of type G, no world can be accessible to itself. Why is this?

  Exercise 3. Prove that in a model of type G, there is at least one proposition p and at least one world x such that the proposition Np⊃p is false in world x.

  Exercise 4. Is the following true or false? In a Kripke model of type G, there is at least one world in which the crazy proposition N⊥ (⊥ is necessarily true) is actually true.

  * * *

  †The proofs of the completeness theorems for the modal logics K, K4, and G can be found in George Boolos, The Unprovability of Consistency (Cambridge University Press, 1979), and a greatly simplified proof for G can be found in George Boolos and Richard C. Jeffrey, Computability and Logic (Cambridge University Press, 1980; second edition).

  • 24 •

  From Necessity to Provability

  THE NEXT important development in modal logic after Kripke’s modal semantics occurred in the early 1970s, when the provability interpretation was given to the word “necessary.” It is surprising that this did not catch on generally sooner, since Gödel suggested it in a very short paper published in 1933. Gödel used the symbol “B” in place of Lewis’s “N,” and suggested that Bp be interpreted as p is provable (in the system of Arithmetic, or in any of the closely related systems investigated by Gödel). Now, these systems are all of type 4, and so the axioms of K4 are all correct under that interpretation. However, the mathematical systems under investigation turned out to be even of type G (as discovered by Löb), hence it was only natural to invent a modal axiom system to take care of them. Thus the modal system G was born. It has been studied by several logicians, including Claudio Bernardi, George Boolos, D. H. J. de Jongh, Roberto Magari, Franco Montagna, Giovanni Sambin, Krister Segerberg, C. Smorynski, and Robert Solovay. Research concerning this system is still going on.

  At this point, it will help to discuss modal axiom systems more rigorously. The symbolism of modal logic is that of propositional logic, with one new symbol added—we shall take this symbol to be “B.” (We recall that Lewis used the symbol “N,” and the more standard symbol these days is “.” But I prefer to use Gödel’s symbol “B.”)

  By a modal formula—more briefly, a formula—we mean any expression formed according to the following rules:

  (1) ⊥ is a formula and each of the propositional variables p, q, r,…is a formula.

  (2) If X and Y are formulas, so is (X⊃Y).

  (3) If X is a formula, so is BX.

  What we called in Chapter 6 (this page) a formula could now be called a propositional formula. A propositional formula is a special case of a modal formula; it is one in which the symbol B does not occur. But we will be concerned from now on with modal formulas, and these will be called simply formulas.

  The logical connectives
~, &, v, ⊃, ≡ are defined from ⊃ and ⊥ in the manner explained in Chapter 8.

  Each modal system has its own axioms. In each of the modal systems that we will consider, one starts from the axioms and successively proves new formulas by use of the following two rules:

  Rule 1 (known as modus ponens). Having proved X and (X⊃Y), we can infer Y.

  Rule 2 (known as necessitation). Having proved X, we can infer BX.

  By a formal proof in the system is meant a finite sequence of formulas (usually displayed vertically and read downward), called the lines of the proof, such that each line is an axiom of the system, or it comes from two earlier lines of the proof by Rule 1, or it comes from one earlier line of the proof by Rule 2. A formula X is called provable in the system if there is a formal proof whose last line is X.

  The three systems that particularly interest us are the systems K, K4, and G, whose axioms we review below.

  Axioms of K: (1) All tautologies.

  (2) All formulas of the form B(X⊃Y)⊃(BX⊃BY).

  Axioms of K4: Those of K together with

  (3) All formulas of the form BX⊃BBX.

  Axioms of G: Those of K4 together with

  (4) All formulas of the form B(BX⊃X)⊃BX.

  Remarks. Let us refer to the axioms of group (4) as the special axioms of G. We recall the Kripke-de Jongh-Sambin theorem of Chapter 18, which is that if a system of type 3 can prove all sentences of the form B(BX⊃X)⊃BX, then it can also prove all sentences of the form BX⊃BBX. Thus we could have alternatively taken as our axioms for G those of groups (1), (2), and (4); the formulas of group (3) would then have been derivable. In other words, if we add the axioms of (4) to those of K, rather than K4, we would still get the full modal system G. The system G is often presented in this alternative manner.