# Modern Origins of Modal Logic

*First published Tue Nov 16, 2010*

Modal logic can be viewed broadly as the logic of different sorts of modalities, or modes of truth: alethic (“necessarily”), epistemic (“it is known that”), deontic (“it ought to be the case that”), or temporal (“it has been the case that”) among others. Common logical features of these operators justify the common label. In the strict sense however, the term “modal logic” is reserved for the logic of the alethic modalities. The scope of this entry is the recent historical development of modal logic, strictly understood as the logic of necessity and possibility, and particularly the historical development of systems of modal logic, both syntactically and semantically, from C. I. Lewis's pioneering work starting in 1918 to S. Kripke's work in the early 1960's. In that short span of time of less than fifty years, modal logic flourished both philosophically and mathematically. Mathematically, different modal systems were developed and advances in algebra helped to foster the model theory for such systems. This culminated in the development of a formal semantics that extended to modal logic the successful first-order model theoretic techniques, thereby affording completeness and decidability results for many systems. Philosophically, the availability of different systems and the adoption of the possible worlds model theoretic semantics were naturally accompanied by reflections on the nature of possibility and necessity, on distinct sorts of necessities, on the role of formal semantics, and on the nature of the possible worlds, to mention just a few.

Modal logic is a rich and complex subject matter. This entry does not present a complete survey of all the systems developed and of all the model theoretic results proved in the lapse of time under consideration. It does however offer a meaningful survey of the main systems and model theoretic results and aims to be useful to those looking for an historical outline of the subject matter that, even if not all-inclusive, delineates the most interesting results and indicates further lines of exploration. Bull and Segerberg's (1984, 3) useful division of the original sources of modal logic into three distinct traditions – syntactic, algebraic, and model theoretic – is adopted. For other less influential traditions, see Bull and Segerberg (1984, 16). The main focus is on propositional modal logic, while only some particular aspects of the semantics of quantified modal logic are discussed. For a more detailed treatment of quantified modal logic, consult the SEP entry on Modal Logic. Concerning the entry's notation, notice that ⇒ is adopted in place of Lewis's fishhook for strict implication, and ⇔ for strict equivalence.

- 1. The Syntactic Tradition
- 2. The Matrix Method and Some Algebraic Results
- 3. The Model Theoretic Tradition
- Bibliography
- Other Internet Resources
- Related Entries

## 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:

(1) ¬p→ (p→q)

and

(2)p→ (q→p)

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.” 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 → or ⊃, 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, and propositional logic may be regarded as unsound
*vis-à-vis* the reading of → 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 → as logical implication and the
equivalence of (¬*p*→*q*) and
(*p*∨*q*), Lewis infers that disjunction too must be
given a new intensional sense, according to which
(*p*∨*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*→*q*) and
(¬*p*∨*q*) are not equivalent:
(¬*p*∨*q*) follows from
(*p*→*q*), but not vice versa (MacColl 1880, 54).
This is the case because MacColl interprets ∨ as regular extensional
disjunction, and → 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 α^{ε}
expresses that α is a certainty, α^{η} that
α is an impossibility, and α^{θ} that α
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 α and β if
whenever α is true β is true, and β is not a certainty.
A general implication holds between α and β whenever α
and not-β is impossible, thus in particular whenever α is an
impossibility or β 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 1990, 75–6) is devoted to
clarify the meaning of statements with iterated indices, including
τ for truth and ι for negation. So for example
*A*^{ηιε} 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 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
which allowed the attribution of 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. Despite MacColl's work, Lewis can
be regarded as the father of the syntactic tradition, not only because
of his influence on later logicians, but especially because of his
introduction 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 are true only for material implication
but not for strict implication, thereby obtaining a sound system for
both material and strict implication, but 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
(¬◊), 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*⇒*q*)⇔(¬◊*q*⇒¬◊*p*)) it can be proved that
(¬*p*⇔¬◊*p*). In 1920, “Strict
Implication–An Emendation”, Lewis fixes the system
substituting for the old axiom the weaker one:
((*p*⇒*q*)⇒(¬◊*q*⇒¬◊*p*)). 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 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 ◊,
strict implication (*p*⇒*q*) is defined as
¬◊(*p*∧¬*q*), and ∨ is ordinary
extensional disjunction. The necessity operator □ can also be
introduced and defined, though Lewis does not, in the usual way as
¬◊¬.

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

Axioms forS1

B1 ( p∧q)⇒(q∧p)B2 ( p∧q)⇒pB3 p⇒(p∧p)B4 (( p∧q)∧r)⇒(p∧(q∧r))B5 p⇒¬¬pB6 (( p⇒q)∧(q⇒r))⇒(p⇒r)B7 ( p∧(p⇒q))⇒q

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

The rules are (1932, 125–6):

Rules for

S1

Uniform SubstitutionA valid formula remains valid if a formula is uniformly substituted in it for a propositional variable. Substitution of Strict EquivalentsEither of two strictly equivalent formulas can be substituted for one another. AdjunctionIf Φ and Ψ have been inferred, then Φ∧Ψ may be inferred. Strict InferenceIf Φ and Φ⇒Ψ have been inferred, then Ψ may be inferred.

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

B8. ◊(p∧q)⇒◊p

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

A8. ((p⇒q)⇒(¬◊q⇒¬◊p))

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 is that both Wajsberg and Parry derived
in system **S3** – in its 1918 axiomatization
– the following theorem:
(*p*⇒*q*)⇒((*q*⇒*r*)⇒(*p*⇒*r*)), 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 the questionable theorem derivable in
**S3** can be derived in **S2**.

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

B9 (∃ p,q)(¬(p⇒q)∧¬(p⇒¬q))

