Syntax and Semantics

Primitive symbols of the basic modal language

The basic language of modal logic contains

1. The propositional constant for falsity $\lfalse$source.

2. A denumerables set of propositional variables: $\Obj p_0$source, $\Obj p_1$source, $\Obj p_2$source, dots

3. The propositional connectives: $\lnot$source (negation) , $\land$source (conjunction) , $\lor$source (disjunction) , $\lif$source (conditional) .

4. The modal operator $\Box$source.

5. The modal operator $\Diamond$source.

Inductive definition of basic modal formulas

Formulas of the basic modal language are inductively defined as follows:

1. $\lfalse$source is an atomic formula.

2. Every propositional variable $\Obj p_i$source is an (atomic) formula.

3. If $!A$source is a formula, then $\lnot !A$source is a formula.

4. If $!A$source and $!B$source are formulas, then $(!A \land !B)$source is a formula.

5. If $!A$source and $!B$source are formulas, then $(!A \lor !B)$source is a formula.

6. If $!A$source and $!B$source are formulas, then $(!A \lif !B)$source is a formula.

7. If $!A$source is a formula, then $\Box !A$source is a formula.

8. If $!A$source is a formula, then $\Diamond !A$source is a formula.

9. Nothing else is a formula.

Projected abbreviations for defined modal operators

Formulas constructed using the defined operators are to be understood as follows:

Definition of simultaneous substitution

Where $!A$source is a modal formula all of whose propositional variables are among $p_1$source, dots, $p_n$source, and $!D_1$source, dots, $!D_n$source are also modal formulas, we define $\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source as the result of simultaneously substituting each $!D_i$source for $p_i$source in $!A$source. Formally, this is a definition by induction on $!A$source:

1. Case: $!A \ident \lfalse$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is $\lfalse$source.

2. Case: $!A \ident q$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is $q$source, provided $q \not\ident p_i$source for $i = 1$source, dots, $n$source.

3. Case: $!A \ident p_i$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is $!D_i$source.

4. Case: $!A \ident \lnot !B$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is $\lnot \SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source.

5. Case: $!A \ident (!B \land !C)$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is

   $$(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \land \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).$$source

6. Case: $!A \ident (!B \lor !C)$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is

   $$(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \lor \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).$$source

7. Case: $!A \ident (!B \lif !C)$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is

   $$(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \lif \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).$$source

8. Case: $!A \ident (!B \liff !C)$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is

   $$(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \liff \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).$$source

9. Case: $!A \ident \Box !B$source

   $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is $\Box \SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}.$source

10. Case: $!A \ident \Diamond !B$source

    $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is $\Diamond \SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}.$source

The formula $\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source is called a substitution instance of $!A$source.

Example contrasting simultaneous and iterated substitution

Suppose $!A$source is $p_1 \lif \Box(p_1 \land p_2)$source, $!D_1$source is $\Diamond(p_2 \lif p_3)$source and $!D_2$source is $\lnot\Box p_1$source. Then $\SSubst{!A}{\subst{!D_1}{p_1}, \subst{!D_2}{p_2}}$source is

Definition of a relational modal model

A model for the basic modal language is a triple $\mModel{M} = \tuple{W, R, V}$source, where

1. $W$source is a nonempty set of “worlds,”

2. $R$source is a binary accessibility relation on $W$source, and

3. $V$source is a function assigning to each propositional variable $p$source a set $V(p)$source of possible worlds.

When $Rww'$source holds, we say that $w'$source is accessible from $w$source. When $w \in V(p)$source we say $p$source is true at $w$source.

Inductive definition of truth at a world

Truth of a formula $!A$source at $w$source in a $\mModel M$source, in symbols: $\mSat{M}{!A}[w]$source, is defined inductively as follows:

1. Case: $!A \ident \lfalse$source

   Never $\mSat{M}{\lfalse}[w]$source.

2. $\mSat{M}{p}[w]$source iff $w \in V(p)$source.

3. Case: $!A \ident \lnot !B$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat/{M}{!B}[w]$source.

4. Case: $!A \ident (!B \land !C)$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat{M}{!B}[w]$source and $\mSat{M}{!C}[w]$source.

5. Case: $!A \ident (!B \lor !C)$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat{M}{!B}[w]$source or $\mSat{M}{!C}[w]$source (or both).

6. Case: $!A \ident (!B \lif !C)$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat/{M}{!B}[w]$source or $\mSat{M}{!C}[w]$source.

