10 Axiomatic Derivations

We now aim for an alternative characterization of the set of formulas of $L^{◻}$ that are valid in different classes of frames. We will begin with a system K, whose theorems are all and only formulas of $L^{◻}$ that are valid in every frame. We will later consider extensions of that system, whose theorems are all and only formulas valid in every frame in a certain class, e.g., reflexive, symmetric, transitive, etc.

The Minimal Modal Logic K

The system consists of an infinite set of axioms and two rules of inference.

Definition 10.1 (The System K) The minimal modal logic $K$ is an axiom system with an infinite set of axioms and two rules of inference. The axioms of $K$ include:

substitution instances of tautologis of propositional logic
substitution instances of the axiom: $\begin{matrix} (K) & ◻ (p \to q) \to (◻ p \to ◻ q) \end{matrix}$

The rules of inference of $K$ include:

Modus Ponens (MP):

$\begin{matrix} (MP) & φ, (φ \to ψ) / ψ \end{matrix}$

Necessitation (N)

$\begin{matrix} (N) & φ / ◻ φ \end{matrix}$

We explain what is for a finite sequence of formulas to be a proof in the axiom system we just now introduced:

Definition 10.2 (Proof in K) A proof or derivation in the axiom system $K$ is, as usual, a finite sequence of formulas $(χ_{1}, \dots, χ_{n})$ of $L^{◻}$ , each of them

an axiom of $K$
the outcome of an application of MP to two prior formulas
the outcome of an application of N to a prior formula

The theorems of $K$ those formulas of $L^{◻}$ for which there is a proof in the system:

Definition 10.3 (Theorem of K) A formula $φ$ of $L^{◻}$ is a theorem of $K$ , written $⊢_{K} φ$ , if, and only if, some proof in K ends with the formula $φ$ .

The axioms of the minimal modal logic $K$ are valid in all frames, and the rules of inference preserve validity in all frames. So, every theorem of $K$ is valid in every frame.

Example 10.1 A substitution instance of axiom $K$ is valid in all frames. $\begin{matrix} (K) & ◻ (p \to q) \to (◻ p \to ◻ q) \end{matrix}$ Consider a substitution instance of axiom $K$ : $◻ (φ \to ψ) \to (◻ φ \to ◻ ψ) .$ Let $(W, R)$ be a frame and let $(W, R, V)$ be a model based on that frame. We argue that $(W, R, V) ⊨ ◻ (φ \to ψ) \to (◻ φ \to ◻ ψ)$ . To that end, let $w \in W$ and suppose that $(W, R, V), w ⊩ ◻ (φ \to ψ)$ and $(W, R, V), w ⊩ ◻ φ$ . If $u \in W$ is such that $R w u$ , then $(W, R, V), u ⊩ φ \to ψ$ and $(W, R, V) ⊩ φ$ . Therefore, $(W, R, V), u ⊩ ψ$ . Generalizing, we find $(W, R, V), w ⊩ ◻ ψ$ .

How to Construct Proofs

While it is a purely mechanical procedure to check whether a finite sequence of formulas is a proof in a given system, it may take some skill and experience to find one. There is no perfectly general recipe for this, but as a general piece of advice, it helps to spend some time considering the question of why the formula should be valid. Since proofs and theorems of $K$ track validity in all frames, the question of validity may on occasion guide us to a proof.

One important observation at this poins is that we are entitled to propositional inferences within the system. If two formulas are propositionally equivalent, then you should feel free to move from one to the other. Here is a formal justification of that fact.

Proposition 10.1 If $⊢_{K} φ_{1}, \dots, ⊢_{K} φ_{n}$ and $ψ$ is derivable from ${φ_{1}, \dots, φ}$ in propositional logic, then $⊢_{K} ψ$ .

Proof. Given the Deduction Theorem for Propositional Logic, if $ψ$ is derivable from ${φ_{1}, \dots, φ}$ in propositional logic, then $φ_{1} \to (φ_{2} \to (\dots (φ_{n} \to ψ) \dots))$ is a theorem of propositional logic and thus a theorem of $K$ . By repeated applications of Modus Ponens, we infer $⊢_{K} ψ$ .

In what follows, we will use the annotation ‘PL’ to indicate that a line is justified by propositional logic or by propositional logic applied to some prior lines.

Distribution Rules

We are similarly able to justify derived rules of inference, which will help us take a more direct route between two steps in a proof.

Proposition 10.2 If $⊢_{K} φ \to ψ$ , then $⊢_{K} ◻ φ \to ◻ ψ$ .