The addition of B9 makes it impossible to interpret ⇒ as
material implication, since in the case of material implication it can
be proved that for any propositions *p* and *q*,
((*p*→*q*)∨(*p*→¬*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 (184–9).

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

Three additional axioms

C10 ¬◊¬ p⇒¬◊¬¬◊¬pC11 ◊ p⇒¬◊¬◊pC12 p⇒¬◊¬◊p

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*⇒*q*) is defined as
¬◊(*p*∧¬*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*∧¬*p*), both *p* and
¬*p* follow. From *p* we can derive
(*p*∨*q*), for any proposition *q*. From
¬*p* and (*p*∨*q*), we can derive
*q* (1932, 250). The argument is controversial since one might
think that the principle (*p*⇒(*p*∨*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*→*q* is a propositional theorem, system
**S1**, and so all the other stronger Lewis systems too,
can prove *p*⇒*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. Necessitation: If ⊢α then
⊢□α, Axiom K:
⊢□(*p*→*q*)→(□*p*→□*q*), Axiom T: ⊢□*p*→*p*, and Axiom
4: ⊢□*p**→*□□*p*.
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 system **S4**. Gödel also claims that a
formula □*p*∨□*q* is not provable in
**S4** unless either □*p* or
□*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 a system is said to contain another
system if all the formulas provable in the second system can be proved
in the first system too. System **S3**, an extension of
**S2**, is not contained in **M**. Neither 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):

A characterization of propositional calculusPC

PCa If α is a tautology, then ⊢α PCb Substitution for propositional variables PCc Material detachment/Modus Ponens: if α and α → β are tautologies, then so is β

Further rules in Lemmon's system are:

(a) If ⊢α then ⊢□α (Necessitation) (a′) If α is a tautology or an axiom, then ⊢□α (b) If ⊢□(α→β) then ⊢□(□α→□β) (b′) Substitutability of strict equivalents.

Further axioms in Lemmon's system are:

(1) □( p→q)→□(□p→□q)(1′) □( p→q)→(□p→□q) (Axiom K)(2) □ p→p(Axiom T)(3) (□( p→q)∧□(q→r))→□(p→r)

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″):

(a″) If α is a tautology, then ⊢□α.

Lemmon interprets system **S0.5** as a formalized
metalogic of the propositional calculus, where □α is
interpreted as “α 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
⊢*p*⇒□◊*p* (equivalent to Becker's
C12) 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
⊢◊*p*⇒□◊*p*, (equivalent to
Becker's C11) 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)
introduced system **S6** by adding to **S2**
the axiom ⊢◊◊*p*. Halldén (1950) calls
**S7** the system that adds the axiom
⊢◊◊*p* to **S3**, and
**S8** the system that extends **S3** with
the addition of the axiom ⊢¬◊¬◊◊*p*.
While the addition of an axiom of universal possibility
⊢◊*p* would be inconsistemt with all the Lewis
systems, since they all contain theorems of the form
⊢□*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**
⊢◊◊*p*⇒◊*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).

## 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*⊆*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 σ of elements of *K* to the variables
of *A* if the value of *A* under σ is a member of
*D*, that is a designated value. A matrix satisfies a formula if
it satisfies it under every assignment σ. A matrix for a modal
logic *M* extends a matrix for a propositional logic by adding a
unary function that corresponds to the connective ◊.

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 σ, assigns to both formulas designated
values. 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 σ assigns to
*A* but not to *B* a designated value. 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 ¬ and ◊. The degree of a modality is given by the
number of ◊ operators contained. A proper modality is of degree
higher than zero. Proper modalities can be of four different forms: (1)
¬…◊*p*, (2) ◊…◊*p*, (3)
¬…◊¬*p*, (4) ◊…¬*p*.
The improper modalities are *p* and ¬*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:
⊢¬◊¬◊¬◊*p*⇒¬◊*p*.
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
⊢¬◊¬◊◊*p*⇒¬◊¬◊*
p* 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.

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*, −, *, ×), with −,
*, and × corresponding to negation, possibility, and conjunction
respectively. A matrix is *normal* if it satisfies the following
conditions:

- if
*x*∈*D*and (*x*⇒*y*) ∈*D*and*y*∈*K*, then*y*∈*D*, - if
*x*∈*D*and*y*∈*D*, then*x*×*y*∈*D*, - if
*x*∈*K*and*y*∈*K*and*x*⇔*y*∈*D*, then*x*=*y*.

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*, −, *, ×) 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*⇔*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}*), whose elements are equivalence classes of provably equivalent formulas of*

_{1}**S2**, i.e. of formulas

*A*and

*B*such that

*A*⇔

*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*)∈

*K*

_{1}, then −

_{1}*E*(

*A*) =

*E*(−

*A*)=

