Modern Origins of Modal Logic

1. The Syntactic Tradition

In a 1912 pioneering article in Mind “Implication and the Algebra of Logic” C.I. Lewis started to voice his concerns on the so-called “paradoxes of material implication”. Lewis points out that in Russell and Whitehead’s Principia Mathematica we find two “startling theorems: (1) a false proposition implies any proposition, and (2) a true proposition is implied by any proposition” (1912: 522). In symbols:

and

Lewis has no objection to these theorems in and of themselves:

In themselves, they are neither mysterious sayings, nor great discoveries, nor gross absurdities. They exhibit only, in sharp outline, the meaning of “implies” which has been incorporated into the algebra. (1912: 522)

However, the theorems are inadequate vis-à-vis the intended meaning of “implication” and our actual modes of inference that the intended meaning tries to capture. So Lewis has in mind an intended meaning for the conditional connective \(\rightarrow\) or \(\supset\), and that is the meaning of the English word “implies”. The meaning of “implies” is that “of ordinary inference and proof” (1912: 531) according to which a proposition implies another proposition if the second can be logically deduced from the first. Given such an interpretation, (1) and (2) ought not to be theorems, thus propositional logic may be regarded as unsound vis-à-vis the reading of \(\rightarrow\) as logical implication. Consider (2) for example: from the sheer truth of a proposition \(p\) it does not (logically) follow that \(p\) follows logically from any proposition whatsoever. Additionally, given the intended, strict reading of \(\rightarrow\) as logical implication and the equivalence of \((\neg p\rightarrow q)\) and \((p\vee q)\), Lewis infers that disjunction too must be given a new intensional sense, according to which \((p\vee q)\) holds just in case if \(p\) were not the case it would have to be the case that \(q\).

Considerations of this sort, based on the distinction between extensional and intensional readings of the connectives, were not original to Lewis. Already in 1880 Hugh MacColl in the first of a series of eight papers on Symbolical Reasoning published in Mind claimed that \((p\rightarrow q)\) and \((\neg p\vee q)\) are not equivalent: \((\neg p\vee q)\) follows from \((p\rightarrow q)\), but not vice versa (MacColl 1880: 54). This is the case because MacColl interprets \(\vee\) as regular extensional disjunction, and \(\rightarrow\) as intensional implication, but then from the falsity of \(p\) or the truth of \(q\) it does not follow that \(p\) without \(q\) is logically impossible. In the second paper of the series, MacColl distinguishes between certainties, possibilities and variable statements, and introduces Greek letters as indices to classify propositions. So \(\alpha^{\varepsilon}\) expresses that \(\alpha\) is a certainty, \(\alpha^{\eta}\) that \(\alpha\) is an impossibility, and \(\alpha^{\theta}\) that \(\alpha\) is a variable, i.e., neither a certainty nor an impossibility (MacColl 1897: 496–7). Using this threefold classification of statements, MacColl proceeds to distinguish between causal and general implication. A causal implication holds between statements \(\alpha\) and \(\beta\) if whenever \(\alpha\) is true \(\beta\) is true, and \(\beta\) is not a certainty. A general implication holds between \(\alpha\) and \(\beta\) whenever \(\alpha\) and not\(-\beta\) is impossible, thus in particular whenever \(\alpha\) is an impossibility or \(\beta\) a certainty (1897: 498). The use of indices opened the door to the iteration of modalities, and the beginning of the third paper of the series (MacColl 1900: 75–6) is devoted to clarifying the meaning of statements with iterated indices, including \(\tau\) for truth and \(\iota\) for negation. So for example \(A^{\eta \iota \varepsilon}\) is read as “It is certain that it is false that A is impossible” (note that the indices are read from right to left). Interestingly, Bertrand Russell’s 1906 review of MacColl’s book Symbolic Logic and its Applications (1906) reveals that Russell did not understand the modal idea of the variability of a proposition, hence wrongly attributed to MacColl a confusion between sentences and propositions, as Russell conferred variability only to sentences whose meaning, hence truth value, was not fixed. Similarly, certainty and impossibility are for Russell material properties of propositional functions (true of everything or of nothing) and not modal properties of propositions. It might be said that MacColl’s work came too early and fell on deaf ears. In fact, Rescher reports on Russell’s declared difficulty in understanding MacColl’s symbolism and, more importantly, argues that Russell’s view of logic had a negative impact on the development of modal logic (“Bertrand Russell and Modal Logic” in Rescher 1974: 85–96). Despite MacColl’s earlier work, Lewis can be regarded as the father of the syntactic tradition, not only because of his greater influence on later logicians, but especially for his development of various systems containing the new intensional connectives.

