First-order modal logic (Q1870904)

This is an introductory textbook to logics for first-order-languages with modal operators, expounding (in addition to standard topics) important material not previously found in other textbooks of the same field. The book approaches semantics using possible world, or Kripke, models and for most of the book the proof-theoretic techniques are systems based on semantic tableau rules. The axiomatic approach to propositional and first-order modal logic is presented only in two of the twelve chapters of the book. Also, no completeness and soundness proofs are offered for the different axiomatic modal formal systems characterized; the reader is rather referred to published works where such proofs can be found. Completeness and soundness proofs are provided for the systems based on semantic tableau rules. In addition to the technical expositions, there are brief and clear discussions of philosophical issues that motivate the development of the modal logics characterized in the book. Also, the book considers what bearing technical developments would have on well-known philosophical problems. Philosophical topics taken into account include the distinction between \textit{de dicto} and \textit{de re} necessity, the possibility of quantified modal logic, the range of quantifiers within modal contexts (and so the problems of actualism and possibilism), the nature of identity, the indiscernibility of identicals, existence and non-being, proper names and definite descriptions. In detail: after characterizing the semantics for propositional modal languages and different semantic tableau systems corresponding to such a semantics, the book initially considers first-order modal languages without (individual) constants and function symbols. Two semantic systems are formulated for these languages: one in which the domain assigned to (first-order) quantifiers varies from possible world to possible world and another in which such a domain is constant. The former semantic system is associated to an actualist interpretation and the latter to a possibilist interpretation of first-order quantifiers, though in later sections of the book the authors show how to embed the possibilist semantic framework in an actualist semantic framework and vice versa. Completeness and soundness proofs of a certain tableau system (having quantifier rules for varying domains) with respect to the varying domain semantics are provided. Left to the reader are the soundness and completeness proofs for the constant domain semantics relative to a system based on tableau rules, which is formulated in the book itself and contains quantifier rules for constant domains. Next, the book focuses on models with varying domains that interpret a certain relation symbol (at each possible world) as the equality relation among the members of the domain of the model (i.e., the union of the different domains associated to each possible world of the model). These models are called ``normal''; completeness and soundness proofs of a certain tableau system (involving equality tableau rules) in relation to normal models are given. In later chapters, first-order modal languages allowing predicate abstraction (i.e., formation of predicates from formulas by means of certain devices in the language) and whose set of terms includes (individual) constants as well as function symbols are taken into account. It is shown that predicate abstraction allows several philosophically important distinctions (such as the \textit{de \(re/de\) dicto} distinction) to be formally represented in the language. The semantic system characterized in previous chapters is accordingly extended to a semantic system covering the new sort of languages; models of this semantics provide non-rigid interpretations of constant and functions symbols. The resulting semantic system is later modified to a semantics assigning partial functions to constant and function symbols with the purpose of formally representing non-designation in individual constants. Also, in the last chapter of the book, first-order modal languages (with predicate abstractions, constant and functions symbols) allowing for the formation of definite description and their corresponding semantics are considered. Varying domain as well as constant domain tableau rules for the logics of the aforementioned sort of languages are formulated. The authors explicitly omit completeness and soundness proofs for systems based on those tableau rules, since, according to them, such proofs would not involve fundamental ideas other than those already present in previously constructed soundness and completeness proofs.