*E*(¬

*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 Kripkean model structure.
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 1940's 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. 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 ¬*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 ¬*A* (where *A* need not be atomic) holds in
*R* if and only if *A* does not hold in *R*;
(*A*∧*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; (∀*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 now
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 □ in place of Carnap's operator *N* for logical
necessity). Let *S* be a system:

- A sentence □
*A*is true in*S*if and only if*A*is*L*-true in*S*(so a sentence □*A*is true in*S*if and only if*A*holds in all the state descriptions of*S*); - A sentence □
*A*is*L*-true in*S*if and only if □*A*is true in*S*(so all state-descriptions agree in their evaluation of modal sentences).

From which it follows that:

- □
*A*is*L*-true in*S*if and only if*A*is*L*-true in*S*.

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
⊨(∀*x*)□*Fx*↔□(∀*x*)*Fx*. This result is guaranteed by the assumption of a fixed domain
of quantification. Carnap proves that **MFC** is sound,
that is that 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”,
(∃*x*)(∃*y*)(*x*≠*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 ◊*p* and
◊¬*p* are *L*-true. Hence, Lewis's rule of
Uniform Substitution fails (if *p*∧¬*p* is
substituted for *p* in ◊*p* we derive
◊(*p*∧¬*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 ◊*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. there
are *L*-truths that are not theorems of Carnap's
**MFC**. Let *A* be a non-modal sentence of
**MFC**. By convention (1), □*A* is true in
**MFC** if and only if *A* is *L*-true in
**MFC**. But *A* is also a sentence of
**FC** and it is then *L*-true in
**FC** too, 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 □*A* sentences of **MFC**, and (iii)
models of **MFC** thereby defining validity for
**MFC**. Now let *A* be a first-order non-valid
sentence of **FC**, that is *A* is true in some but
not all the models or state-descriptions of **FC**.
*A* is then also a non-valid sentence of **MFC**.
Hence, by convention (1) ¬□*A* is true in
**MFC**. By convention (2), ¬□*A* is
*L*-true in **MFC**, i.e. in **MFC**
⊨¬□*A*. But the non-valid first-order sentences
are not recursively enumerable, hence 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.

### 3.2. Kripke's Possible Worlds Semantics

Carnap's semantics is indeed a precursor of Possible Worlds
Semantics (PWS). Yet some crucial ingredients are still missing. First,
the maximal notion of validity must be replaced by a new universal
notion. Second, definite descriptions must make space for possible
worlds understood as indices or points of evaluation. Last, a relation
of accessibility between worlds needs to be introduced. Though Kripke
is by no means the only logician in the fifties and early sixties to
work on these ideas, it is in Kripke's version of PWS that *all*
these innovations are present. Kanger (1957), Montague (1960, but
originally presented in 1955), Hintikka (1961), and Prior (1957) were
all thinking of a relation between worlds, and Hintikka (1961) like
Kripke (1959) adopted a new notion of validity that required truth in
all arbitrary sets of worlds. But Kripke was the only one to
characterize the worlds as simple points of evaluation (in 1963). Other
logicians were still thinking of the worlds fundamentally as models of
first-order logic, though perhaps Prior in his development of temporal
logic was also moving towards a more abstract characterization of
instants of time. Kripke's more abstract characterization of the worlds
is crucial in the provision of a link between the model theoretic
semantics and the algebra of modal logic. Kripke saw very clearly this
connection between the algebra and the semantics, and this made it
possible for him to obtain model theoretic completeness and
decidability results for various modal systems in a systematic way.
Goldblatt (2003, section 4.8) argues convincingly that Kripke's
adoption of points of evaluation in the model structures is a
particularly crucial innovation. Such a generalization opens the door
to different future developments of the model theory and makes it
possible to provide model theories for intensional logics in general.
For these reasons, in this entry we devote more attention to Kripke's
version of PWS. For a more comprehensive treatment of the initial
development of PWS, including the late fifties work on
**S5** of the French logician Bayart, the reader is
referred to Goldblatt 2003. On the differences between Kanger's
semantics and standard PWS semantics, see Lindström 1996 and
1998.

Kripke's 1959 “A Completeness Theorem in Modal Logic”
contains a model theoretic completeness result for a quantified version
of **S5** with identity. In Kripke's semantic treatment of
quantified **S5**, which he calls
**S5* ^{=}**, an assignment of values to a formula

*A*in a domain of individuals

*D*assigns a member of

*D*to each free individual variable of

*A*, a truth value

*T*or

*F*to each propositional variable of

*A*, and a set of ordered

*n*-tuples of members of

*D*to each

*n*-place predicate variable of

*A*(the language for the system contains no non-logical constants). Kripke defines a

*model over a non-empty domain*

*D*of individuals as an ordered pair (

*G*,

*K*), such that

*G*∈

*K*,

*K*is an

*arbitrary*subset of assignments of values to the formulas of

**S5***, and all

^{=}*H*∈

*K*agree on the assignments to individual variables. For each

*H*∈

*K*, the value that

*H*assigns to a formula

*B*is defined inductively. Propositional variables are assigned

*T*or

*F*by hypothesis. If

*B*is

*P*(

*x*, …,

_{1}*x*),

_{n}*B*is assigned

*T*if and only if the

*n*-tuple of elements that are assigned to

*x*, …,

_{1}*x*belongs to the set of

_{n}*n*-tuples of individuals that

*H*assigns to

*P*.

*H*assigns

*T*to ¬

*B*if and only if it assigns

*F*to

*B*.

*H*assigns

*T*to

*B*∧

*C*if and only if it assigns

*T*to

*B*and to

*C*. If

*B*is

*x*=

*y*it is assigned

*T*if and only if

*x*and

*y*are assigned the same value in

*D*. If

*B*is (∀

*x*)

*Fx*it is assigned

*T*if and only if

*Fx*is assigned

*T*for every assignment to

*x*. □

*B*is assigned

*T*if and only if

*B*is assigned

*T*by every

*H*∈

*K*.

The most important thing to be noticed in the 1959 model theory is
the definition of validity. A formula *A* is said to be
*valid in a model* (*G*, *K*) in *D* if and
only if it is assigned *T* in *G*, to be *valid in a
domain* *D* if and only if it is valid in every model in
*D*, and to be *universally valid* if and only if it is
valid in every non-empty domain. Kripke says: “In trying to
construct a definition of universal logical validity, it seems
plausible to assume not only that the universe of discourse may contain
an arbitrary number of elements and that predicates may be assigned any
given interpretations in the actual world, but also that *any
combination of possible worlds may be associated with the real world
with respect to some group of predicates*. In other words, it is
plausible to assume that no further restrictions need be placed on
*D*, *G*, and *K*, except the standard one that
*D* be non-empty. This assumption leads directly to our
definition of universal validity.” (1959, 3). This new universal
notion of validity is much more general than Carnap's maximal validity.
The elements *H* of *K* still correspond to first-order
models, like Carnap's state-descriptions, and in each model of Kripke
the elements *H* of *K* are assigned the same domain
*D* of individuals and the individual variables have a fixed
cross-model assignment. So far the only significant difference from
Carnap is that different Kripke models can have domains of different
cardinality. This by itself is sufficient to reintroduce completeness
for the non-modal part of the system. But the most significant
difference, and the one that makes it possible to prove completeness
for the modal system, is the definition of validity not as truth in all
worlds of a maximal structure of worlds, but as truth across all the
subsets of the maximal structure. Kripke's model theory disconnects
validity from necessity. While necessities are relative to a model,
hence to a set of worlds, validities must hold across all such sets.
This permits the reintroduction of the rule of Uniform Substitution. To
see this intuitively in a simple case, consider an atomic sentence
*p*. The classical truth-table for *p* contains two rows,
one where *p* is true and one where *p* is false. Each
row is like a possible world, or an element *H* of *K*.
If we only consider this complete truth table, we are only considering
maximal models that contain two worlds (it makes no difference which
world is actual). By the definition of truth for a formula
□*B*, □*p* is false in all the worlds of the
maximal model, and ◊*p* is true in all of them. If validity
is truth in all worlds, like for Carnap, it follows that
⊨◊*p*, but in **S5**
**⊬**◊*p*. If instead we define validity
as Kripke does, we have to consider also the non-maximal models that
contain only one world, that is incomplete truth-tables that cancel
some rows. Hence, there are two more models to be taken into
consideration: one which contains only one world *H*=*G*
where *p* is true, hence so is □*p*, and one which
contains only one world *H*=*G* where *p* is false
and so is □*p* as well as ◊*p*. Thanks to this
last model ⊭◊*p*.

Kripke's completeness proof makes use of Beth's method of semantic
tableaux. A semantic tableau is used to test whether a formula
*B* is a semantic consequence of some formulas
*A*_{1}, …, *A*_{n}. The
tableau assumes that the formulas *A*_{1}, …,
*A*_{n} are true and *B* is false and is
built according to rules that follow the definitions of the logical
connectives. For example, if a formula ¬*A* is on the left
column of the tableau (where true formulas are listed), *A* will
be put on the right column (where false formulas are listed). To deal
with modal formulas, sets of tableaux must be considered, since if
□*A* is on the right column of a tableau, a new auxiliary
tableau must be introduced with *A* on its right column. A main
tableau and its auxiliary tableaux form a set of tableaux. If a formula
*A*∧*B* is on the right column of the main tableau,
the set of tableaux splits into two new sets of tableaux: one whose
main tableau lists *A* on its right column and one whose main
tableau lists *B* on the right column. So we have to consider
alternative sets of tableaux. A semantic tableau is closed if and only
if all its alternative sets are closed. A set of tableaux is closed if
it contains a tableau (main or auxiliary) that reaches a contradiction
in the form of (i) one and the same formula *A* appearing in
both its columns or (ii) an identity formula of the form *a* =
*a* in its right side (this is an oversimplification of the
definition of a closed tableau, but not harmful for our purposes).
Oversimplifying once more, the structure of Kripke's completeness proof
consists of proving that a semantic tableau used to test whether a
formula *B* is a semantic consequence of formulas
*A*_{1}, …, *A*_{n} is
closed if and only (i) in **S5* ^{=}**

*A*

_{1}, …,

*A*

_{n}⊢

*B*and (ii)

*A*

_{1}, …,

*A*

_{n}⊨

*B*. This last result is achieved by showing how to build models from semantic tableaux. As a consequence of (i) and (ii) we have soundness and completeness for

**S5***, that is:

^{=}*A*

_{1}, …,

*A*

_{n}⊢

*B*if and only if

*A*

_{1}, …,

*A*

_{n}⊨

*B*.

The 1959 paper contains also a proof of the modal counterpart of the
Löwenhein-Skolem theorem for first-order logic, according to which
if a formula is satisfiable in a non-empty domain then if it is
satisfiable, and hence valid (true in *G*), in a model
(*G*, *K*) in a domain *D*, where *both*
*K* and *D* are either finite or denumerable; and if a
formula is valid in every finite or denumerable domain it is valid in
every domain.

Kripke's 1962 “The Undecidability of Monadic Modal Quantification Theory” develops a parallel between first-order logic with one dyadic predicate and first-order monadic modal logic with just two predicate letters, to prove that this fragment of first-order modal logic is already undecidable.

Of great importance is the paper “Semantical Analysis of Modal
Logic I” (1963a) where normal systems are treated. It is here
that Kripke fully develops the analogy with the algebraic results of
Jónsson and Tarski and proves completeness and decidability for
propositional systems **T**, **S4**,
**S5**, and **B** (the Brouwersche system),
which is here introduced. Kripke claims to have derived on his own the
main theorem of “Boolean Algebras with Operators” by an
algebraic analog of his own semantical methods (69, fn. 2). It is in
this paper that two crucial generalizations of the model theory are
introduced. The first is the new understanding of the elements
*H* of *K* as simple points, not assignments of values.
Once this change is introduced, the models have to be supplemented by
an auxiliary function *Φ* needed to assign values to the
propositional variables relative to worlds. Hence, while in the 1959
model theory “*there can be no two worlds in which the same
truth-value is assigned to each atomic formula* [which] turns out
to be convenient perhaps for **S5**, but it is rather
inconvenient when we treat normal MPC's in general” (1963a, 69),
we can now have world duplicates. What is most important about the
detachment of the elements of *K* from the evaluation function
is that it opens the door to the general consideration of modal frames,
sets of worlds plus a binary relation between them, and the
correspondence of such frames to modal systems. So, the second new
element of the paper, the introduction of a relation *R* between
the elements of *K*, naturally accompanies the first. Let it be
emphasized once again that the idea of a relation between worlds is not
new to Kripke. For example, it is already present as an alternativeness
relation in Montague 1960, Hintikka 1961, and Prior 1962, where the
idea is attributed to Peter Geach.

In 1963a Kripke “asks various questions concerning the
relation *R*” (70). First, he shows that every satisfiable
formula has a connected model, i.e., a model based on a model structure
(*G*, *K*, *R*) where for all
*H*∈*K*, *GR*H*, where *R** is the
ancestral relation corresponding to *R*. Hence, only connected
models need to be considered. Then, Kripke shows the nowadays
well-known results that axiom 4 corresponds to the transitivity of the
relation *R*, that axiom *B* correspond to symmetry, and
that the characteristic axiom of **S5** added to system
**T** corresponds to *R* being an equivalence
relation. Using the method of tableaux, completeness for the modal
propositional systems **T**, **S4**,
**S5**, and **B** *vis-à-vis*
the appropriate class of models (reflexive structures for
**T**) is proved. The decidability of these systems,
including the more complex case of **S4**, is also proved.
(For a more detailed treatment of frames, consult the SEP entry on
Modal Logic.)

In the 1965 paper “Semantical Analysis of Modal Logic
II”, Kripke extends the model theory to treat non-normal modal
systems, including Lewis's **S2** and **S3**.
Though these systems are considered by Kripke to be somewhat unnatural,
their model theory is deemed elegant. Completeness and decidability
results are proved, including the completeness of **S2**
and **S3**, and the decidability of **S3**.
The model theory is extended by the introduction of a new element
*N*⊆*K* in the model structures (*G*,
*K*, *R*, *N*). *N* is the subset of normal
worlds, i.e., worlds *H* such that *HRH*. Another
interesting aspect of the non-normal systems is that in the model
theoretic results that pertain to them, *G* (the actual world)
plays an essential role. Instead, the rule of necessitation that
applies to normal systems makes the choice of *G* model
theoretically irrelevant.

In 1963b, “Semantical Considerations on Modal Logic”,
Kripke introduces a new generalization to the models of quantified
modal systems. In 1959 a model was defined in a domain *D*. The
result was that all worlds in one model have the same cardinality. In
1963b models are not given in a domain, hence worlds in the same model
can be assigned different domains by a function *Ψ* that
assigns domains to the elements *H* of *K*. Given the
variability of domains across worlds, Kripke can now construct
counter-examples to both the Barcan Formula
(∀*x*)□*Fx*→□(∀*x*)*Fx* and its converse
□(∀*x*)*Fx*→(∀*x*)□*Fx*. The Barcan formula can be falsified in structures with growing
domains. For example, a model with two worlds, *G* and one other
possible world *H* extending it. The domain of *G* is
{*a*} and *Fa* is true in *G*. The domain of
*H* is the set {*a*, *b*} and *Fa* is true
in *H* but *Fb* is not true in *H*. In this model
(∀*x*)□*Fx* but not
□(∀*x*)*Fx* is true in *G*. To
disprove the converse of the Barcan formula we need models with
decreasing domains. For example, a model with two worlds *G* and
*H*, where the domain of *G* is {*a*, *b*}
and the domain of *H* is {*a*}, with *Fa* and
*Fb* true in *G*, *Fa* true in *H*, but
*Fb* false in *H*. This model requires that we assign a
truth-value to the formula *Fb* in the world *H* where
the individual *b* does not exist (is not in the domain of
*H*). Kripke points out that from a model theoretical point of
view this is just a technical choice.

Kripke reconstructs a proof of the converse Barcan formula in
quantified **T** and shows that the proof goes through
only by allowing the necessitation of a sentence containing a free
variable. But if free variables are instead to be considered as
universally bound, this step is illicit. Necessitating directly an open
formula, without first closing it, amounts to assuming what is to be
proved. Prior 1956 contains a proof of the Barcan formula. Kripke does
not discuss the details of Prior's proof. Prior's proof for the Barcan
formula adopts Łukasiewicz's rules for the introduction of the
existential quantifier. The second of these rules states that if
⊢*A*→*B* then ⊢*A*→(∃*x*)*B*. Prior uses the rule to derive
⊢◊*Fx*→(∃*x*)◊*Fx* from
⊢◊*Fx*→◊*Fx*. This seems to us to be
the ‘illegitimate’ step in the proof, since
◊*Fx*→(∃*x*)◊*Fx* does not hold
in a model with two worlds *G* and *H*, where the domain
of *G* is {*a*} and the domain of *H* is
{*a*, *b*}, and where *Fa* is false in both
*G* and *H*, but *Fb* is true in *H*. In
this model ◊*Fx* is true but
(∃*x*)◊*Fx* is false in *G*. In this
counter-model ◊*Fx* is made true in *G* by the
individual *b* that is not in the domain of *G*. In
general, the rule that if ⊢*A*→*B* then
⊢*A*→(∃*x*)*B* does not preserve
validity if we allow that *Fx* may be made true at a world by an
individual that does not exist there. We conclude that the rule is to
be rejected to preserve the soundness of **S5** relatively
to this model theoretic assumption.

## Bibliography

Please note that the distinction in the bibliography between introductory texts, primary, and secondary literature is partially artificial.

### Introductory Texts

- Blackburn, P., de Rijke, M., and Venema, Y., 2001,
*Modal Logic*, Cambridge: Cambridge University Press. - Chellas, B. F., 1980,
*Modal Logic: an Introduction*, Cambridge: Cambridge University Press. - Fitting, M., and Mendelsohn, R. L., 1998,
*First-Order Modal Logic*, Dordrecht: Kluver Academic Publishers. - Hughes, G. E., and Cresswell, M. J., 1968,
*An Introduction to Modal Logic*, London: Methuen. - Hughes, G. E., and Cresswell, M. J., 1984,
*A Companion to Modal Logic*, London: Methuen. - Hughes, G. E., and Cresswell, M. J., 1996,
*A New Introduction to Modal Logic*, London: Routledge.

### Primary Literature

- Alban, M. J., 1943, “Independence of the Primitive Symbols of
Lewis's Calculi of Propositions”,
*Journal of Symbolic Logic*, 8: pp. 25–26. - Anderson, A. R., 1957, “Independent Axiom Schemata for Von
Wright's M”,
*Journal of Symbolic Logic*, 22: pp. 241–244. - Barcan (Marcus), R., 1946a, “A Functional Calculus of First
Order Based on Strict Implication,”
*Journal of Symbolic Logic*, 11: pp. 1–16. - –––, 1946b, “The Deduction Theorem in a
Functional Calculus of First Order Based on Strict Implication”,
*Journal of Symbolic Logic*, 11: pp. 115–118. - –––, 1947, “The Identity of Individuals in
a Strict Functional Calculus of Second Order”,
*Journal of Symbolic Logic*, 12: pp. 12–15. - Bayart, A., 1958, “Correction de la Logique Modal du Premier
et du Second Ordre S5”,
*Logique et Analyse*, 1: pp. 28–45. - –––, 1959, “Quasi-Adéquation de la
Logique Modal du Second Ordre S5 et Adéquation de la Logique
Modal du Premier Ordre S5”,
*Logique et Analyse*, 2: pp. 99–121. - Becker, O., 1930, “Zur Logik der Modalitäten”,
*Jahrbuch für Philosophie und Phänomenologische Forschung*, 11: pp. 497–548. - Bennett, J., 1954, “Meaning and Implication”,
*Mind*, 63: pp. 451–463. - Bernays, P., 1926, “Axiomatische Untersuchung des
Aussagenkalküls der
*Principia Mathematica*”,*Mathematische Zeitschrift*, 25: pp. 305–320. - –––, 1948, “Review of Rudolf Carnap's
‘Modalities and Quantification’”,
*Journal of Symbolic Logic*, 13: pp. 218–219. - –––, 1950, “Review of Rudolf Carnap's
*Meaning and Necessity*”,*Journal of Symbolic Logic*, 14: pp. 237–241. - Bull, R. A., 1964, “A Note on the Modal Calculi S4.2 and
S4.3”,
*Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 10: pp. 53–55. - –––, 1965, “An Algebraic Study of Diodorean
Modal Systems”,
*Journal of Symbolic Logic*, 30: pp. 58–64. - –––, 1966, “Than All Normal Extensions of
S4.3 Have the Finite Model Property”,
*Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 12: pp. 341–344. - –––, 1968, “An Algebraic Study of Tense
Logics with Linear Time”,
*Journal of Symbolic Logic*, 33: pp. 27–38. - Carnap, R., 1946, “Modalities and Quantification”,
*Journal of Symbolic Logic*, 11: pp. 33–64. - –––, 1947,
*Meaning and Necessity*, Chicago: University of Chicago Press. 2^{nd}edition with supplements 1956. - –––, 1963a, “My Conception of the Logic of
Modalities”, in
*The Philosophy of Rudolf Carnap*, in*The Library of Living Philosophers*, Vol. 11, P. A. Schlipp (ed.), La Salle: Open Court, pp. 889–900. - –––, 1963b, “My Conception of
Semantics”, in
*The Philosophy of Rudolf Carnap*, in*The Library of Living Philosophers*, Vol. 11, P. A. Schlipp (ed.), La Salle: Open Court, pp. 900–905. - Dugundji, J., 1940, “Note on a Property of Matrices for Lewis
and Langford's Calculi of Propositions”,
*Journal of Symbolic Logic*, 5: pp. 150–151. - Dummett, M. A. E., and Lemmon, E. J., 1959, “Modal Logics
between S4 and S5”,
*Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 5: pp. 250–264. - Feys, R., 1937, “Les Logiques Nouvelles des
Modalités”,
*Revue Néoscolastique de Philosophie*, 40: pp. 517–553. - –––, 1963, “Carnap on Modalities”, in
*The Philosophy of Rudolf Carnap*, in*The Library of Living Philosophers*, Vol. 11, P. A. Schlipp (ed.), La Salle: Open Court, pp. pp. 283–297. - –––, 1965,
*Modal Logics*, in*Collection de Logique Mathématique*, Vol. 4, J. Dopp (ed.), Louvain: E. Nauwelaerts. - Gödel, K., 1933, “Eine Interpretation des
Intuitionistischen Aussagenkalküls”,
*Ergebnisse eines Mathematischen Kolloquiums*, 4: pp. 39–40. English translation “An Interpretation of the Intuitionistic Propositional Calculus”, with an introductory note by A. S. Troelstra, in*Kurt Gödel. Collected Works*, Vol. 1:*Publications 1929–1936*, S. Feferman, J. W. Dawson, S. C. Kleene, G. H. Moore, R. M. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press, 1986, pp. 296–303. - Halldén, S., 1948, “A Note Concerning the Paradoxes of
Strict Implication and Lewis's System S1”,
*Journal of Symbolic Logic*, 13: pp. 138–139. - –––, 1950, “Results Concerning the Decision
Problem of Lewis's Calculi S3 and S6”,
*Journal of Symbolic Logic*, 14: pp. 230–236. - Hintikka, J., 1961, “Modalities and Quantification”,
*Theoria*, 27: pp. 119–28. Expanded version in Hintikka 1969: pp. 57–70. - –––, 1963, “The Modes of Modality”,
*Acta Philosophica Fennica*, 16: pp. 65–81. Reprinted in Hintikka 1969: pp. 71–86. - –––, 1969,
*Models for Modalities*, Dordrecht: D. Reidel. - Jónsson, B., and Tarski, A., 1951, “Boolean Algebras
with Operators. Part I”,
*American Journal of Mathematics*, 73: pp. 891–939. - Jónsson, B., and Tarski, A., 1952, “Boolean Algebras
with Operators. Part II”,
*American Journal of Mathematics*, 74: pp. 127–162. - Kanger, S., 1957,
*Provability in Logic*, in*Acta Universitatis Stockholmiensis, Stockholm Studies in Philosophy*, Vol. 1, Stockholm: Almqvist and Wiksell. - Kripke, S. A., 1959a, “A Completeness Theorem in Modal
Logic”,
*Journal of Symbolic Logic*, 24: pp. 1–14. - –––, 1959b, “Semantical Analysis of Modal
Logic (abstract)”,
*Journal of Symbolic Logic*, 24: pp. 323–324. - –––, 1962, “The Undecidability of Monadic
Modal Quantification Theory”,
*Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 8: pp. 113–116. - –––, 1963a, “Semantical Analysis of Modal
Logic I. Normal Modal Propositional Calculi”,
*Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 9: pp. 67–96. - –––, 1963b, “Semantical Considerations on
Modal Logic”,
*Acta Philosophica Fennica*, 16: pp. 83–94. - –––, 1965, “Semantical Analysis of Modal
Logic II. Non-normal Modal Propositional Calculi”, in
*Symposium on the Theory of Models*, J. W. Addison, L. Henkin, and A. Tarski (eds.), Amsterdam: North-Holland, pp. 206–220. - –––, 1967a, “Review of Lemmon
(1966a)”,
*Mathematical Reviews*, 34: pp. 1021–1022. - –––, 1967b, “Review of Lemmon
(1966b)”,
*Mathematical Reviews*, 34: 1022. - Lemmon, E. J., 1957, “New Foundations for Lewis Modal
Systems”,
*Journal of Symbolic Logic*, 22: pp. 176–186. - –––, 1966a, “Algebraic Semantics for Modal
Logics I”,
*Journal of Symbolic Logic*, 31: pp. 46–65. - –––, 1966b, “Algebraic Semantics for Modal
Logics II”,
*Journal of Symbolic Logic*, 31: pp. 191–218. - Lemon, E. J. (with D. Scott), 1977,
*The “Lemmon Notes”. An Introduction to Modal Logic*, Vol. 11 of*American Philosophical Quarterly Monograph Series*, K. Segerberg (ed.), Oxford: Basil Blackwell. - Lewis, C. I., 1912, “Implication and the Algebra of
Logic”,
*Mind*, 21: pp. 522–531. - –––, 1914, “The Calculus of Strict
Implication”,
*Mind*, 23: pp. 240–247. - –––, 1918,
*A Survey of Symbolic Logic*, Berkeley: University of California Press. - –––, 1920, “Strict Implication—An
Emendation”,
*Journal of Philosophy, Psychology and Scientific Methods*, 17: pp. 300–302. - Lewis, C. I., and Langford, C. H., 1932,
*Symbolic Logic*, London: Century. 2^{nd}edition 1959, New York: Dover. - Łukasiewicz, J., 1920, “O Logice
Trójwartościowej”,
*Ruch Filozoficzny*, 5: pp. 170–171. - –––, 1930, “Philosophische Bemerkungen zu
Mehrwertigen Systemen des Aussagenkalküls”,
*Comptes Rendus des Séances de la Société des Sciences et des Lettres de Varsovie*, 23: pp. 51–77. Translated and reprinted in Łukasiewicz, J., 1970, pp. 153–178. - –––, 1970,
*Selected Works*, L. Borkowski (ed.), Amsterdam: North-Holland. - Łukasiewicz, J., and Tarski, A., 1931,“Investigations
into the Sentential Calculus”, in Tarski, A., 1956,
*Logic, Semantics, Metamathematics*, Oxford: Clarendon Press, pp. 38–59. - MacColl, H., 1880, “Symbolical Reasoning”,
*Mind*, 5: pp. 45–60. - –––, 1897, “Symbolical Reasoning
(II)”,
*Mind*, 6: pp. 493–510. - –––, 1900, “Symbolical Reasoning
(III)”,
*Mind*, 9: pp. 75–84. - –––, 1906,
*Symbolic Logic and its Applications*, London: Longmans, Green, and Co.. - Makinson, D. C., 1966a, “How Meaningful are Modal
Operators?”,
*Australasian Journal of Philosophy*, 44: pp. 331–337. - –––, 1966b, “On Some Completeness Theorems
in Modal logic”,
*Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 12: pp. 379–384. - McKinsey, J. C. C., 1934, “A Reduction in Number of the
Postulates for C. I. Lewis' System of Strict Implication”,
*Bulletin (New Series) of the American Mathematical Society*, 40: pp. 425–27. - –––, 1941, “A Solution of the Decision
Problem for the Lewis Systems S2 and S4, with an Application to
Topology”,
*Journal of Symbolic Logic*, 6: pp. 117–134. - –––, 1944, “On the Number of Complete Extensions of the Lewis Systems of Sentential Calculus”, 9: pp. 42–45.
- –––, 1945, “On the Syntactical Construction
of Systems of Modal Logic”,
*Journal of Symbolic Logic*, 10: pp. 83–94. - McKinsey, J. C. C., and Tarski, A., 1944, “The Algebra of
Topology”,
*Annals of Mathematics*, 45: pp. 141–191. - –––, 1946, “On Closed Elements in Closure
Algebras”,
*Annals of Mathematics*, 47: pp. 122–162. - –––, 1948, “Some Theorems about the
Sententional Calculi of Lewis and Heyting”,
*Journal of Symbolic Logic*, 13: pp. 1–15. - Montague, R., 1960, “Logical Necessity, Physical Necessity,
Ethics, and Quantifiers”,
*Inquiry*, 3: pp. 259–269. - Nelson, E. J., 1930, “Intensional Relations”,
*Mind*, 39: pp. 440–453. - Parry, W. T., 1934, “The Postulates for Strict
Implication”,
*Mind*, 43: pp. 78–80. - –––, 1939, “Modalities in the Survey System
of Strict Implication”,
*Journal of Symbolic Logic*, 4: pp. 137–154. - Prior, A. N., 1955,
*Formal Logic*, Oxford: Clarendon Press. - –––, 1956, “Modality and Quantification in
S5”,
*Journal of Symbolic Logic*, 21: pp. 60–62. - –––, 1957,
*Time and Modality*, Oxford: Clarendon Press. - Prior, A. N., 1962, “Possible Worlds”,
*Philosophical Quarterly*, 12: pp. 36–43. - Prior, A. N., and Fine, K., 1977,
*Worlds, Times and Selves*, Amherst: University of Massachusetts Press. - Quine, W. V., 1947a, “The Problem of Interpreting Modal
Logic”,
*Journal of Symbolic Logic*, 12: pp. 43–48. - –––, 1947b, “Review of Barcan
(1946b)”,
*Journal of Symbolic Logic*, 12: pp. 95–96. - –––, 1970,
*Philosophy of Logic*, Cambridge, Massachusetts: Harvard University Press. - Russell, B., 1906, “Review of MacColl (1906)”,
*Mind*, 15: pp. 255–260. - Scroggs, S. J., 1951, “Extensions of the Lewis System
S5”,
*Journal of Symbolic Logic*, 16: pp. 112–120. - Segerberg, K., 1968, “Decidability of S4.1”,
*Theoria*, 34: pp. 7–20. - –––, 1971,
*An Essay in Classical Modal Logic*, Vols. 1, 2, 3,*Filosofiska Studier*, 13, Uppsala: Uppsala Universitet. - Simons, L., 1953, “New Axiomatizations of S3 and S4”,
*Journal of Symbolic Logic*, 18: pp. 309–316. - Sobociński, B., 1953, “Note on a Modal System of
Feys-von Wright”,
*Journal of Computing Systems*, 1: pp. 171–178. - –––, 1962, “A Contribution to the
Axiomatization of Lewis' System S5”,
*Notre Dame Journal of Formal Logic*, 3: pp. 51–60. - Strawson, P. F., 1948, “Necessary Propositions and
Entailment-Statements”,
*Mind*, 57: pp. 184–200. - Thomason, R. H., 1973, “Philosophy and Formal
Semantics”, in
*Truth, Syntax and Modality*, H. Leblanc (ed.), Amsterdam: North-Holland, pp. 294–307. - Thomason, S. K., 1973, “A New Representation of S5”,
*Notre Dame Journal of Formal Logic*, 14: pp. 281–284. - van Benthem, J., 1984, “Possible Worlds Semantics: A Research
Program that Cannot Fail?”,
*Studia Logica*, 43: pp. 379–393. - von Wright, G. H., 1951,
*An Essay in Modal Logic*, Vol. V of*Studies in Logic and the Foundations of Mathematics*, L. E. J. Brouwer, E. W. Beth, and A. Heyting (eds.), Amsterdam: North-Holland. - Whitehead, A. N., and Russell, B., 1910,
*Principia Mathematica*, Volume I, Cambridge: Cambridge University Press.

### Secondary Literature

- Ballarin, R., 2005, “Validity and Necessity”,
*Journal of Philosophical Logic*, 34: pp. 275–303. - Belnap, N. D., Jr., 1981, “Modal and Relevance Logics:
1977”, in
*Modern Logic–A Survey*, E. Agazzi (ed.), Dordrecht: D. Reidel, pp. 131–151. - Blackburn, P., van Benthem, J., and Wolter, F., eds, 2007,
*Handbook of Modal Logic*, in*Studies in Logic and Practical Reasoning*, Vol. 3, Amsterdam: Elsevier. - Bull, R., and Segerberg, K., 1984, “Basic Modal Logic”,
in
*Handbook of Philosophical Logic*, in*Extensions of Classical Logic*, Vol. 2, D. M. Gabbay and F. Guenthner (eds.), Dordrecht: Kluwer, pp. 1–88. - Cocchiarella, N., 1975a, “Logical Atomism, Nominalism, and
Modal Logic”,
*Synthese*, 31: pp. 23–62. - –––, 1975b, “On the Primary and Secondary
Semantics of Logical Necessity”,
*Journal of Philosophical Logic*, 4: pp. 13–27. - Copeland, B. J., 2002, “The Genesis of Possible Worlds
Semantics”,
*Journal of Philosophical Logic*, 31: pp. 99–137. - Curley, E. M., 1975, “The Development of Lewis' Theory of
Strict Implication”,
*Notre Dame Journal of Formal Logic*, 16: pp. 517–527. - Goldblatt, R., 2003, “Mathematical Modal Logic: A View of its
Evolution”, in
*Handbook of the History of Logic*, in*Logic and the Modalities in the Twentieth Century*, Vol. 7, D. M. Gabbay and J. Woods (eds.), Amsterdam: Elsevier, pp. 1–98. - Kaplan, D., 1966, “Review of Kripke (1963a)”,
*Journal of Symbolic logic*, 31: pp. 120–122. - –––, “Opacity”, in L. E. Hahn and P.
A. Schilpp (eds.),
*The Philosophy of W. V. Quine*, in*The Library of Living Philosophers*, Vol. 18, La Salle: Open Court, pp. 229–289. - Lindström, S., 1996, “Modality Without Worlds: Kanger's
Early Semantics for Modal Logic”, in
*Odds and Ends. Philosophical Essays Dedicated to Wlodek Rabinowicz on the Occasion of his Fiftieth Birthday*, S. Lindström, R. Sliwinski, and J. Österberg (eds.), Uppsala, Sweden, pp. 266–284. - –––, 1998, “An Exposition and Development
of Kanger's Early Semantics for Modal Logic”, in
*The New Theory of Reference: Kripke, Marcus, and its Origins*, P. W. Humphreys, and J. H. Fetzer (eds.), Dordrecht: Kluwer, pp. 203–233. - –––, 2001, “Quine's Interpretation Problem
and the Early Development of Possible Worlds Semantics”,
*Uppsala Philosophical Studies*, 50: pp. 187–213. - Linsky, L., (ed.), 1971,
*Reference and Modality*, Oxford: Oxford University Press. - Löb, M. H., 1966, “Extensional Interpretations of Modal
Logic”,
*Journal of Symbolic Logic*, 31: pp. 23–45. - Rahman, S., and Redmond, J., 2007,
*Hugh MacColl: An Overview of his Logical Work with Anthology*, London: College Publications.

## Other Internet Resources

- Basic Concepts in Modal Logic, by Edward N. Zalta
- Logic Systems, by John Halleck
- Modal Logic Handbook, by Blackburn, van Benthem, and Wolter

## Related Entries

actualism | algebra of logic tradition | Boolean algebra: the mathematics of | logic: classical | logic: deontic | logic: hybrid | logic: intensional | logic: many-valued | logic: modal | logic: relevance | logic: temporal | logical consequence: propositional consequence relations and algebraic logic | modality: medieval theories of | possible objects | possible worlds | Prior, Arthur

### Acknowledgements

I would like to thank Max Weiss who has assisted me at different stages of this project.