7. Case: $!A \ident \Box !B$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat{M}{!B}[w']$source for all $w' \in W$source with $Rww'$source.

8. Case: $!A \ident \Diamond !B$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat{M}{!B}[w']$source for at least one $w' \in W$source with $Rww'$source.

Exercise evaluating nine formulas in the simple model

Consider the model of the simple three-world model figure. Which of the following hold?

1. $\mSat{M}{q}[w_1]$source;

2. $\mSat{M}{\lnot q}[w_3]$source;

3. $\mSat{M}{p \lor q}[w_1]$source;

4. $\mSat{M}{\Box (p \lor q)}[w_1]$source;

5. $\mSat{M}{\Box q}[w_3]$source;

6. $\mSat{M}{\Box \bot}[w_3]$source;

7. $\mSat{M}{\Diamond q}[w_1]$source;

8. $\mSat{M}{\Box q}[w_1]$source;

9. $\mSat{M}{\lnot \Box\Box \lnot q}[w_1]$source.

Duality of necessity and possibility

1. $\mSat{M}{\Box !A}[w]$source iff $\mSat{M}{\lnot\Diamond\lnot !A}[w]$source.

2. $\mSat{M}{\Diamond !A}[w]$source iff $\mSat{M}{\lnot\Box\lnot !A}[w]$source.

Proof

1. $\mSat{M}{\lnot\Diamond\lnot !A}[w]$source iff $\mSat/{M}{\Diamond\lnot !A}[w]$source by definition of $\mSat{M}{}[w]$source. $\mSat{M}{\Diamond\lnot !A}[w]$source iff for some $w'$source with $Rww'$source, $\mSat{M}{\lnot !A}[w']$source. Hence, $\mSat/{M}{\Diamond\lnot !A}[w]$source iff for all $w'$source with $Rww'$source, $\mSat/{M}{\lnot !A}[w']$source. We also have $\mSat/{M}{\lnot !A}[w']$source iff $\mSat{M}{!A}[w']$source. Together we have $\mSat{M}{\lnot\Diamond\lnot !A}[w]$source iff for all $w'$source with $Rww'$source, $\mSat{M}{!A}[w']$source. Again by definition of $\mSat{M}{}[w]$source, that is the case iff $\mSat{M}{\Box !A}[w]$source.

2. Exercise.

Exercise completing the modal duality proof

probDiamond Complete the proof of the proposition on duality of necessity and possibility.

Exercise on worlds with matching atoms and successors

Let $\mModel{M} = \tuple{W, R, V}$source be a model, and suppose $w_1, w_2 \in W$source are such that:

1. $w_1 \in V(p)$source if and only if $w_2 \in V(p)$source (for every propositional variable $p$source); and

2. for all $w \in W$source: $Rw_1w$source if and only if $Rw_2w$source.

Using induction on formulas, show that for all formulas $!A$source: $\mSat{M}{!A}[w_1]$source if and only if $\mSat{M}{!A}[w_2]$source.

Exercise on not-possible and necessary-not

prvDiamond Let $\mModel{M} = \tuple{W, R, V}$source. Show that $\mSat{M}{\lnot\Diamond !A}[w]$source if and only if $\mSat{M}{\Box\lnot!A}[w]$source.

Definition of truth throughout a model

A formula $!A$source is true in a model $M = \tuple{W, R, V}$source, written $\mSat{M}{!A}$source, if and only if $\mSat{M}{!A}[w]$source for every $w \in W$source.

Two facts about truth throughout a model

1. If $\mSat{M}{!A}$source then $\mSat/{M}{\lnot !A}$source, but not vice-versa.

2. If $\mSat{M}{!A \lif !B}$source then $\mSat{M}{!A}$source only if $\mSat{M}{!B}$source, but not vice-versa.

Proof

1. If $\mSat{M}{!A}$source then $!A$source is true at all worlds in $W$source, and since $W \neq \emptyset$source, it can't be that $\mSat{M}{\lnot!A}$source, or else $!A$source would have to be both true and false at some world.

   On the other hand, if $\mSat/{M}{\lnot !A}$source then $!A$source is true at some world $w \in W$source. It does not follow that $\mSat{M}{!A}[w]$source for every $w \in W$source. For instance, in the model of the simple three-world model figure, $\mSat/{M}{\lnot p}$source, and also $\mSat/{M}{p}$source.

2. Assume $\mSat{M}{!A \lif !B}$source and $\mSat{M}{!A}$source; to show $\mSat{M}{!B}$source let $w \in W$source be an arbitrary world. Then $\mSat{M}{!A \lif !B}[w]$source and $\mSat{M}{!A}[w]$source, so $\mSat{M}{!B}[w]$source, and since $w$source was arbitrary, $\mSat{M}{!B}$source.

   To show that the converse fails, we need to find a model $\mModel{M}$source such that $\mSat{M}{!A}$source only if $\mSat{M}{!B}$source, but $\mSat/{M}{!A \lif !B}$source. Consider again the model of the simple three-world model figure: $\mSat/{M}{p}$source and hence (vacuously) $\mSat{M}{p}$source only if $\mSat{M}{q}$source. However, $\mSat/{M}{p \lif q}$source, as $p$source is true but $q$source false at $w_1$source.

Exercise evaluating formulas throughout a three-world model

Consider the following model $\mModel{M}$source for the language comprising $p_1$source, $p_2$source, $p_3$source as the only propositional variables:

Are the following formulas and schemas true in the model $\mModel{M}$source, i.e., true at every world in $\mModel{M}$source? Explain.

1. $p\lif \Diamond p$source (for $p$source atomic);

2. $!A\lif \Diamond !A$source (for $!A$source arbitrary);

3. $\Box p \lif p$source (for $p$source atomic);

4. $\lnot p \lif \Diamond \Box p$source (for $p$source atomic);

5. $\Diamond \Box !A$source (for $!A$source arbitrary);

6. $\Box \Diamond p$source (for $p$source atomic).

Explain

Formulas that are true in all models, i.e., true at every world in every model, are particularly interesting. They represent those modal propositions which are true regardless of how $\Box$source and $\Diamond$source are interpreted, as long as the interpretation is “normal” in the sense that it is generated by some accessibility relation on possible worlds. We call such formulas valid. For instance, $\Box(p \land q) \lif \Box p$source is valid. Some formulas one might expect to be valid on the basis of the alethic interpretation of $\Box$source, such as $\Box p \lif p$source, are not valid, however. Part of the interest of relational models is that different interpretations of $\Box$source and $\Diamond$source can be captured by different kinds of accessibility relations. This suggests that we should define validity not just relative to all models, but relative to all models of a certain kind. It will turn out, e.g., that $\Box p \lif p$source is true in all models where every world is accessible from itself, i.e., $R$source is reflexive. Defining validity relative to classes of models enables us to formulate this succinctly: $\Box p \lif p$source is valid in the class of reflexive models.

Definition of validity relative to a class of models

A formula $!A$source is valid in a class $\mClass{C}$source of models if it is true in every model in $\mClass{C}$source (i.e., true at every world in every model in $\mClass{C}$source). If $!A$source is valid in $\mClass{C}$source, we write $\mClass{C} \Entails !A$source, and we write $\Entails !A$source if $!A$source is valid in the class of all models.

Validity is inherited by subclasses

If $!A$source is valid in $\mClass{C}$source it is also valid in each class $\mClass{C}' \subseteq \mClass{C}$source.

Validity is closed under necessitation

If $!A$source is valid, then so is $\Box!A$source.

Proof

Assume $\Entails !A$source. To show $\Entails \Box!A$source let $\mModel{M} = \tuple{W, R, V}$source be a model and $w \in W$source. If $Rww'$source then $\mSat{M}{!A}[w']$source, since $!A$source is valid, and so also $\mSat{M}{\Box!A}[w]$source. Since $\mModel{M}$source and $w$source were arbitrary, $\Entails \Box!A$source.

Exercise proving three valid modal formulas

Show that the following are valid:

1. $\Box p \lif \Box (q \lif p)$source;

2. $\Box \lnot \lfalse$source;

3. $\Box p \lif (\Box q \lif \Box p)$source.

Exercise on validity in singleton and edgeless models

Show that $!A \lif \Box!A$source is valid in the class $\mClass{C}$source of models $\mModel{M} = \tuple{W, R, V}$source where $W = \{w\}$source. Similarly, show that $!B \lif \Box !A$source and $\Diamond !A \lif !B$source are valid in the class of models $\mModel{M} = \tuple{W, R, V}$source where $R = \emptyset$source.

Explain

A modal-free formula is a tautology if it is true under every truth-value assignment. Clearly, every tautology is true at every world in every model. But for formulas involving $\Box$source and $\Diamond$source, the notion of tautology is not defined. Is it the case, e.g., that $\Box p \lor \lnot \Box p$source---an instance of the principle of excluded middle---is valid? The notion of a tautological instance helps: a formula that is a substitution instance of a (non-modal) tautology. It is not surprising, but still requires proof, that every tautological instance is valid.

Definition of a tautological instance

A modal formula $!B$source is a tautological instance if and only if there is a modal-free tautology $!A$source with propositional variables $p_1$source, dots, $p_n$source and formulas $!D_1$source, dots, $!D_n$source such that $!B \ident \SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$source.

Lemma transferring a modal-free valuation into a model

Suppose $!A$source is a modal-free formula whose propositional variables are $p_1$source, dots, $p_n$source, and let $!D_1$source, dots, $!D_n$source be modal formulas. Then for any assignment $\pAssign{v}$source, any model $\mModel{M} = \tuple{W, R, V}$source, and any $w \in W$source such that $\pAssign{v}(p_i) = \True$source if and only if $\mSat{M}{!D_i}[w]$source we have that $\pSat{v}{!A}$source if and only if $\mSat{M}{\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]$source.

Proof

By induction on $!A$source.

1. Case: $!A \ident \lfalse$source

   Both $\pSat/{v}{\lfalse}$source and $\mSat/{M}{\lfalse}[w]$source.

2. Case: $!A \ident p_i$source

   $$\pSat{v}{p_i} \Leftrightarrow {} & \pAssign{v}(p_i) = \True \\ & \qquad \text{by definition of $\pSat{v}{p_i}$}\\ \Leftrightarrow {} & \mSat{M}{!D_i}[w] \\ &\qquad \text{by assumption}\\ \Leftrightarrow {} & \mSat{M}{\SSubst{p_i}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{since $\SSubst{p_i}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \ident !D_i$}.$$source

3. Case: $!A \ident \lnot !B$source

   $$\pSat{v}{\lnot !B} \Leftrightarrow {} & \pSat/{v}{!B}\\ &\qquad \text{by definition of $\pSat{v}{}$};\\ \Leftrightarrow {} & \mSat/{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by induction hypothesis}\\ \Leftrightarrow {} & \mSat{M}{\SSubst{\lnot !B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by definition of $\pSat{v}{}$}.$$source

4. Case: $!A \ident (!B \land !C)$source

   $$\pSat{v}{!B \land !C} \Leftrightarrow {} & \pSat{v}{!B} \text{ and } \pSat{v}{!C}\\ &\qquad \text{by definition of $\pSat{v}{}$}\\ \Leftrightarrow {} & \mSat{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w] \text{ and } \\ & \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by induction hypothesis}\\ \Leftrightarrow{} & \mSat{M}{\SSubst{(!B \land !C)}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by definition of $\mSat{M}{}[w]$}.$$source

5. Case: $!A \ident (!B \lor !C)$source

   $$\pSat{v}{!B \lor !C} \Leftrightarrow{} & \pSat{v}{!B} \text{ or } \pSat{v}{!C}\\ &\qquad \text{by definition of $\pSat{v}{}$};\\ \Leftrightarrow{} & \mSat{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w] \text{ or }\\ & \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by induction hypothesis}\\ \Leftrightarrow{} & \mSat{M}{\SSubst{(!B \lor !C)}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by definition of $\mSat{M}{}[w]$}.$$source

6. Case: $!A \ident (!B \lif !C)$source

   $$\pSat{v}{!B \lif !C} \Leftrightarrow{} & \pSat/{v}{!B} \text{ or } \pSat{v}{!C}\\ &\qquad \text{by definition of $\pSat{v}{}$}\\ \Leftrightarrow{} & \mSat/{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w] \text{ or }\\ & \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by induction hypothesis}\\ \Leftrightarrow{} & \mSat{M}{\SSubst{(!B \lif !C)}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]\\ &\qquad \text{by definition of $\mSat{M}{}[w]$}.$$source

Every tautological instance is valid

All tautological instances are valid.

Proof

Contrapositively, suppose $!A$source is such that $\mSat/{M}{\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}}[w]$source, for some model $\mModel{M}$source and world $w$source. Define an assignment $\pAssign{v}$source such that $\pAssign{v}(p_i) = \True$source if and only if $\mSat{M}{!D_i}[w]$source (and $\pAssign{v}$source assigns arbitrary values to $q \notin \{p_1, \dots, p_n \}$source). Then by the lemma transferring modal-free satisfaction to a substitution instance, $\pSat/{v}{!A}$source, so $!A$source is not a tautology.