Proof. We may transform a derivation of $φ \to ψ$ into a derivation of $φ \to ◻ ψ$ . $\begin{array}{lllll} 1 & φ \to ψ & Given \\ 2 & ◻ (φ \to ψ) & RN 1 \\ 3 & ◻ (φ \to ψ) \to (◻ φ \to ◻ ψ) & K [φ / p, ψ / q] \\ 4 & ◻ φ \to ◻ ψ & MP 2, 3 \end{array}$

This justifies a derived rule of inference we annotate RK: $\begin{matrix} (RK) & If ⊢ φ \to ψ then ⊢ ◻ φ \to ◻ ψ \end{matrix}$ We are now able to justify a related rule of inference: $\begin{matrix} (RK ◊) & If ⊢ φ \to ψ then ⊢ ◊ φ \to ◊ ψ \end{matrix}$

Proposition 10.3 If $⊢_{K} φ \to ψ$ , then $⊢_{K} ◊ φ \to ◊ ψ$ .

Proof. We may transform a proof of $φ \to ψ$ into a proof of $◊ φ \to ◊ ψ$ $\begin{array}{lllll} 1 & φ \to ψ & Given \\ 2 & \neg ψ \to \neg φ & PL 1 \\ 3 & ◻ \neg ψ \to ◻ \neg φ & RK 2 \\ 4 & \neg ◻ \neg φ \to \neg ◻ \neg ψ & PL 3 \\ 7 & ◊ φ \to ◊ ψ & Def ◊ 4 \end{array}$

More generally, if $Q$ is a string of modal operators, we are in a position to justify the derived rule of inference:

$\begin{matrix} (RKQ) & If ⊢_{K} φ \to ψ then ⊢_{K} Q φ \to Q ψ \end{matrix}$

Example 10.2 Consider the derived rule of inference:

\begin{matrix} (RK ◻ ◊) & If ⊢_{K} φ \to ψ then ⊢_{K} ◻ ◊ φ \to ◻ ◊ ψ \end{matrix}

We may transform a derivation of

φ \to ψ

into a derivation of

◻ ◊ φ \to ◻ ◊ ψ

\begin{array}{lllll} 1 & φ \to ψ & Given \\ 2 & ◊ φ \to ◊ ψ & RK ◊ 1 \\ 3 & ◻ ◊ φ \to ◻ ◊ ψ & RK 2 \end{array}

Some Theorems of K

We may exploit some of these derived rules in order to prove some theorems of $K$ .

Proposition 10.4 $⊢_{K} ◻ (φ \to ψ) \to (◊ φ \to ◊ ψ)$

Proof. $\begin{array}{lllll} 11 & (φ \to ψ) \to (\neg ψ \to \neg φ) & PL \\ 2 & ◻ (φ \to ψ) \to ◻ (\neg ψ \to \neg φ) & RK 1 \\ 3 & ◻ (\neg ψ \to \neg φ) \to (◻ \neg ψ \to ◻ \neg φ) & K [\neg ψ / p, \neg φ / q] \\ 4 & (◻ \neg ψ \to ◻ \neg φ) \to (\neg ◻ \neg φ \to \neg ◻ \neg ψ) & PL \\ 5 & ◻ (φ \to ψ) \to (\neg ◻ \neg φ \to \neg ◻ \neg ψ) & PL 2, 3, 4 \\ 6 & ◻ (φ \to ψ) \to (◊ φ \to ◊ ψ) & Def ◊ 6 \end{array}$

Example 10.3 Given those observations, it is simple to justify:

$⊢_{K} ◊ p \land ◻ (p \to q) \to ◊ q$

The crucial observation is that the formula $◊ p \land ◻ (p \to q) \to ◊ q$ is propositionally equivalent to $◻ (p \to q) \to (◊ p \to ◊ q)$ . So, a proof of the latter immediately gives us a proof of the former.

Other well-known theorems of the minimal logic K are principles such as the distribution of $◻$ over $\land$ and the distribution of $◊$ over $\lor$ .

Proposition 10.5 $⊢_{K} ◻ (φ \land ψ) \to (◻ φ \land ◻ ψ)$

Proof. The key to this proof is to find appropriate tautologies on which to apply a distribution rule. $\begin{array}{lllll} 1 & (φ \land ψ) \to φ & PL \\ 2 & ◻ (φ \land ψ) \to ◻ φ & RK 1 \\ 3 & (φ \land ψ) \to ψ & PL \\ 4 & ◻ (φ \land ψ) \to ◻ ψ & RK 3 \\ 5 & ◻ (φ \land ψ) \to (◻ φ \land ◻ ψ) & PL 2, 4 \end{array}$

Proposition 10.6 $⊢_{K} (◻ φ \land ◻ ψ) \to ◻ (φ \land ψ)$