1.1 The Lewis Systems

In “The Calculus of Strict Implication” (1914) Lewis suggests two possible alternatives to the extensional system of Whitehead and Russell’s Principia Mathematica. One way of introducing a system of strict implication consists in eliminating from the system those theorems that, like (1) and (2) above, are true only for material implication but not for strict implication, thereby obtaining a sound system for both material and strict implication, though in neither case complete. The second, more fruitful alternative consists in introducing a new system of strict implication, still modeled on the Whitehead and Russell system of material implication, that will contain (all or a part of) extensional propositional logic as a proper part, but aspiring to completeness for at least strict implication. This second option is further developed in A Survey of Symbolic Logic (1918). There Lewis introduces a first system meant to capture the ordinary, strict sense of implication, guided by the idea that:

Unless “implies” has some “proper” meaning, there is no criterion of validity, no possibility even of arguing the question whether there is one or not. And yet the question What is the “proper” meaning of “implies”? remains peculiarly difficult. (1918: 325)

The 1918 system takes as primitive the notion of impossibility \((\neg \Diamond)\), defines the operator of strict implication in its terms, and still employs an operator of intensional disjunction. However, Post will prove that this system leads to the collapse of necessity to truth—alternatively, of impossibility to falsity—since from one of its theorems \(((p\Rightarrow q)\Leftrightarrow(\neg \Diamond q\Rightarrow \neg \Diamond p))\) it can be proved that \((\neg p\Leftrightarrow \neg \Diamond p)\). In 1920, “Strict Implication—An Emendation”, Lewis fixes the system substituting the weaker axiom \(((p\Rightarrow q)\Rightarrow(\neg \Diamond q\Rightarrow \neg \Diamond p))\) for the old one. Finally, in Appendix II of the Lewis and Langford’s volume Symbolic Logic (1932: 492–502) “The Structure of the System of Strict Implication” the (weakened) 1918 system is given a new axiomatic base.

In the 1932 Appendix C.I. Lewis introduces five different systems. The modal primitive symbol is now the operator of possibility \(\Diamond\), strict implication \((p\Rightarrow q)\) is defined as \(\neg \Diamond(p\wedge \neg q)\), and \(\vee\) is ordinary extensional disjunction. The necessity operator \(\Box\) can also be introduced and defined, though Lewis does not, in the usual way as \(\neg \Diamond \neg\).

Where \(p, q\), and \(r\) are propositional variables, System S1 has the following axioms:

Axiom B5 was proved redundant by McKinsey (1934), and can thereby be ignored.

The rules are (1932: 125–6):

System S2 is obtained from System S1 by adding what Lewis calls “the consistency postulate”, since it obviously holds for \(\Diamond\) interpreted as consistency:

System S3 is obtained from system S1 by adding the axiom:

System S3 corresponds to the 1918 system of A Survey, which Lewis originally considered the correct system for strict implication. By 1932, Lewis has come to prefer system S2. The reason, as reported in Lewis 1932: 496, is that both Wajsberg and Parry derived in system S3—in its 1918 axiomatization—the following theorem:

which according to Lewis ought not to be regarded as a valid principle of deduction. In 1932 Lewis is not sure that the questionable theorem is not derivable in S2. Should it be, he would then adjudicate S1 as the proper system for strict implication. However, Parry (1934) will later prove that neither A8 nor

