This paper continues earlier work and extends it to an intuitionistic setting. Kripke frames are used to semantically define a family of intuitionisticlike logics for which the "local" part of the truth definition is supplied by manyvalued logics whose semantics are algebraically simple and natural. A uniform tableau system is given and soundness and completeness are proved. The tableau connection entails that the semantic family collectively determines just four logics, intuitionistic logic itself, and intuitionistic-like versions of FDE, K3, and LP. These, apparently, are new logics, and are of natural interest. For instance, all have the disjunction property, and standard double negation embeddings are applicable. In addition, intuitionistic analogues of ST (strict-tolerant logic) and TS (tolerant-strict) logics are defined, and shown to have the same relationships to intuitionistic logic that the usual ST and TS have to classical logic.

Consider those many-valued logic models in which the truth values are a lattice that supplies interpretations for the logical connectives of conjunction and disjunction, and which has a De Morgan involution supplying an interpretation for negation. Assume that the set of designated truth values is a prime filter in the lattice. Each of these structures determines a simple many-valued logic. We show that there is a single Smullyan-style signed tableau system appropriate for all of the logics these structures determine. Differences between the logics are confined entirely to tableau branch closure rules. Completeness, soundness, and interpolation can be proved in a uniform way for all cases. Since branch closure rules have a limited number of variations, in fact all the semantic structures determine just four different logics, all well-known ones. Asymmetric logics such as strict/tolerant, ST , also share all the same tableau rules, but differ in what constitutes an initial tableau. It is also possible to capture the notion of antivalidity using the same set of tableau rules. Thus a simple set of tableau rules serves as a unifying and classifying device for a natural and simple family of many-valued logics.

Saul Aaron Kripke, the most influential philosopher and logician of his generation, died on September 15, 2022, at the age of 81.

We have used phrases like “the King of France” or “the tallest person in the world” several times, though we always treated them like non-rigid constant symbols. But such phrases have more structure than constant symbols—they do not arbitrarily designate. The King of France, for instance, has the property of being King of France, provided there is one, and the phrase “the King of France” designates him because he alone has that property. Phrases of the form “the so-and-so” are called definite descriptions. In this chapter we examine the behavior of definite descriptions in modal contexts.

Logics are generally specified in two fundamentally different ways, using proofs and using models. Both are important, and the two are intimately connected.

For analytic philosophy, formalization is a fundamental tool for clarifying language, leading to better understanding of thoughts expressed through language. Formalization involves abstraction and idealization. This is true in the sciences as well as in philosophy.

Historically, most of the best-known modal logics had axiomatic characterizations long before either tableau systems or semantical approaches were available. While early modal axiom systems were somewhat circuitous by today’s standards, a natural and elegant system for $$\mathbf {S4}$$ was given in Gödel (1933), and this has become the paradigm for axiomatizing modal logics ever since. It is how we do things here.

We discussed equality at length in Chap. 11 , but this was before we introduced the machinery of predicate abstraction. Recall that a model is normal if the relation symbol “=” is interpreted to be the equality relation on the domain of the model. The relation is thus the same from world to world. Now it is time to see how equality and predicate abstraction interact. While the basics of what we have to say applies to non-rigid terms generally, things are most easily understood if function symbols are not present, and that is all we discuss formally in this section. Our setting throughout this section can be assumed to be the modal logic K, with varying domains, allowing terms that may not designate, that is, K with the VN conditions. This is the most general setting we have, since all other setups are the result of putting further restrictions on this one.

We have seen several soundness and completeness proofs so far. And we have just introduced four more tableau systems in need of such proofs. For each of the modal logics from the Lesser Modal Cube, Fig. 7.1 , we have a quantified version that is constant domain and a quantified version that is varying domain. For each of these we have versions with and without equality. And we have predicate abstract extensions for which terms always designate and extensions for which terms might not designate. Rather than give a multiplicity of soundness and completeness arguments in full detail we just summarize what needs to be added to earlier proofs and we do this for a single representative example.

We discussed propositional classical tableaus in Chap. 3 , and now this is extended to take modal operators into account. The extension retains the pleasant advantages that classical tableaus had. A tableau proof generally only uses subformulas and negations of subformulas of the formula being proved, and hence the search for a proof is easier than axiomatically.

Over the course of history, modal logic has earned a reputation for being difficult and confusing. To be sure, modal logic is more complex than classical logic, and to ease the way into the subject we have emphasized thinking in terms of possible worlds throughout this book. In this chapter, however, we will address some of the sources of difficulty. One of the main reasons for confusion is that the way in which we ordinarily express modal claims can frequently be interpreted—very naturally—in more than one way. This ambiguity is often hidden from view, and that is how even the most gifted of logicians can get tripped up. Accordingly we are going to spend a considerable amount of time in the current chapter identifying the most famous of these ambiguities, and explaining the notation that we have chosen to ensure that it is free from these problems.

There are several propositional modal logics that we have looked at.

In this chapter we construct an axiomatic proof system for classical propositional logic. In the next chapter we revisit the logic, but with semantic tableaus as the main proof method. There are many logics in use today but all have a certain commonality. Syntactically there is a specification of a formal language. There is some notion of a semantics, providing a mathematically defined meaning for formulas of the language. There is some specification of a proof system. And finally, there are connections established between the semantics and the proof system. All this is at its clearest and simplest for classical propositional logic. It is the most well-behaved of all the logics. Think of our presentation in this and the next chapter as providing a foundation on which many more elaborate logics can be built. Our interest, of course, will be on those that are modal.

Through all our discussions about classical and modal logics, we have examined both tableau and axiom systems. Propositionally, modal axiomatics is quite general, much more so than tableau systems. One can specify any number of modal logics axiomatically, each with its corresponding semantics, but for which no tableau systems are known. Of course, what it means to be a tableau system is somewhat open. When moving to a modal setting we added prefix machinery, in Chap. 7 . In Sect. 7.7 other kinds of machinery were discussed. How much extra machinery can we add and still have something that can be considered a tableau system? But since our primary interests in this book are philosophical, relatively simple modal logics are of primary concern to us, and for these we have both axiomatics and tableaus at the propositional level.