Proof. This proof combines the use of a distribution rule with an instance of K. $\begin{array}{lllll} 1 & φ \to (ψ \to (φ \land ψ)) & PL \\ 2 & ◻ φ \to ◻ (ψ \to (φ \land ψ)) & RK 1 \\ 3 & ◻ (ψ \to (φ \land ψ)) \to (◻ ψ \to ◻ (φ \land ψ)) & K [ψ / p, (φ \land ψ) / q] \\ 4 & ◻ φ \to (◻ ψ \to ◻ (φ \land ψ)) & PL 2, 3 \\ 5 & (◻ φ \land ◻ ψ) \to ◻ (φ \land ψ) & PL 4 \end{array}$

Proposition 10.7 $⊢_{K} (◊ φ \lor ◊ ψ) \to ◊ (φ \lor ψ)$

Proof. The strategy behind the proof is to exploit the fact that $◊$ is a dual of $◻$ , that is, $◊$ is $\neg ◻ \neg$ , and the fact that the negation of a disjunction is propositionally equivalent to a conjunction of negations. When we combine them with the fact that $◻$ distributes over $\land$ , we have a proof ot the principle.

$\begin{array}{lllll} 1 & \neg ◊ (φ \lor ψ) \to \neg \neg ◻ \neg (φ \lor ψ) & Def ◊ \\ 2 & \neg ◊ (φ \lor ψ) \to ◻ \neg (φ \lor ψ) & PL 1 \\ 3 & \neg (φ \lor ψ) \to (\neg φ \land \neg ψ) & PL \\ 4 & ◻ \neg (φ \lor ψ) \to ◻ (\neg φ \land \neg ψ) & RK 3 \\ 5 & ◻ (\neg φ \land \neg ψ) \to (◻ \neg φ \land ◻ \neg ψ) & Prop 7.5 \\ 6 & (◻ \neg φ \land ◻ \neg ψ) \to \neg (\neg ◻ \neg φ \lor \neg ◻ \neg ψ) & PL \\ 7 & \neg (\neg ◻ \neg φ \lor \neg ◻ \neg ψ) \to \neg (◊ φ \lor ◊ ψ) & Def ◊ \\ 8 & ◻ \neg (φ \lor ψ) \to \neg (◊ φ \lor ◊ ψ) & PL 5, 6, 7 \\ 9 & \neg ◊ (φ \lor ψ) \to \neg (◊ φ \lor ◊ ψ) & PL 2, 8 \\ 10 & (◊ φ \lor ◊ ψ) \to ◊ (φ \lor ψ) & PL 9 \end{array}$

Proposition 10.8 $⊢_{K} ◊ (φ \lor ψ) \to (◊ φ \lor ◊ ψ)$

Proof. This time we exploit the fact that a conjunction of necessitations entails the necessitation of a conjunction. $\begin{array}{lllll} 1 & \neg (◊ φ \lor ◊ ψ) \to \neg (\neg ◻ \neg φ \lor \neg ◻ \neg ψ) & Def ◊ \\ 2 & \neg (\neg ◻ \neg φ \lor \neg ◻ \neg ψ) \to (◻ \neg φ \land ◻ \neg ψ) & PL \\ 3 & (◻ \neg φ \land ◻ ψ) \to ◻ (\neg φ \land \neg ψ) & Prop 7.6 \\ 4 & \neg (◊ φ \lor ◊ ψ) \to ◻ (\neg φ \land \neg ψ) & PL 1, 2, 3 \\ 5 & (\neg φ \land \neg ψ) \to \neg (φ \lor ψ) & PL \\ 6 & ◻ (\neg φ \land \neg ψ) \to ◻ \neg (φ \lor ψ) & RK 5 \\ 7 & \neg (◊ φ \lor ◊ ψ) \to ◻ \neg (φ \lor ψ) & PL 4, 6 \\ 8 & ◻ \neg (φ \lor ψ) \to \neg \neg ◻ \neg (φ \lor ψ) & PL \\ 9 & \neg \neg ◻ \neg (φ \lor ψ) \to \neg ◊ (φ \lor ψ) & Def ◊ \\ 10 & \neg (◊ φ \lor ◊ ψ) \to \neg ◊ (φ \lor ψ) & PL 7, 8, 9 \\ 11 & ◊ (φ \lor ψ) \to (◊ φ \lor ◊ ψ) & PL 10 \end{array}$

We conclude with another helpful theorem of K.

Proposition 10.9 $⊢_{K} (◊ φ \land ◻ ψ) \to ◊ (φ \land ψ)$