can be derived in S2.

A further existence axiom can be added to all these systems:

The addition of B9 makes it impossible to interpret \(\Rightarrow\) as material implication, since in the case of material implication it can be proved that for any propositions \(p\) and \(q, ((p\rightarrow q)\vee(p\rightarrow \neg q))\) (1932: 179). From B9 Lewis proceeds to deduce the existence of at least four logically distinct propositions: one true and necessary, one true but not necessary, one false and impossible, one false but not impossible (1932: 184–9).

Following Becker (1930), Lewis considers three more axioms:

System S4 adds axiom C10 to the basis of S1. System S5 adds axiom C11, or alternatively C10 and C12, to the basis of S1. Lewis concludes Appendix II by noting that the study of logic is best served by focusing on systems weaker than S5 and not exclusively on S5.

Paradoxes of strict implication similar to those of material implication arise too. Given that strict implication \((p\Rightarrow q)\) is defined as \(\neg \Diamond(p\wedge \neg q)\), it follows that an impossible proposition implies anything, and that a necessary proposition is implied by anything. Lewis argues that this is as it ought to be. Since impossibility is taken to be logical impossibility, i.e., ultimately a contradiction, Lewis argues that from an impossible proposition like \((p\wedge \neg p)\), both \(p\) and \(\neg p\) follow. From \(p\) we can derive \((p\vee q)\), for any proposition \(q\). From \(\neg p\) and \((p\vee q)\), we can derive \(q\) (1932: 250). The argument is controversial since one can argue that the principle \((p\Rightarrow(p\vee q))\) should not be a theorem of a system aiming to express ordinary implication (see, e.g., Nelson 1930: 447). Whatever the merits of this argument, those who disagreed with Lewis started to develop a logic of entailment based on the assumption that entailment requires more than Lewis’s strict implication. See, for example, Nelson 1930, Strawson 1948, and Bennett 1954. See also the SEP entry on relevance logic.

Notice that it was Lewis’s search for a system apt to express strict implication that made Quine reject modal systems as based on a use-mention confusion insofar as such systems were formulated to express at the object level proof-theoretic or semantic notions like consistency, implication, derivability and theoremhood (in fact, whenever \(p\rightarrow q\) is a propositional theorem, system S1, and so all the other stronger Lewis systems too, can prove \(p\Rightarrow q\) (Parry 1939: 143)).

1.2 Other Systems and Alternative Axiomatizations of the Lewis Systems

Gödel in “An Interpretation of the Intuitionistic Propositional Calculus” (1933) is the first to propose an alternative axiomatization of the Lewis system S4 that separates the propositional basis of the system from the modal axioms and rules. Gödel adds the following rules and axioms to the propositional calculus.

Initially, Gödel employs an operator \(B\) of provability to translate Heyting’s primitive intuitionistic connectives, and then observes that if we replace \(B\) with an operator of necessity we obtain the system S4. Gödel also claims that a formula \(\Box p\vee \Box q\) is not provable in S4 unless either \(\Box p\) or \(\Box q\) is provable, analogously to intuitionistic disjunction. Gödel’s claim will be proved algebraically by McKinsey and Tarski (1948). Gödel’s short note is important for starting the fruitful practice of axiomatizing modal systems separating the propositional calculus from the strictly modal part, but also for connecting intuitionistic and modal logic.

Feys (1937) is the first to propose system T by subtracting axiom 4 from Gödel’s system S4 (see also Feys 1965: 123–124). In An Essay in Modal Logic (1951) von Wright discusses alethic, epistemic, and deontic modalities, and introduces system M, which Sobociński (1953) will prove to be equivalent to Feys’ system T. Von Wright (1951: 84–90) proves that system M contains Lewis’s S2, which contains S1—where system S is said to contain system S′ if all the formulas provable in S′ can be proved in S too. System S3, an extension of S2, is not contained in M. Nor is M contained in S3. Von Wright finds S3 of little independent interest, and sees no reason to adopt S3 instead of the stronger S4. In general, the Lewis systems are numbered in order of strength, with S1 the weakest and S5 the strongest, weaker systems being contained in the stronger ones.

