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



\[\tag{1}
\neg p \rightarrow(p \rightarrow q)
\]


and

 

\[\tag{2}
p \rightarrow(q \rightarrow 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. (1912: 522) 
> 
> 
> 



However, the theorems are inadequate *vis-a-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-a-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:




Axioms for **S1**

 

\[
\begin{align}
\tag{B1}
 (p\wedge q)&\Rightarrow(q\wedge p) \\

\tag{B2}
 (p\wedge q)&\Rightarrow p \\

\tag{B3}
 p&\Rightarrow(p\wedge p) \\

\tag{B4}
 ((p\wedge q)\wedge r)&\Rightarrow(p\wedge(q\wedge r)) \\

\tag{B5}
 p&\Rightarrow \neg \neg p \\

\tag{B6}
 ((p\Rightarrow q)\wedge(q\Rightarrow r)) & \Rightarrow(p\Rightarrow r) \\

\tag{B7}
 (p\wedge(p\Rightarrow q)) & \Rightarrow q \\
\end{align}
\]



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



The rules are (1932: 125-6):




Rules for **S1**



*Uniform Substitution*
  

A valid formula remains valid if a formula is uniformly substituted in
it for a propositional variable.



*Substitution of Strict Equivalents*
  

Either of two strictly equivalent formulas can be substituted for one
another.



*Adjunction*
  

If \(\Phi\) and \(\Psi\) have been inferred, then \(\Phi \wedge \Psi\)
may be inferred.



*Strict Inference*
  

If \(\Phi\) and \(\Phi \Rightarrow \Psi\) have been inferred, then
\(\Psi\) may be inferred.




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

 

\[\tag{B8} 
\Diamond(p\wedge q)\Rightarrow \Diamond p
\]


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

 

\[\tag{A8}
((p\Rightarrow q)\Rightarrow(\neg \Diamond q\Rightarrow \neg \Diamond 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, as reported in Lewis 1932: 496, is
that both Wajsberg and Parry derived in system
**S3**--in its 1918 axiomatization--the
following theorem:

 

 \[(p\Rightarrow q)\Rightarrow((q\Rightarrow r)\Rightarrow(p\Rightarrow 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

 

\[(p\Rightarrow q)\Rightarrow((q\Rightarrow r)\Rightarrow(p\Rightarrow r))\]


can be derived in **S2**.



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



\[\tag{B9}
(\exists p, q)(\neg(p\Rightarrow q)\wedge \neg(p\Rightarrow \neg q))
\]


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:




Three additional axioms

 

\[
\begin{align}
\tag{C10}
 \neg \Diamond \neg p &\Rightarrow \neg \Diamond \neg \neg \Diamond \neg p\\
\tag{C11}
 \Diamond p & \Rightarrow \neg \Diamond \neg \Diamond p\\
\tag{C12}
p&\Rightarrow \neg \Diamond \neg \Diamond p\\
\end{align}
\]



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



Godel 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. Godel adds the following rules and axioms to
the propositional calculus. 

 

\[\begin{align\*}
\tag{Necessitation} \textrm{If } \mvdash \alpha &\textrm{ then } \mvdash \Box \alpha, \\
\tag{Axiom K} \mvdash \Box(p\rightarrow q)&\rightarrow(\Box p\rightarrow \Box q), \\
\tag{Axiom T} \mvdash \Box p&\rightarrow p\textrm{, and} \\
\tag{Axiom 4} \mvdash \Box p&\rightarrow \Box \Box p.\\
\end{align\*}
\]


Initially, Godel 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**. Godel 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. Godel's claim will be proved
algebraically by McKinsey and Tarski (1948). Godel'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 Godel'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
Sobocinski (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 Godel 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 calculus **PC**



PCa
If \(\alpha\) is a tautology, then \(\mvdash \alpha\)
PCb
Substitution for propositional variables
PCc
Material detachment/*Modus Ponens*: if \(\alpha\) and
\(\alpha \rightarrow \beta\) are tautologies, then so is
\(\beta\)



Further rules in Lemmon's system are:



(a)
If \(\mvdash \alpha\) then \(\mvdash \Box \alpha\) (Necessitation)
(a')
If \(\alpha\) is a tautology or an axiom, then \(\mvdash \Box
\alpha\)
(b)
If \(\mvdash \Box(\alpha \rightarrow \beta)\) then \(\mvdash
\Box(\Box \alpha \rightarrow \Box \beta)\)
(b')
Substitutability of strict equivalents.


Further axioms in Lemmon's system are:

 

\[
\begin{align}
\tag{1}
 \Box(p \rightarrow q)&\rightarrow \Box(\Box p\rightarrow \Box q) \\
\tag{\(1'\)}
 \Box(p\rightarrow q)&\rightarrow(\Box p\rightarrow \Box q) &\textrm{(Axiom K)} \\
\tag{2}
 \Box p&\rightarrow p &\textrm{(Axiom T)} \\
\tag{3}
 (\Box(p\rightarrow q)\wedge \Box(q\rightarrow r))&\rightarrow \Box(p\rightarrow r)\\
\end{align}
\]


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 \(\alpha\) is a tautology, then \(\mvdash \Box \alpha\).


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 



\[\mvdash p\Rightarrow \Box \Diamond p \quad\textrm{(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 



\[\mvdash \Diamond p\Rightarrow \Box \Diamond p \quad \textrm{(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)
introduces system **S6** by adding to **S2**
the axiom \(\mvdash \Diamond \Diamond p\). Hallden (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\). Hallden 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 Lukasiewicz 1920 is a
preliminary Polish version of the main ideas of this paper),
Lukasiewicz 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 Lukasiewicz 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 1/2.
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: 

 

\[\begin{align}
\tag{1} \neg \ldots \Diamond p\\
\tag{2} \Diamond \ldots \Diamond p\\
\tag{3} \neg \ldots \Diamond \neg p\\
\tag{4} \Diamond \ldots \neg p.\\
\end{align}\]


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: 

 

\[\mvdash \neg \Diamond \neg \Diamond \neg \Diamond p\Rightarrow \neg \Diamond 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 

 

\[\mvdash \neg \Diamond \neg \Diamond \Diamond p\Rightarrow \neg \Diamond \neg \Diamond 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 (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:


1. if \(x \in D\) and \((x\Rightarrow y) \in D\) and \(y \in K\),
then \(y \in D\),
2. if \(x \in D\) and \(y \in D\), then \(x\times y \in D\),
3. if \(x \in K\) and \(y \in K\) and \(x\Leftrightarrow y \in 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, -, \*,
\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.



Jonsson 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 Jonsson 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. Jonsson 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
Jonsson 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 Jonsson 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 Godel'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:


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



From which it follows that:


3. \(\Box 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, 



 \[\mvDash(\forall x)\Box Fx\leftrightarrow \Box(\forall x)Fx.\]


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**.
Godel 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 naive 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-a-vis*
Carnap's maximal validity. Cocchiarella (1975b) attributes the
result to Richard Montague and Donald Kalish. See also Lindstrom
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, state-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 (1959a) 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 1963a). 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
Lindstrom 1996 and 1998.



Kripke's 1959a "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\in
K, K\) is an *arbitrary* subset of assignments of values to the
formulas of **S5\*\(^=\)**, and all \(H\in K\) agree on
the assignments to individual variables. For each \(H\in 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, \ldots, x\_n)\), \(B\) is assigned \(T\) if and only
if the \(n\)-tuple of elements assigned to \(x\_1\), ..., \(x\_n\)
belongs to the set of \(n\)-tuples of individuals that \(H\) assigns
to \(P. H\) assigns \(T\) to \(\neg B\) if and only if it assigns
\(F\) to \(B. H\) assigns \(T\) to \(B\wedge 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 \((\forall x)Fx\) it is assigned \(T\) if
and only if \(Fx\) is assigned \(T\) for every assignment to \(x\).
\(\Box B\) is assigned \(T\) if and only if \(B\) is assigned \(T\) by
every \(H\in 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. (1959a: 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 Kripke model 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 divergence 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 development, 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. The consideration of arbitrary subsets of possible
worlds, makes it possible for Kripke's model theory to
disconnect 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 \(\Box B, \Box p\)
is false in all the worlds of the maximal model, and \(\Diamond p\) is
true in all of them. If validity is truth in all worlds of this
maximal model, like for Carnap, it follows that \(\mvDash \Diamond
p\), but in **S5** \(\nmvdash\Diamond 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 \(\Box p\), and one which
contains only one world \(H=G\) where \(p\) is false and so is \(\Box
p\) as well as \(\Diamond p\). Thanks to this last model \(\nmvDash
\Diamond p\). Notice that the crucial innovation is the definition of
validity as truth across all subsets of worlds, not just the maximal
subset. The additional fact that validity in a model is defined as
truth at the actual world of the model--as opposed to truth at
all worlds of the model--though revealing of the fact that Kripke
did not link the notion of necessity to the notion of validity, is
irrelevant to this technical result. 



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,
\ldots, A\_n\). The tableau assumes that the formulas \(A\_1, \ldots,
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 \(\neg 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 \(\Box 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\wedge 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, \ldots, A\_n\) is closed if and only (i) in
**S5\*\(^=\)** \(A\_1, \ldots, A\_n\vdash B\) and (ii)
\(A\_1, \ldots, A\_n\vDash 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, \ldots, A\_n\vdash B\) if
and only if \(A\_1, \ldots, A\_n\vDash B\).



The 1959 paper contains also a proof of the modal counterpart of the
Lowenhein-Skolem theorem for first-order logic, according to
which if a formula is satisfiable in a non-empty domain then 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" (Kripke 1963a) where normal systems are treated. It is
here that Kripke fully develops the analogy with the algebraic results
of Jonsson 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 the two additional crucial generalizations of the model theory are
introduced. The first is the new understanding of the elements \(H\)
of \(K\) as simple indices, not assignments of values. Once this
change is introduced, the models have to be supplemented by an
auxiliary function \(\Phi\) 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\)" (1963a: 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\in K\), \(G\mathrel{R\*}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-a-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 somewhat unnatural, their model
theory is deemed elegant. Completeness and decidability results are
proved *vis-a-vis* the proper class of structures,
including the completeness of **S2** and
**S3**, and the decidability of **S3**. To
achieve these results, the model theory is extended by the
introduction of non-normal worlds which do not respect the standard
Leibnizian interpretation of \(\Box\) as truth in every accessible
world, and that make every formula of the form \(\Box B\) false. This
leads to a corresponding revision of the interpretation of \(\Box\),
and to the introduction of a new element \(N\subseteq K\) in the model
structures \((G, K, R, N). N\) is the subset of normal worlds which
respect the standard interpretation of \(\Box\). Non-normal worlds are
needed to prevent the validity of formulas like \(\Box\Box A\) even
when \(\Box A\) is valid, by basically allowing A but not \(\Box A\)
to be true in every world accessible from the actual world and thus
\(\Box A\) but not \(\Box\Box A\) to hold in the actual world. This is
required as the systems under consideration do not have a full rule of
necessitation. 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, in particular in
the **S2** and **S3** model structures the
actual world has to be normal. Instead, the full rule of necessitation
that holds in normal systems eliminates the need of non-normal worlds
and makes the choice of \(G\) model theoretically irrelevant.



The great success of the Kripkean model theory notwithstanding, it is
worth emphasizing that not all modal logics are complete. For
incompleteness results see Makinson 1969, for a system weaker than
**S4**; and Fine 1974, S. Thomason 1974, Goldblatt 1975,
and van Benthem 1978, for systems between **S4** and
**S5**. Some modal formulas impose conditions on frames
that cannot be expressed in a first-order language, thus even
propositional modal logic is fundamentally second-order in nature.
Insofar as the notion of validity on a frame abstracts from the
interpretation function, it implicitly involves a higher-order
quantification over propositions. On the correspondence between frame
validity and second-order logic and on the model-theoretic criteria
that distinguish the modal sentences that are first-order expressible
from those that are essentially second-order see Blackburn and van
Benthem's "Modal Logic: A Semantic Perspective"
(2007a).



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\). As a
result all worlds in one model had 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 \(\Psi\) that assigns
domains to the elements \(H\) of \(K\). Given the variability of
domains across worlds, Kripke can now construct counter-examples both
to the Barcan Formula 

 

\[(\forall x)\Box Fx\rightarrow\Box(\forall x)Fx\]

and its converse

 

\[\Box(\forall x)Fx\rightarrow(\forall x)\Box 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\), but not \(Fb\), is true in \(H\). In this model
\((\forall x)\Box Fx\) but not \(\Box(\forall 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's system has no individual
constants so our explanation is simplified for brevity; for example,
to be exact, we should not say that \(Fb\) is true in \(H\) but rather
that \(Fx\) is so true under the assignment of \(b\) to \(x.\)) 



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. Kripke's remarks constitute an objection not so much
to the rule of Necessitation, but (following Quine) to the theoremhood
of open formulas of first-order logic. Prior 1956 contains a proof of
the Barcan formula in the alternative formulation



\[\Diamond(\exists x)Fx\rightarrow(\exists x)\Diamond Fx.\]


Kripke does not discuss the details of Prior's proof.
Prior's proof for the Barcan formula adopts
Lukasiewicz's rules for the introduction of the existential
quantifier. The second of these rules states that if \(\mvdash
A\rightarrow B\) then \(\mvdash A\rightarrow(\exists x)B\). Prior applies
the rule to 

 

\[\mvdash \Diamond Fx\rightarrow \Diamond Fx\]

and derives



\[\mvdash \Diamond Fx\rightarrow(\exists x)\Diamond Fx\]

which he then necessitates to 

 

\[\mvdash\Box(\Diamond Fx\rightarrow(\exists x)\Diamond Fx).\]


As seen, Kripke objects to the necessitation of open formulas. Indeed,
if open formulas are understood as universally closed, \(\Diamond
Fx\rightarrow(\exists x)\Diamond Fx\) is to be read as \((\forall
x)(\Diamond Fx\rightarrow(\exists x)\Diamond Fx)\) and Prior's
proof will not go through. On the other hand, the open formula
\(\Diamond Fx\rightarrow(\exists x)\Diamond Fx\) is already
'problematic' insofar as it 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 \(\Diamond
Fx\) is true but \((\exists x)\Diamond Fx\) is false in \(G\). In this
counter-model \(\Diamond Fx\) is made true in \(G\) by the individual
\(b\) that is not in the domain of \(G\). 



In general, Existential Generalization, for example in the form of
Lukasiewicz's rule that if \(\mvdash A\rightarrow B\) then
\(\mvdash A\rightarrow(\exists 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. When discussing the Converse of the Barcan
Formula, Kripke blamed the Necessitation of open formulas, though
suggesting that the problem lies not so much in the rule of
Necessitation but rather in the alleged theoremhood of the open
formulas to which it is applied, and by extension in the validity of
the rules of existential generalization and universal
instantiation. Kripke's discussion of this question is limited,
also because his modal systems do not employ individual constants,
which would reinstate the possibility of proving both the Barcan
Formula and its Converse without employing theorems with free
variables. 



The discussion of the Barcan Formula and its Converse has accompanied
the development of quantified modal logic, as these formulas are
linked both to the technical questions of how to combine Classical
Quantification Theory with Modal Logic and how to define validity for
quantified modal systems, as well as to the philosophical questions
surrounding the variability of domains and the interpretations of the
quantifiers. Proof theoretically, the most straightforward combination
of classical quantification theory and modal logic makes both the
Barcan Formula and its Converse theorems. Model theoretically,
intra-model domain variability is a welcome generalization. We do not
discuss here the technical solutions open to logicians who wish to
build systems sound for variable domains, that is, systems that, like
Kripke's, do not allow proofs of the Barcan and its Converse
(Deutsch 1994 and Linsky and Zalta 1994 contain useful overviews of
the various technical options; see also the SEP entry on the
possibilism-actualism debate).