Proof. $\begin{array}{lllll} 1 & \neg (φ \land ψ) \to (ψ \to \neg φ) & PL \\ 2 & ◻ \neg (φ \land ψ) \to ◻ (ψ \to \neg φ) & RK 1 \\ 3 & ◻ (ψ \to \neg φ) \to (◻ ψ \to ◻ \neg φ) & K [ψ / p, \neg φ / q] \\ 4 & ◻ \neg (φ \land ψ) \to (◻ ψ \to ◻ \neg φ) & PL 2, 3 \\ 5 & \neg (◻ ψ \to ◻ \neg φ) \to \neg ◻ \neg (φ \land ψ) & PL 4 \\ 6 & \neg (◻ ψ \to ◻ \neg φ) \to ◊ (φ \land ψ) & Def ◊ \\ 7 & (◻ ψ \land \neg ◻ \neg φ) \to \neg (◻ ψ \to ◻ \neg φ) & PL \\ 8 & (◻ ψ \land \neg ◻ \neg φ) \to ◊ (φ \land ψ) & PL 6, 7 \\ 9 & (◻ ψ \land ◊ φ) \to (◻ ψ \land \neg ◻ \neg φ) & Def ◊ \\ 10 & (◊ φ \land ◻ ψ) \to (◻ ψ \land ◊ φ) & PL \\ 11 & (◊ φ \land ◻ ψ) \to ◊ (φ \land ψ) & PL 8, 9, 10 \end{array}$

Part of the interest of the minimal modal logic $K$ is that it provides an alternative characterization of the set of validities in all frames. That is, we will eventually prove that a formula $φ$ of $L^{◻}$ is a theorem of $K$ if, and only if, $φ$ is valid in all frames. Before we do, however, we will consider some extensions of the minimal modal logic.

Normal Modal Systems

We will focus on extensions of the minimal modal logic that result from $K$ when we supplement its axioms with all substitution instances of further modal axioms.

Definition 10.4 (Normal Modal Logic) A normal modal $Σ$ logic is an axiom system, which results from $K$ when we add to its axioms all substitution instances of further modal axioms.

Example 10.4 The modal logic $K T$ is the system which results from the minimal modal logic $K$ when we supplement its axioms with all substitution instances of the axiom: $\begin{matrix} (T) & ◻ p \to p \end{matrix}$ The theorems of the normal modal logic $K T$ those formulas of $L^{◻}$ for which there is a proof in the system $K T$ . We write $⊢_{K T} φ$ to indicate that $φ$ is a theorem of $T$ .

Two notable normal modal systems are $S 4$ and $S 5$ , respectively:

Example 10.5 The modal logic $S 4$ is the system which results from the minimal modal logic $K$ when we supplement its axioms with all substitution instances of the axioms: $\begin{matrix} (T) & ◻ p \to p \end{matrix}$ $\begin{matrix} (4) & ◻ p \to ◻ ◻ p \end{matrix}$ The theorems of the normal modal logic $S 4$ those formulas of $L^{◻}$ for which there is a proof in the system $S 4$ . We write $⊢_{S 4} φ$ to indicate that $φ$ is a theorem of $T$ .

Example 10.6 The modal logic $S 5$ is the system which results from the minimal modal logic $K$ when we supplement its axioms with all substitution instances of the axioms: $\begin{matrix} (T) & ◻ p \to p \end{matrix}$ $\begin{matrix} (5) & ◊ p \to ◻ ◊ p \end{matrix}$ The theorems of the normal modal logic $S 5$ those formulas of $L^{◻}$ for which there is a proof in the system $S 5$ . We write $⊢_{S 5} φ$ to indicate that $φ$ is a theorem of $S 5$ .

Modal Duality

The axioms below are interderivable from their modal duals:

$T$	$◻ p \to p$	$p \to ◊ p$	$T_{◊}$
$B$	$p \to ◻ ◊ p$	$◊ ◻ p \to p$	$B_{◊}$
$4$	$◻ p \to ◻ ◻ p$	$◊ ◊ p \to ◊ p$	$4_{◊}$
$5$	$◊ p \to ◻ ◊ p$	$◊ ◻ p \to ◻ p$	$5_{◊}$

Example 10.7 Consider the interderivability of $T_{◊}$ from $T$ :

$K T ⊢ T_{◊}$

$\begin{array}{lllll} 1 & ◻ \neg p \to \neg p & T [\neg p / p] \\ 2 & \neg \neg p \to \neg ◻ \neg p & PL 1 \\ 3 & \neg \neg p \to ◊ p & Def ◊ 2 \\ 4 & p \to ◊ p & PL 3 \end{array}$

$K T_{◊} ⊢ T$