Lemmon (1957) also follows Gödel in axiomatizing modal systems on a propositional calculus base, and presents an alternative axiomatization of the Lewis systems. Where PC is the propositional calculus base, PC may be characterized as the following three rules (1957: 177):

Further rules in Lemmon’s system are:

Further axioms in Lemmon’s system are:

Using the above rules and axioms Lemmon defines four systems. System P1, which is proved equivalent to the Lewis system S1, employs the propositional basis (PC), rules (a′)—necessitation of tautologies and axioms—and (b′), and axioms (2) and (3). System P2, equivalent to S2, employs (PC), rules (a′) and (b), and axioms (2) and (1′). System P3, equivalent to S3, employs (PC), rule (a′), and axioms (2) and (1). System P4, equivalent to S4, employs (PC), rule (a), and axioms (2) and (1). In Lemmon’s axiomatization it is easy to see that S3 and von Wright’s system M (Feys’ T) are not included in each other, given M’s stronger rule of necessitation and S3’s stronger axiom (1) in place of (1′) = K. In general, Lemmon’s axiomatization makes more perspicuous the logical distinctions between the different Lewis systems.

Lemmon considers also some systems weaker than S1. Of particular interest is system S0.5 which weakens S1 by replacing rule (a′) with the weaker rule (a″):

Lemmon interprets system S0.5 as a formalized metalogic of the propositional calculus, where \(\Box \alpha\) is interpreted as “\(\alpha\) is a tautology”.

We call “normal” the systems that include PC, axiom K and the rule of necessitation. System K is the smallest normal system. System T adds axiom T to system K. System B (the Brouwersche system) adds axiom B

to system T. S4 adds axiom 4 (equivalent to Becker’s C10) to system T. S5 adds axioms B and 4, or alternatively axiom E

to system T. Lewis’s systems S1, S2, and S3 are non-normal given that they do not contain the rule of Necessitation. For the relationship between these (and other) systems, and the conditions on frames that the axioms impose, consult the SEP entry on modal logic.

Only a few of the many extensions of the Lewis systems that have been discussed in the literature are mentioned here. Alban (1943) introduces system S6 by adding to S2 the axiom \(\mvdash \Diamond \Diamond p\). Halldén (1950) calls S7 the system that adds the axiom \(\mvdash \Diamond \Diamond p\) to S3, and S8 the system that extends S3 with the addition of the axiom \(\mvdash \neg \Diamond \neg \Diamond \Diamond p\). While the addition of an axiom of universal possibility \(\mvdash \Diamond p\) would be inconsistent with all the Lewis systems, since they all contain theorems of the form \(\mvdash \Box p\), systems S6, S7 and S8 are consistent. Instead, the addition of either of these axioms to S4, and so also to S5, results in an inconsistent system, given that in S4 \(\mvdash \Diamond \Diamond p\Rightarrow \Diamond p\). Halldén also proved that a formula is a theorem of S3 if and only if it is a theorem of both S4 and S7 (1950: 231–232), thus S4 and S7 are two alternative extensions of S3.

2. The Matrix Method and Some Algebraic Results

In “Philosophical Remarks on Many-Valued Systems of Propositional Logic” (1930; but Łukasiewicz 1920 is a preliminary Polish version of the main ideas of this paper), Łukasiewicz says:

When I recognized the incompatibility of the traditional theorems on modal propositions in 1920, I was occupied with establishing the system of the ordinary “two-valued” propositional calculus by means of the matrix method. I satisfied myself at the time that all theses of the ordinary propositional calculus could be proved on the assumption that their propositional variables could assume only two values, “0” or “the false”, and “1” or “the true”. (1970: 164)