Definition of a modal schema

A schema is a set of formulas comprising all and only the substitution instances of some modal formula $!C$source, i.e.,

The formula $!C$source is called the characteristic formula of the schema, and it is unique up to a renaming of the propositional variables. A formula $!A$source is an instance of a schema if it is a member of the set.

Truth and validity of a schema

A schema is true in a model if and only if all of its instances are; and a schema is valid if and only if it is true in every model.

Validity of the K schema

The following schema AxK is valid

Proof

We need to show that all instances of the schema are true at every world in every model. So let $\mModel{M} = \tuple{W,R,V}$source and $w \in W$source be arbitrary. To show that a conditional is true at a world we assume the antecedent is true to show that the consequent is true as well. In this case, let $\mSat{M}{\Box(!A \lif !B)}[w]$source and $\mSat{M}{\Box !A}[w]$source. We need to show $\mSat{M}{\Box !B}[w]$source. So let $w'$source be arbitrary such that $Rww'$source. Then by the first assumption $\mSat{M}{!A \lif !B}[w']$source and by the second assumption $\mSat{M}{!A}[w']$source. It follows that $\mSat{M}{!B}[w']$source. Since $w'$source was arbitrary, $\mSat{M}{\Box !B}[w]$source.

Validity of the Dual schema

The following schema Dual is valid