$\begin{array}{lllll} 1 & \neg p \to ◊ \neg p & T_{◊} [\neg p / p] \\ 2 & \neg p \to \neg ◻ \neg \neg p & Def ◊ 1 \\ 3 & \neg \neg ◻ \neg \neg p \to \neg \neg p & PL 2 \\ 4 & ◻ \neg \neg p \to \neg \neg p & PL 3 \\ 5 & p \to \neg \neg p & PL \\ 6 & ◻ p \to ◻ \neg \neg p & RK 5 \\ 7 & ◻ p \to p & PL 4, 6 \end{array}$

The equivalence proof is completely parallel in all other cases.

We are in a position to compare the deductive strength of different normal modal systems. In what follows, we aim to develop an overview of the landscape of normal modal systems for propositional modal logic.

Definition 10.5 (Extension) A modal system $Σ$ extends another modal system $Δ$ , written $Δ ⊑ Σ$ , if, and only if, every theorem of $Δ$ is a theorem of $Σ$ . Or, in other words, for every formula $φ$ of $L^{◻}$ , $If ⊢_{Δ} φ then ⊢_{Σ} φ$ A modal system $Σ$ is a proper extension of $Δ$ , written $Δ ⊏ Σ$ if, and only if, $Δ ⊑ Σ$ but $Σ ⋢ Δ$ .

Here is a graphical representation of some of the relations in which eleven normal modal systems stand to. each other. Each edge connects a modal system with a proper extension located above in the diagram.

Landscape of normal modal systems

There are two main techniques we use in order to justify the diagram. To argue that a modal system $Σ$ extends a system $Δ$ , we argue that every axiom of $Δ$ is a theorem of $Σ$ .

Proposition 10.10 $Δ ⊑ Σ$ if $Σ$ proves every axiom of $Δ$ .

Proof. Since $Δ$ and $Σ$ share the same rules of inference, if every axiom of $Δ$ is a theorem of $Σ$ , then every theorem of $Δ$ is a theorem of $Σ$ .

Example 10.8 $K D ⊑ K T$

This is because $⊢_{K T} ◻ φ \to ◊ φ$ . $\begin{array}{lllll} 1 & ◻ φ \to φ & T [φ / p] \\ 2 & φ \to ◊ φ & T_{◊} [φ / p] \\ 3 & ◻ φ \to ◊ φ & P L 1, 2 \end{array}$

There is a semantic counterpart to this observation. We will eventually observe that each normal modal system characterizes the set of validities in a certain class of frames. In fact, each node in the earlier diagram corresponds to a class of formulas valid in a specific class of frames:

Classes of frames

We will, for example, explain that the normal modal systems $K T$ and $K D$ are sound and complete with respect to the class of reflexive and serial frames, respectively. That means that the theorems of $K T$ are exactly those formulas that are valid in all reflexive frames. And the theorems of $K D$ are the formulas that are valid in all serial frames. Now:

Proposition 10.11 Every reflexive frame is serial.

That means that if a formula is valid in all serial frames, then it will be valid in all reflexive frames. The soundness and completeness theorems for $K D$ and $K T$ will deliver a semantic route to the conclusion that every theorem of $K D$ is a theorem of $K T$ .

On the other hand, the fact that $T$ defines the class of reflexive frames suggests a semantic argument for the conclusion that $K D$ does not extend $K T$ .

Proposition 10.12 If every theorem of $Σ$ is valid in every frame in $C$ , then $Δ ⋢ Σ$ if not every axiom of $Δ$ is valid in every frame in $C$ .

Proof. If an axiom $φ$ of $Δ$ is not valid in every frame in $C$ , then $φ$ is not a theorem of $Σ$ . That means that not every theorem of $Δ$ is a theorem of $Σ$ .

Since the theorems of $K D$ are valid in all serial frames, the observation that $◻ p \to p$ , which is an axiom of $K T$ , is not valid in some serial frames tells us that $K T$ is a proper extension of $K D$ .

Example 10.9 $K T ⋢ K D$

This is because $◻ p \to p$ is not valid in every serial frame. To that purpose, consider the model based on a serial frame depicted below.

(W, R, V), w_{1} ⊮ ◻ p \to p

We may similarly use the fact that axiom 4 is not valid in every reflexive and symmetric frame to establish that some theorems of $K B 5$ are not theorems of $K T B$ .

Example 10.10 $K B 5 ⋢ K T B$

This is because $◊ p \to ◻ ◊ p$ is not valid in every reflexive and symmetric frame. To that purpose, consider the model based on a reflexive and symmetric frame depicted below.

(W, R, V), w_{1} ⊮ ◊ p \to ◻ ◊ p

Where should we locate $K B 5$ in the diagram? We now argue that $K B 4$ and $K B 5$ are mutual extensions of each other, which is the reason we do not have a further node for $K B 5$ in the diagram:

Example 10.11 $K B 4 ⊑ K B 5$

This is because $⊢_{K B 5} ◻ φ \to ◻ ◻ φ$ .

$\begin{array}{lllll} 1 & ◻ φ \to ◻ ◊ ◻ φ & B [◻ φ / p] \\ 2 & ◊ ◻ φ \to ◻ φ & 5_{◊} [φ / p] \\ 3 & ◻ ◊ ◻ φ \to ◻ ◻ φ & R K 2 \\ 4 & ◻ φ \to ◻ ◻ φ & P L 1, 3 \end{array}$

Example 10.12 $K B 5 ⊑ K B 4$

This is because $⊢_{K B 4} ◊ φ \to ◻ ◊ φ$ .

$\begin{array}{lllll} 1 & ◊ φ \to ◻ ◊ ◊ φ & B [⋄ φ / p] \\ 2 & ◊ ◊ φ \to ◊ φ & 4_{◊} [φ / p] \\ 3 & ◻ ◊ ◊ φ \to ◻ ◊ φ & R K 2 \\ 4 & ◊ φ \to ◻ ◊ φ & P L 1, 3 \end{array}$

Example 10.13 $K B 4 = K B 5$

This is an immediate consequence of the last two examples.

The Reduction of Pure Modalities

We conclude the survey of the landscape of normal modal logics with a discussion of two salient normal systems, $K T 4$ ( $S 4$ ), and $K T 5$ ( $S 5$ ), and their ability to collapse certain iterations of modalities.

S4

The normal modal logic $S 4$ results from $K$ when we supplement its axioms with all substitution instances of the axioms: $\begin{matrix} (T) & ◻ p \to p \end{matrix}$ $\begin{matrix} (4) & ◻ p \to ◻ ◻ p \end{matrix}$

Neither KTB nor KB4 extend S4.

Proposition 10.13 $S 4 ⋢ K T B$

Proof. This is because axiom 4, $◻ p \to ◻ ◻ p$ , is not valid in every reflexive and symmetric frame, witness the model we used in example 7.10.

(W, R, V), w_{1} ⊮ ◻ p \to ◻ ◻ p

Proposition 10.14 $S 4 ⋢ K B 4$

Proof. This is because axiom T, $◻ p \to p$ , is not valid in every symmetric and transitive frame. To that purpose, consider the model based on a symmetric and transitive frame depicted below.

(W, R, V), w_{1} ⊮ ◻ p \to p

On the other hand, $S 4$ extends neither $K T B$ nor $K B 4$ .

Proposition 10.15 $K B 4 ⋢ S 4$ and $K T B ⋢ S 4$

Proof. This is because axiom B, $p \to ◻ ◊ p$ . is not valid in every reflexive and transitive frame. To that purpose, consider the model based on a reflexive and transitive frame depicted below.

(W, R, V), w_{1} ⊮ p \to ◻ ◊ p

One reason $S 4$ is of interest is that its axioms have seemed plausible to some on certain interpretations of the modal operators, e.g., in terms of knowledge and metaphysical modality. But another reason to consider $S 4$ is that it allows one to collapse certain iterations of modalities.

Definition 10.6 (Pure Modality) A pure modality is a finite iteration of zero or more occurrences of the modal operators $◻$ and $◊$ .

Definition 10.7 (Entailment) A modality $α$ entails a modality $β$ relative to a modal system $Σ$ if, and only if, $⊢_{Σ} α φ \to β φ .$

Definition 10.8 (Equivalence) A modality $α$ is equivalent to a modality $β$ relative to a modal system $Σ$ if, and only if, $⊢_{Σ} α φ \leftrightarrow β φ .$

One way in which a normal modal system may enable one to reduce a pure modality to another is by means of one of four main reduction laws: $\begin{array}{lll} R 1 & ◊ ◊ φ \leftrightarrow ◊ φ \\ R 2 & ◻ ◻ φ \leftrightarrow ◻ φ \\ R 3 & ◊ ◻ φ \leftrightarrow ◻ φ \\ R 4 & ◻ ◊ φ \leftrightarrow ◊ φ \end{array}$

Example 10.14 If a normal modal system $Σ$ proves all four reduction laws, then $Σ$ allows one to collapse a modal formula such as $\neg ◻ ◻ ◊ \neg ◻ ◊ φ$ into the much simpler $◊ φ$ .