This passage illustrates well how Łukasiewicz was thinking of logic in the early twenties. First, he was thinking in algebraic terms, rather than syntactically, concerning himself not so much with the construction of new systems, but with the evaluation of the systems relatively to sets of values. Secondly, he was introducing three-valued matrices to make logical space for the notion of propositions (eminently about future contingents) that are neither true nor false, and that receive the new indeterminate value ½. Ironically, later work employing his original matrix method will show that the hope of treating modal logic as a three-valued system cannot be realized. See also the SEP entry on many-valued logic.

A matrix for a propositional logic L is given by (i) a set K of elements, the truth-values, (ii) a non-empty subset \(D\subseteq K\) of designated truth-values, and (iii) operations on the set K, that is, functions from \(n\)-tuples of truth-values to truth-values, that correspond to the connectives of L. A matrix satisfies a formula A under an assignment \(\sigma\) of elements of K to the variables of A if the value of A under \(\sigma\) is a member of D, that is, a designated value. A matrix satisfies a formula if it satisfies it under every assignment \(\sigma\). A matrix for a modal logic M extends a matrix for a propositional logic by adding a unary function that corresponds to the connective \(\Diamond\).

Matrices are typically used to show the independence of the axioms of a system as well as their consistency. The consistency of two formulas A and B is established by a matrix that, under an assignment \(\sigma\), assigns designated values to both formulas. The independence of formula B from formula A is established by a matrix that (i) preserves the validity of the rules of the system and that (ii) under an interpretation \(\sigma\) assigns a designated value to A but not to B. Parry (1939) uses the matrix method to show that the number of modalities of Lewis’s systems S3 and S4 is finite. A modality is a modal function of one variable that contains only the operators \(\neg\) and \(\Diamond\). The degree of a modality is given by the number of \(\Diamond\) operators contained. A proper modality is of degree higher than zero. Proper modalities can be of four different forms:

The improper modalities are \(p\) and \(\neg p\) (1939: 144). Parry proves that S3 has 42 distinct modalities, and that S4 has 14 distinct modalities. It was already known that system S5 has only 6 distinct modalities since it reduces all modalities to modalities of degree zero or one. Parry introduces system S4.5 by adding to S4 the following axiom:

The system reduces the number of modalities of S4 from 14 to 12 (or 10 proper ones). The addition of the same axiom to Lewis’s system S3 results in a system with 26 distinct modalities. Moreover, if we add

to S3 we obtain a distinct system with 26 modalities also intermediate between S3 and S4. Therefore the number of modalities does not uniquely determine a system. Systems S1 and S2, as well as T and B, have an infinite number of modalities (Burgess 2009, chapter 3 on Modal Logic, discusses the additional systems S4.2 and S4.3 and explains well the reduction of modalities in different systems).

A characteristic matrix for a system L is a matrix that satisfies all and only the theorems of L. A matrix is finite if its set K of truth-values is finite. A finite characteristic matrix yields a decision procedure, where a system is decidable if every formula of the system that is not a theorem is falsified by some finite matrix (this is the finite model property). Yet Dugundji (1940) shows that none of S1–S5 has a finite characteristic matrix. Hence, none of these systems can be viewed as an \(n\)-valued logic for a finite \(n\). Later, Scroggs (1951) will prove that every proper extension of S5 that preserves detachment for material implication and is closed under substitution has a finite characteristic matrix.

Despite their lack of a finite characteristic matrix, McKinsey (1941) shows that systems S2 and S4 are decidable. To prove these results McKinsey introduces modal matrices \((K, D, -, *, \times)\), with \(-\), \(*\), and \(\times\) corresponding to negation, possibility, and conjunction respectively. A matrix is normal if it satisfies the following conditions:

These conditions correspond to Lewis’s rules of strict inference, adjunction and substitution of strict equivalents. The structure of McKinsey’s proof is as follows. The proof employs three steps. First, using an unpublished method of Lindenbaum explained to him by Tarski which holds for systems that have the rule of Substitution for propositional variables, McKinsey shows that there is an S2-characteristic matrix \(M = (K, D, -, *, \times)\) that does not satisfy condition (iii) and is therefore non-normal. M is a trivial matrix whose domain is the set of formulas of the system, whose designated elements are the theorems of the system, and whose operations are the connectives themselves. The trivial matrix M does not satisfy (iii) given that for some distinct formulas A and B, \(A\Leftrightarrow B\) is an S2-theorem. Second, McKinsey shows how to construct from M a normal, but still infinite, S2-characteristic matrix \(M_1 = (K_1, D_1, -_1, *_1, \times_1 )\), whose elements are equivalence classes of provably equivalent formulas of S2, i.e., of formulas A and B such that \(A\Leftrightarrow B\) is a theorem of S2, and whose operations are revised accordingly. For example, if \(E(A)\) is the set of formulas provably equivalent to A and \(E(A)\in K_1\), then \(-_1 E(A) = E(-A)= E(\neg A). M_1\) satisfies exactly the formulas satisfied by M without violating condition (iii), hence it is a characteristic normal matrix for S2 (\(M_1\) is the Lindenbaum algebra for S2). Finally, it is shown that for every formula A that is not a theorem of S2 there is a finite and normal matrix (a sub-algebra of \(M_1)\) that falsifies it. A similar proof is given for S4.

A matrix is a special kind of algebra. An algebra is a matrix without a set D of designated elements. Boolean algebras correspond to matrices for propositional logic. According to Bull and Segerberg (1984: 10) the generalization from matrices to algebras may have had the effect of encouraging the study of these structures independently of their connections to logic and modal systems. The set of designated elements D in fact facilitates a definition of validity with respect to which the theorems of a system can be evaluated. Without such a set the most obvious link to logic is severed. A second generalization to classes of algebras, rather than merely to individual algebras, was also crucial to the mathematical development of the subject matter. Tarski is the towering figure in such development.

Jónsson and Tarski (1951 and 1952) introduce the general idea of Boolean algebras with operators, i.e., extensions of Boolean algebras by addition of operators that correspond to the modal connectives. They prove a general representation theorem for Boolean algebras with operators that extends Stone’s result for Boolean algebras (every Boolean algebra can be represented as a set algebra). This work of Jónsson and Tarski evolved from Tarski’s purely mathematical study of the algebra of relations and includes no reference to modal logic or even logic in general. Jónsson and Tarski’s theorem is a (more general) algebraic analog of Kripke’s later semantic completeness results, yet this was not realized for some time. Not only was Tarski unaware of the connection, but it appears that both Kripke and Lemmon had not read the Jónsson and Tarski papers at the time in which they did their modal work in the late fifties and sixties, and Kripke claims to have reached the same result independently.

Lemmon (1966a and 1966b) adapts the algebraic methods of McKinsey to prove decidability results and representation theorems for various modal systems including T (though apparently in ignorance of Jónsson and Tarski’s work). In particular, he extends McKinsey’s method by introducing a new technique for constructing finite algebras of subsets of a Kripke model structure (discussed in the next section of this entry). Lemmon (1966b: 191) attributes to Dana Scott the main result of his second 1966 paper. This is a general representation theorem proving that algebras for modal systems can be represented as algebras based on the power set of the set K in the corresponding Kripke’s structures. As a consequence, algebraic completeness translates into Kripke’s model theoretic completeness. So, Lemmon elucidates very clearly the connection between Kripke’s models whose elements are worlds and the corresponding algebras whose elements are sets of worlds that can be thought of as propositions, thereby showing that the algebraic and model theoretic results are deeply connected. Kripke (1963a) is already explicit on this connection. In The Lemmon Notes (1977), written in collaboration with Dana Scott and edited by Segerberg, the 1966 technique is transformed into a purely model theoretic method which yields completeness and decidability results for many systems of modal logic in as general a form as possible (1977: 29).

See also the SEP entry on the algebra of logic tradition. For a basic introduction to the algebra of modal logic, consult Hughes and Cresswell 1968, Chapter 17 on “Boolean Algebra and Modal Logic”. For a more comprehensive treatment, see chapter 5 of Blackburn, de Rijke, and Venema 2001. See also Goldblatt 2003.