We use the definition of $◊$ in terms of $\neg$ and $◻$ and a rule of replacement for equivalent modal formulas to bring occurrences of negation to the front: $\begin{aligned} \neg ◻ ◻ ◊ \neg ◻ ◊ φ \\ \neg ◻ ◻ \neg ◻ \neg \neg ◻ ◊ φ \\ \neg ◻ ◻ \neg ◻ ◻ ◊ φ \\ \neg ◻ \neg \neg ◻ \neg ◻ ◻ ◊ φ \\ ◊ ◊ ◻ ◻ ◊ φ \end{aligned}$ The four reduction laws now allow us to reduce each pure modality of depth greater than one to one with one fewer pure modality. $\begin{aligned} ◊ ◻ ◻ ◊ φ & R 1 \\ ◻ ◻ ◊ φ & R 3 \\ ◻ ◊ φ & R 2 \\ ◊ φ & R 4 \end{aligned}$ So, the initial modal formula $\neg ◻ ◻ ◊ \neg ◻ ◊ φ$ is in fact equivalent to $◊ φ$ relative to $Σ$ .

For the general study of pure modalities, we distinguish two directions in each of the four reduction laws: $\begin{array}{lll} R 1 a & ◊ φ \to ◊ ◊ φ & R 1 b & ◊ ◊ φ \to ◊ φ \\ R 2 a & ◻ ◻ φ \to ◻ φ & R 2 b & ◻ φ \to ◻ ◻ φ \\ R 3 a & ◻ φ \to ◊ ◻ φ & R 3 b & ◊ ◻ φ \to ◻ φ \\ R 4 a & ◻ ◊ φ \to ◊ φ & R 4 b & ◊ φ \to ◻ ◊ φ \end{array}$

We are now in a position to explain how different normal modal systems enable us to collapse some iterations of pure modalities into simpler ones.

Proposition 10.16 $K T$ delivers $R 1 a$ , $R 2 a$ , $R 3 a$ , and $R 4 a$ .

Proposition 10.17 $S 4$ delivers $R 1$ , $R 2$ , $R 3 a$ , and $R 4 a$ .

There are at most seven inequivalent pure modalities relative to $S 4$ , which are depicted in the diagram below. A modality is understood to entail another modality in the diagram if it is connected to it by an upwards link:

Pure Modalities in

S 4

We now justify the entailments depicted by the diagram. There is, first, entailment 1 in the diagram:

Proposition 10.18 $⊢_{S 4} ◊ ◻ ◊ φ \to ◊ φ$

$\begin{array}{lllll} 1 & ◻ ◊ φ \to ◊ φ & T [◊ φ / p] \\ 2 & ◊ ◻ ◊ φ \to ◊ ◊ φ & RK ◊ 1 \\ 3 & ◊ ◊ φ \to ◊ φ & 4_{◊} [φ / p] \\ 4 & ◊ ◻ ◊ φ \to ◊ φ & PL 2, 3 \end{array}$

On to entailment 2:

Proposition 10.19 $⊢_{S 4} ◊ ◻ φ \to ◊ ◻ ◊ φ$

$\begin{array}{lllll} 1 & φ \to ◊ φ & T [φ / p] \\ 2 & ◻ φ \to ◻ ◊ φ & RK 1 \\ 3 & ◊ ◻ φ \to ◊ ◻ ◊ φ & RK ◊ 2 \end{array}$

Entailments 3 and 4 are instances of $T_{◊}$ and $T$ , respectively, in which occurrences of $p$ are uniformly replaced with occurrences of $◻ ◊ φ$ .

For entailments 5 and 6, we rely on a lemma:

Lemma 10.1 $⊢_{S 4} ◻ ◊ φ \leftrightarrow ◻ ◊ ◻ ◊ φ$

For one direction, we argue: $\begin{array}{lllll} 1 & ◻ ◊ φ \to ◊ ◻ ◊ φ & T_{◊} [◻ ◊ φ / p] \\ 2 & ◻ ◻ ◊ φ \to ◻ ◊ ◻ ◊ φ & RK 1 \\ 3 & ◻ ◊ φ \to ◻ ◻ ◊ φ & 4 [◊ φ / p] \\ 4 & ◻ ◊ φ \to ◻ ◊ ◻ ◊ φ & PL 2, 3 \end{array}$ For the other, we reason:

$\begin{array}{lllll} 1 & ◻ ◊ φ \to ◊ φ & T [◊ φ / p] \\ 2 & ◊ ◻ ◊ φ \to ◊ ◊ φ & RK ◊ 1 \\ 3 & ◊ ◊ φ \to ◊ φ & 4_{◊} [φ / p] \\ 4 & ◊ ◻ ◊ φ \to ◊ φ & PL 2, 3 \\ 5 & ◻ ◊ ◻ ◊ φ \to ◻ ◊ φ & RK 4 \end{array}$

We are now in a position to justify entailments 6 and 7, respectively:

Proposition 10.20 $⊢_{S 4} ◻ ◊ ◻ φ \to ◻ ◊ φ$

$\begin{array}{llll} 1 & φ \to ◊ φ & T_{◊} [φ / p] \\ 2 & ◻ φ \to ◻ ◊ φ & RK 1 \\ 3 & ◊ ◻ φ \to ◊ ◻ ◊ φ & RK ◊ 2 \\ 4 & ◻ ◊ ◻ φ \to ◻ ◊ ◻ ◊ φ & RK 3 \\ 5 & ◻ ◊ ◻ ◊ φ \to ◻ ◊ φ & Lemma 7.1 \\ 6 & ◻ ◊ ◻ φ \to ◻ ◊ φ & PL 4, 5 \end{array}$

Proposition 10.21 $⊢_{S 4} ◻ φ \to ◻ ◊ ◻ φ$

$\begin{array}{lllll} 1 & ◻ φ \to ◊ ◻ φ & T_{◊} [◻ φ / p] \\ 2 & ◻ ◻ φ \to ◻ ◊ ◻ φ & RK 1 \\ 3 & ◻ φ \to ◻ ◻ φ & 4 [φ / p] \\ 4 & ◻ φ \to ◻ ◊ ◻ φ & PL 2, 3 \end{array}$

We conclude that there is an upper bound on the number of inequivalent pure modalities relative to $S 4$ .

Proposition 10.22 There are exactly seven inequivalent pure modalities relative to $S 4$ .

Proof. There are exactly three inequivalent modalities of depth 1.

$◻$
$◊$

There are two new inequivalent modalities of depth 2:

$◻ ◊$
$◊ ◻$

The reason for this is that $◻ ◻$ and $◊ ◊$ collapse into $◻$ and $◊$ , respectively, relative to $S 4$ .

There are two new inequivalent modalities of depth 3:

$◊ ◻ ◊$
$◻ ◊ ◻$

The reason is that $◻ ◻ ◊$ collapses into $◻ ◊$ and $◊ ◊ ◻$ collapses into $◊ ◻$ .

There are no new inequivalent modalities of depth 4.

By lemma 7.1, $◻ ◊ ◻ ◊$ is equivalent to $◻ ◊$ relative to $S 4$ . On the other hand, $◊ ◻ ◊ ◻$ is equivalent to $◊ ◻$ relative to $S 4$ .

We conclude that there are exactly seven inequivalent modalities relative to $S 4$ .

S5

The modal logic $S 5$ is the system which results from the minimal modal logic $K$ when we supplement its axioms with all substitution instances of the axioms: $\begin{matrix} (T) & ◻ p \to p \end{matrix}$ $\begin{matrix} (5) & ◊ p \to ◻ ◊ p \end{matrix}$

Proposition 10.23 $S 4 ⊑ S 5$

All substitution instances of axiom 4 are theorems of $S 5$ : $\begin{array}{lllll} 1 & ◊ ◻ φ \to ◻ ◊ ◻ φ & 5 [◻ φ / p] \\ 2 & ◻ φ \to ◊ ◻ φ & T_{◊} [◻ φ / p] \\ 3 & ◻ φ \to ◻ ◊ ◻ φ & PL 1, 2 \\ 4 & ◊ ◻ φ \to ◻ φ & 5_{◊} [φ / p] \\ 5 & ◻ ◊ ◻ φ \to ◻ ◻ φ & RK 4 \\ 6 & ◻ φ \to ◻ ◻ φ & PL 3, 5 \end{array}$

Proposition 10.24 $K B 5 ⊑ S 5$

All substitution instances of axiom B are theorems of $S 5$

$\begin{array}{lllll} 1 & ◊ φ \to ◻ ◊ φ & 5 [⋄ φ / p] \\ 2 & φ \to ◊ φ & T_{◊} [φ / p] \\ 3 & φ \to ◻ ◊ φ & PL 1, 2 \end{array}$

$S 5$ proves all four reduction laws for pure modalities.

Proposition 10.25 $S 4$ delivers $R 1$ , $R 2$ , $R 3$ , and $R 4$ .

It follows that there are no new pure modalities of depth greater than 1, and that it turns delivers exactly three inequivalent pure modalities relative to $S 5$ .

Proposition 10.26 There are exactly three inequivalent pure modalities relative to $S 5$ .

Proof. There are exactly three inequivalent modalities of depth 1:

$◻$
$◊$

There are no new inequivalent modalities of depth 2.

The reason for this is that $S 5$ proves all four reduction laws, which allows the system to collapse every modality of depth 2 into one of depth 1.

We conclude that there are exactly seven inequivalent modalities relative to $S 4$ .