3. The Model Theoretic Tradition

3.1 Carnap

In the early 1940s the recognition of the semantical nature of the notion of logical truth led Rudolf Carnap to an informal explication of this notion in terms of Leibnizian possible worlds. At the same time, he recognized that the many syntactical advances in modal logic from 1918 on were still not accompanied by adequate semantic considerations. One notable exception was Gödel’s interpretation of necessity as provability and the resulting preference for S4. Carnap instead thought of necessity as logical truth or analyticity. Considerations on the properties of logically true sentences led him to think of S5 as the right system to formalize this ‘informal’ notion. Carnap’s work in the early forties would then be focused on (1) defining a formal semantic notion of L-truth apt to represent the informal semantic notions of logical truth, necessity, and analyticity, that is, truth in virtue of meaning alone (initially, he drew no distinction between these notions, but clearly thought of analyticity as the leading idea); and (2) providing a formal semantics for quantified S5 in terms of the formal notion of L-truth with the aim of obtaining soundness and completeness results, that is, prove that all the theorems of quantified S5 are L-true, and that all the L-truths (expressible in the language of the system) are theorems of the system.

The idea of quantified modal systems occurred to Ruth Barcan too. In “A Functional Calculus of First Order Based on Strict Implication” (1946a) she added quantification to Lewis’s propositional system S2; Carnap (1946) added it to S5. Though some specific semantic points about quantified modal logic will be considered, this entry is not focused on the development of quantified modal logic, but rather on the emergence of the model theoretic formal semantics for modal logic, propositional or quantified. For a more extensive treatment of quantified modal logic, consult the SEP entry on modal logic.

In “Modalities and Quantification” (1946) and in Meaning and Necessity (1947), Carnap interprets the object language operator of necessity as expressing at the object level the semantic notion of logical truth:

[T]he guiding idea in our constructions of systems of modal logic is this: a proposition \(p\) is logically necessary if and only if a sentence expressing \(p\) is logically true. That is to say, the modal concept of the logical necessity of a proposition and the semantical concept of the logical truth or analyticity of a sentence correspond to each other. (1946: 34)

Carnap introduces the apparatus of state-descriptions to define the formal semantic notion of L-truth. This formal notion is then to be used to provide a formal semantics for S5.

A state-description for a language L is a class of sentences of L such that, for every atomic sentence \(p\) of L, either \(p\) or \(\neg p\), but not both, is contained in the class. An atomic sentence holds in a state-description R if and only if it belongs to R. A sentence \(\neg A\) (where A need not be atomic) holds in R if and only if A does not hold in R; \((A\wedge B)\) holds in R if and only if both A and B hold in R, and so on for the other connectives in the usual inductive way; \((\forall x)Fx\) holds in R if and only if all the substitution instances of \(Fx\) hold in R. The range of a sentence is the class of state-descriptions in which it holds. Carnap’s notion of validity or L-truth is a maximal notion, i.e., Carnap defines a sentence to be valid or L-true if and only if it holds in all state-descriptions. In later work Carnap adopts models in place of state-descriptions. Models are assignments of values to the primitive non-logical constants of the language. In Carnap’s case predicate constants are the only primitive constants to which the models assign values, since individual constants are given a fixed pre-model interpretation and value assignments to variables are done independently of the models (1963a).

It is important to notice that the definition of L-truth does not employ the notion of truth, but rather only that of holding-in-a-state-description. Truth is introduced later as what holds in the real state description. To be an adequate formal representation of analyticity, L-truth must respect the basic idea behind analyticity: truth in virtue of meaning alone. In fact, the L-truths of a system S are such that the semantic rules of S suffice to establish their truth. Informally, state-descriptions represent something like Leibnizian possible worlds or Wittgensteinian possible states of affairs and the range of state-descriptions for a certain language is supposed to exhaust the range of alternative possibilities describable in that language.

Concerning modal sentences, Carnap adopts the following conventions (we use \(\Box\) in place of Carnap’s operator N for logical necessity). Let S be a system:

From which it follows that:

Carnap’s conventions hold also if we substitute “truth in a state description of S” for “truth in S”.

Carnap assumes a fixed domain of quantification for his quantified system, the functional calculus with identity FC, and consequently for the modal functional calculus with identity MFC, a quantified form of S5. The language of FC contains denumerably many individual constants, the universe of discourse contains denumerably many individuals, each constant is assigned an individual of the domain, and no two constants are assigned the same individual. This makes sentences like \(a = a\) L-true, and sentences like \(a = b\) L-false (1946: 49). Concerning MFC, the Barcan formula and its converse are both L-true, that is,

This result is guaranteed by the assumption of a fixed domain of quantification. Carnap proves that MFC is sound, that is, all its theorems are L-true, and raises the question of completeness for both FC and MFC. Gödel proved completeness for the first order predicate calculus with identity, but the notion of validity employed was truth in every non-empty domain of quantification, including finite domains. Carnap instead adopts one unique denumerable domain of quantification. The adoption of a fixed denumerable domain of individuals generates some additional validities already at the pre-modal level which jeopardize completeness, for example “There are at least two individuals”, \((\exists x)(\exists y)(x\ne y)\), turns out to be valid (1946: 53).

A consequence of the definitions of state-descriptions for a language and L-truth is that each atomic sentence and its negation turn out to be true at some, but not all, state-descriptions. Hence, if \(p\) is atomic both \(\Diamond p\) and \(\Diamond \neg p\) are L-true. Hence, Lewis’s rule of Uniform Substitution fails (if \(p\wedge \neg p\) is substituted for \(p\) in \(\Diamond p\) we derive \(\Diamond(p\wedge \neg p)\), which is L-false, not L-true). This is noticed by Makinson (1966a) who argues that what must be done is reinstate substitutivity and revise Carnap’s naïve notion of validity (as logical necessity) in favor of a schematic Quinean notion (“A logical truth … is definable as a sentence from which we get only truths when we substitute sentences for its simple sentences” Quine 1970: 50) that will not make sentences like \(\Diamond p\) valid. Nonetheless, Carnap proves the soundness and completeness of propositional S5, which he calls “MPC” for “modal propositional calculus”, following Wajsberg. The proof however effectively employs a schematic notion of validity.

It has been proved that Carnap’s notion of maximal validity makes completeness impossible for quantified S5, i.e., that there are L-truths that are not theorems of Carnap’s MFC. Let \(A\) be a non-modal sentence of MFC. By convention (1), \(\Box A\) is true in MFC if and only if \(A\) is L-true in MFC. But \(A\) is also a sentence of FC, thus if L-true in MFC it is also L-true in FC, since the state descriptions (models) of modal functional logic are the same as those of functional logic (1946: 54). This means that the state descriptions hold the triple role of (i) first-order models of FC thereby defining first-order validity, (ii) worlds for MFC thereby defining truth for \(\Box A\) sentences of MFC, and (iii) models of MFC thereby defining validity for MFC. The core of the incompleteness argument consists in the fact that the non-validity of a first-order sentence \(A\) can be represented in the modal language, as \(\neg \Box A\), but all models agree on the valuation of modal sentences, making \(\neg \Box A\) valid. Roughly, and setting aside complications created by the fact that Carnap’s semantics has only denumerable domains, if \(A\) is a first-order non-valid sentence of FC, \(A\) is true in some but not all the models or state-descriptions. Given Carnap’s conventions, it follows that \(\neg \Box A\) is true in MFC. But then \(\neg \Box A\) is L-true in MFC, i.e., in MFC \(\mvDash \neg \Box A\). Given that the non-valid first-order sentences are not recursively enumerable, neither are the validities for the modal system MFC. But the class of theorems of MFC is recursively enumerable. Hence, MFC is incomplete vis-à-vis Carnap’s maximal validity. Cocchiarella (1975b) attributes the result to Richard Montague and Donald Kalish. See also Lindström 2001: 209 and Kaplan 1986: 275–276.