Axiomatic Derivations

Definition of modus ponens

The rule of modus ponens is the inference schema

We say a formula $!B$source follows from formulas $!A$source, $!C$source by modus ponens iff $!C \ident !A \lif !B$source.

Definition of necessitation

The rule of necessitation is the inference schema

We say the formula $!B$source follows from the formulas $!A$source by necessitation iff $!B \ident \Box !A$source.

Definition of an axiomatic derivation

A derivation from a set of axioms $\Sigma$source is a sequence of formulas $!B_1$source, $!B_2$source, dots, $!B_n$source, where each $!B_i$source is either

1. a substitution instance of a tautology, or

2. a substitution instance of a formula in $\Sigma$source, or

3. follows from two formulas $!B_j$source, $!B_k$source with $j$source, $k < i$source by modus ponens, or

4. follows from a formula $!B_j$source with $j < i$source by necessitation.

If there is such a derivation with $!B_n \ident !A$source, we say that $!A$source is derivable from $\Sigma$source, in symbols $\Sigma \Proves !A$source.

Definition of a modal logic

A modal logic is a set $\Sigma$source of modal formulas which

1. contains all tautologies, and

2. is closed under substitution, i.e., if $!A \in \Sigma$source, and $!D_1$source, dots, $!D_n$source are formulas, then

   $$\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \in \Sigma,$$source

3. is closed under modus ponens, i.e., if $!A$source and $!A \lif !B \in \Sigma$source, then $!B \in \Sigma$source.

Definition of a normal modal logic

A modal logic $\Sigma$source is normal if it contains

and is closed under necessitation, i.e., if $!A \in \Sigma$source, then $\Box !A \in \Sigma$source.

Normal modal logics are closed under rule R K

Every normal modal logic is closed under rule RK,

Proof

By induction on $n$source: If $n = 1$source, then the rule is just Nec, and every normal modal logic is closed under Nec.

Now suppose the result holds for $n-1$source; we show it holds for $n$source.

Assume

Normal modal logics exclude possible falsity

Every normal modal logic $\Sigma$source contains $\lnot\Diamond\lfalse$source.

Exercise on possible falsity

Prove the proposition that no normal modal logic permits possibly falsity.

Existence of the smallest generated modal logic

Let $!A_1$source, dots, $!A_n$source be formulas. Then there is a smallest modal logic $\Sigma$source containing all instances of $!A_1$source, dots, $!A_n$source.

Proof

Given $!A_1$source, dots, $!A_n$source, define $\Sigma$source as the intersection of all normal modal logics containing all instances of $!A_1$source, dots, $!A_n$source. The intersection is non-empty as $\Frm[L]$source, the set of all formulas, is such a modal logic.

Definition of a modal system

The smallest normal modal logic containing $!A_1$source, dots, $!A_n$source is called a modal system and denoted by $\Log{K} !A_1 \dots !A_n$source. The smallest normal modal logic is denoted by LogK.

Definition of derivability in a modal system

Given a modal system $\Log{K} !A_1 \dots !A_n$source and a formula $!B$source we say that $!B$source is derivable in $\Log{K} !A_1 \dots !A_n$source, written $\Log{K} !A_1 \dots !A_n \Proves !B$source, if and only if there are formulas $!C_1$source, dots, $!C_k$source such that $!C_k = !B$source and each $!C_i$source is either a tautological instance, or an instance of one of $\Ax{K}$source, $\Dual$source, $!A_1$source, dots, $!A_n$source, or it follows from previous formulas by means of the rules MP or Nec.

Modal-system membership equals derivability

$\Log{K} !A_1 \dots !A_n = \Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B}$source.

Proof

We use induction on the length of derivations to show that $\Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B} \subseteq \Log{K} !A_1 \dots !A_n$source.

If the derivation of $!B$source has length $1$source, it contains a single formula. That formula cannot follow from previous formulas by MP or Nec, so must be a tautological instance, an instance of AxK, $\Dual$source, or an instance of one of $!A_1$source, dots, $!A_n$source. But $\Log{K}!A_1\dots!A_n$source contains these as well, so $!B \in \Log{K}!A_1 \dots !A_n$source.

If the derivation of $!B$source has length $> 1$source, then $!B$source may in addition be obtained by MP or Nec from formulas not occurring as the last line in the derivation. If $!B$source follows from $!C$source and $!C \lif !B$source (by MP), then $!C$source and $!C \lif !B \in \Log{K}!A_1 \dots !A_n$source by induction hypothesis. But every modal logic is closed under modus ponens, so $!B \in \Log{K}!A_1 \dots !A_n$source. If $!B \equiv \Box !C$source follows from $!C$source by Nec, then $!C \in \Log{K}!A_1 \dots !A_n$source by induction hypothesis. But every normal modal logic is closed under $\Nec$source, so $!B \in \Log{K}!A_1\dots!A_n$source.

The converse inclusion follows by showing that $\Sigma = \Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B }$source is a normal modal logic containing all the instances of $!A_1$source, dots, $!A_n$source, and the observation that $\Log{K} !A_1 \dots !A_n$source is, by definition, the smallest such logic.

1. Every tautology $!B$source is a tautological instance, so $\Log{K}!A_1\dots!A_n \Proves !B$source, so $\Sigma$source contains all tautologies.

2. If $\Log{K}!A_1\dots!A_n \Proves !C$source and $\Log{K}!A_1\dots!A_n \Proves !C \lif !B$source, then $\Log{K}!A_1\dots!A_n \Proves !B$source: Combine the derivation of $!C$source with that of $!C \lif !B$source, and add the line $!B$source. The last line is justified by MP. So $\Sigma$source is closed under modus ponens.

3. If $!B$source has a derivation, then every substitution instance of $!B$source also has a derivation: apply the substitution to every formula in the derivation. (Exercise: prove by induction on the length of derivations that the result is also a correct derivation). So $\Sigma$source is closed under uniform substitution. (We have now established that $\Sigma$source satisfies all conditions of a modal logic.)

4. We have $\Log{K}!A_1\dots!A_n \Proves \Ax{K}$source, so $K \in \Sigma$source.

5. We have $\Log{K}!A_1\dots!A_n \Proves \Dual$source, so $\Dual \in \Sigma$source.

6. If $\Log{K}!A_1\dots!A_n \Proves !C$source, the additional line $\Box !C$source is justified by Nec. Consequently, $\Sigma$source is closed under Nec. Thus, $\Sigma$source is normal.

Boxed weakening theorem

$\Log{K} \Proves \Box!A \lif \Box (!B\lif !A)$source

Proof

Box distributes to both conjuncts

$\Log{K} \Proves \Box(!A \land !B) \lif (\Box !A \land \Box!B)$source

Proof

Note that the formula on line $9$source is an instance of the tautology

Two necessary conjuncts imply their necessary conjunction

$\Log{K}\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$source

Proof

The formulas on lines $6$source and $9$source are instances of the tautologies

Box and diamond under negation

$\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$source

Proof

The formulas on lines $8$source and $10$source are instances of the tautologies

Exercises in K

Find derivations in $\Log{K}$source for the following formulas:

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

2. $(\Box p \lor \Box q) \lif \Box(p \lor q)$source

3. $\Diamond p \lif \Diamond(p \lor q)$source

Propositional consequence may be used inside K

If $\Log{K} \Proves !A_1$source, dots, $\Log{K} \Proves !A_n$source, and $!B$source follows from $!A_1$source, dots, $!A_n$source by propositional logic, then $\Log{K} \Proves !B$source.

Proof

If $!B$source follows from $!A_1$source, dots, $!A_n$source by propositional logic, then

is a tautological instance. Applying MP $n$source times gives a derivation of $!B$source.

Derived n-ary rule R K

If $\Log{K} \Proves !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\dots)$source then $\Log{K} \Proves \Box !A_1 \lif (\Box !A_2 \lif \cdots (\Box !A_{n-1} \lif \Box !A_n)\dots)$source.

Proof

By induction on $n$source, just as in the proof of the proposition that every normal modal logic is closed under rule R K.

Short proof of boxed conjunction

$\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$source

Proof

Rewriting proposition

If $\Log{K} \Proves !A \liff !B$source and $\Log{K} \Proves \Subst{!C}{!A}{q}$source then $\Log{K} \Proves \Subst{!C}{B}{q}$source

Proof

Exercise.

Exercise proving the rewriting proposition

Prove the rewriting proposition by proving, by induction on the complexity of $!C$source, that if $\Log{K} \Proves !A \liff !B$source then $\Log{K} \Proves \Subst{!C}{!A}{q} \liff \Subst{!C}{!B}{q}$source.

Not-box implies possible negation

$\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$source

Proof

Uniform substitution preserves derivability

If $!A$source is a substitution instance of $!B$source and $\Log{K} \Proves !B$source, then $\Log{K} \Proves !A$source.

Proof

It is tedious but routine to verify (by induction on the length of the derivation of $!B$source) that applying a substitution to an entire derivation also results in a correct derivation. Specifically, substitution instances of tautological instances are themselves tautological instances, substitution instances of instances of Dual and AxK are themselves instances of Dual and AxK, and applications of MP and Nec remain correct when substituting formulas for propositional variables in both premise(s) and conclusion.

Boxed implication preserves possibility

$\Log{K} \Proves \Box (!A \lif !B) \lif (\Diamond !A \lif \Diamond !B)$source

Proof

A boxed antecedent and possible conditional yield a possible consequent

$\Log{K}\Proves \Box!A \lif (\Diamond(!A \lif !B) \lif \Diamond !B)$source

Proof

Either possible disjunct makes the disjunction possible

$\Log{K} \Proves (\Diamond!A \lor \Diamond!B) \lif \Diamond(!A \lor !B)$source

Proof

Possibility distributes over disjunction

$\Log{K} \Proves \Diamond(!A \lor!B) \lif (\Diamond!A \lor \Diamond!B)$source

Proof

Exercises on derived K proofs

Show that the following derivability claims hold:

1. $\Log{K} \Proves \Diamond \lnot \lfalse \lif (\Box !A \lif \Diamond !A)$source;

2. $\Log{K} \Proves \Box(!A \lor !B) \lif (\Diamond !A \lor \Box !B)$source;

3. $\Log{K} \Proves (\Diamond !A \lif \Box !B) \lif \Box(!A \lif !B)$source.

Definition of the dual modal schemata

Each of the formulas AxT, AxB, Ax4, and Ax5 has a dual, denoted by a subscripted diamond, as follows:

A modal schema and its dual generate the same system

For each formula $!A$source in the definition of the dual modal schemata: $\Log{K}!A = \Log{K}!A_{\Diamond}$source.

Proof

Exercise.

Exercise on dual modal systems

Prove the proposition that adjoining a schema or its dual gives the same modal system.

Six derivability facts among modal systems

The following provability results obtain:

1. $\Log{KT5} \Proves \Ax{B}$source;

2. $\Log{KT5} \Proves \Ax{4}$source;

3. $\Log{KDB4} \Proves \Ax{T}$source;

4. $\Log{KB4} \Proves \Ax{5}$source;

5. $\Log{KB5} \Proves \Ax{4}$source;

6. $\Log{KT} \Proves \Ax{D}$source.

Proof

We exhibit proofs for each.

1. $\Log{KT5} \Proves \Ax{B}$source:

   Three-line K T five proof of axiom B

   Derivation. Line one: modal system K T five derives diamond formula A implies box diamond formula A. Justification: axiom five. Line two: modal system K T five derives formula A implies diamond formula A. Justification: axiom T subscript diamond. Source justification formula, in order: axiom T subscript diamond. Line three: modal system K T five derives formula A implies box diamond formula A. Justification: propositional logic. End derivation.

   1. Line 1. $\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$source Justification: axiom five. Depends on: none. Discharges: none.

   2. Line 2. $\Log{KT5} \Proves !A \lif \Diamond!A$source$\Ax{T_\Diamond}$source Justification: axiom T subscript diamond. Depends on: none. Discharges: none.

   3. Line 3. $\Log{KT5} \Proves !A \lif \Box\Diamond!A$source Justification: propositional logic. Depends on: line-2, line-1. Discharges: none.

   source 31

2. $\Log{KT5} \Proves \Ax{4}$source:

   Six-line K T five proof of axiom four

   Derivation. Line one: modal system K T five derives diamond box formula A implies box diamond box formula A. Justification: axiom five; the source-listed replacement. Source justification formulas, in order: box formula A; then propositional variable p. Line two: modal system K T five derives box formula A implies diamond box formula A. Justification: axiom T subscript diamond; the source-listed replacement. Source justification formulas, in order: axiom T subscript diamond; then box formula A; then propositional variable p. Line three: modal system K T five derives box formula A implies box diamond box formula A. Justification: propositional logic. Line four: modal system K T five derives diamond box formula A implies box formula A. Justification: axiom five subscript diamond. Source justification formula, in order: axiom five subscript diamond. Line five: modal system K T five derives box diamond box formula A implies box box formula A. Justification: rule R K. Line six: modal system K T five derives box formula A implies box box formula A. Justification: propositional logic. End derivation.

   1. Line 1. $\Log{KT5} \Proves \Diamond\Box!A \lif \Box\Diamond\Box!A$source$\Box!A$source$p$source Justification: axiom five; the source-listed replacement. Depends on: none. Discharges: none.

   2. Line 2. $\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$source$\Ax{T_\Diamond}$source$\Box!A$source$p$source Justification: axiom T subscript diamond; the source-listed replacement. Depends on: none. Discharges: none.

   3. Line 3. $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$source Justification: propositional logic. Depends on: line-2, line-1. Discharges: none.

   4. Line 4. $\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$source$\Ax{5_\Diamond}$source Justification: axiom five subscript diamond. Depends on: none. Discharges: none.

   5. Line 5. $\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$source Justification: rule R K. Depends on: line-4. Discharges: none.

   6. Line 6. $\Log{KT5} \Proves \Box!A \lif \Box\Box!A$source Justification: propositional logic. Depends on: line-3, line-5. Discharges: none.

   source 37

3. $\Log{KDB4} \Proves \Ax{T}$source:

   Five-line K D B four proof of axiom T

   Derivation. Line one: modal system K D B four derives diamond box formula A implies formula A. Justification: axiom B subscript diamond. Source justification formula, in order: axiom B subscript diamond. Line two: modal system K D B four derives box box formula A implies diamond box formula A. Justification: axiom D; the source-listed replacement. Source justification formulas, in order: axiom D; then box formula A; then propositional variable p. Line three: modal system K D B four derives box box formula A implies formula A. Justification: propositional logic. Line four: modal system K D B four derives box formula A implies box box formula A. Justification: axiom four. Line five: modal system K D B four derives box formula A implies formula A. Justification: propositional logic. End derivation.

   1. Line 1. $\Log{KDB4} \Proves \Diamond\Box!A \lif !A$source$\Ax{B_\Diamond}$source Justification: axiom B subscript diamond. Depends on: none. Discharges: none.

   2. Line 2. $\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$source$\Ax{D}$source$\Box!A$source$p$source Justification: axiom D; the source-listed replacement. Depends on: none. Discharges: none.

   3. Line 3. $\Log{KDB4} \Proves \Box\Box!A \lif !A$source Justification: propositional logic. Depends on: line-1, line-2. Discharges: none.

   4. Line 4. $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$source Justification: axiom four. Depends on: none. Discharges: none.

   5. Line 5. $\Log{KDB4} \Proves \Box!A \lif !A$source Justification: propositional logic. Depends on: line-4, line-3. Discharges: none.

   source 48

4. $\Log{KB4} \Proves \Ax{5}$source:

   Four-line K B four proof of axiom five

   Derivation. Line one: modal system K B four derives diamond formula A implies box diamond diamond formula A. Justification: axiom B; the source-listed replacement. Source justification formulas, in order: diamond formula A; then propositional variable p. Line two: modal system K B four derives diamond diamond formula A implies diamond formula A. Justification: axiom four subscript diamond. Source justification formula, in order: axiom four subscript diamond. Line three: modal system K B four derives box diamond diamond formula A implies box diamond formula A. Justification: rule R K. Line four: modal system K B four derives diamond formula A implies box diamond formula A. Justification: propositional logic. End derivation.

   1. Line 1. $\Log{KB4} \Proves \Diamond!A \lif \Box \Diamond\Diamond!A$source$\Diamond!A$source$p$source Justification: axiom B; the source-listed replacement. Depends on: none. Discharges: none.

   2. Line 2. $\Log{KB4} \Proves \Diamond\Diamond !A \lif \Diamond !A$source$\Ax{4_\Diamond}$source Justification: axiom four subscript diamond. Depends on: none. Discharges: none.

   3. Line 3. $\Log{KB4} \Proves \Box\Diamond\Diamond !A \lif \Box \Diamond!A$source Justification: rule R K. Depends on: line-2. Discharges: none.

   4. Line 4. $\Log{KB4} \Proves \Diamond!A \lif \Box\Diamond!A$source Justification: propositional logic. Depends on: line-1, line-3. Discharges: none.

   source 57

5. $\Log{KB5} \Proves \Ax{4}$source:

   Four-line K B five proof of axiom four

   Derivation. Line one: modal system K B five derives box formula A implies box diamond box formula A. Justification: axiom B; the source-listed replacement. Source justification formulas, in order: box formula A; then propositional variable p. Line two: modal system K B five derives diamond box formula A implies box formula A. Justification: axiom five subscript diamond. Source justification formula, in order: axiom five subscript diamond. Line three: modal system K B five derives box diamond box formula A implies box box formula A. Justification: rule R K. Line four: modal system K B five derives box formula A implies box box formula A. Justification: propositional logic. End derivation.

   1. Line 1. $\Log{KB5} \Proves \Box!A \lif \Box\Diamond\Box !A$source$\Box!A$source$p$source Justification: axiom B; the source-listed replacement. Depends on: none. Discharges: none.

   2. Line 2. $\Log{KB5} \Proves \Diamond\Box!A \lif \Box !A$source$\Ax{5_\Diamond}$source Justification: axiom five subscript diamond. Depends on: none. Discharges: none.

   3. Line 3. $\Log{KB5} \Proves \Box\Diamond\Box!A \lif \Box\Box !A$source Justification: rule R K. Depends on: line-2. Discharges: none.

   4. Line 4. $\Log{KB5} \Proves \Box!A \lif \Box\Box!A$source Justification: propositional logic. Depends on: line-1, line-3. Discharges: none.

   source 67

6. $\Log{KT} \Proves \Ax{D}$source:

   Three-line K T proof of axiom D

   Derivation. Line one: modal system K T derives box formula A implies formula A. Justification: axiom T. Line two: modal system K T derives formula A implies diamond formula A. Justification: axiom T subscript diamond. Source justification formula, in order: axiom T subscript diamond. Line three: modal system K T derives box formula A implies diamond formula A. Justification: propositional logic. End derivation.

   1. Line 1. $\Log{KT} \Proves \Box !A \lif !A$source Justification: axiom T. Depends on: none. Discharges: none.

   2. Line 2. $\Log{KT} \Proves !A \lif \Diamond!A$source$\Ax{T_\Diamond}$source Justification: axiom T subscript diamond. Depends on: none. Discharges: none.

   3. Line 3. $\Log{KT} \Proves \Box !A \lif \Diamond !A$source Justification: propositional logic. Depends on: line-1, line-2. Discharges: none.

   source 76

Definitions of S four and S five

Following tradition, we define LogS4 to be the system LogKT4, and LogS5 the system LogKTB4.

Equivalent axiomatizations of S five

$\Log{KTB4} = \Log{KT5} = \Log{KDB4} = \Log{KDB5}$source.

Proof

Exercise.

Exercise proving the S-five equivalences

Prove the proposition giving equivalent axiomatizations of S five.

Soundness theorem for modal systems

[Soundness Theorem] If every instance of $!A_1$source, dots, $!A_n$source is valid in the classes of models $\mClass{C}_1$source, dots, $\mClass{C}_n$source, respectively, then $\Log{K}!A_1\dots !A_n \Proves !B$source implies that $!B$source is valid in the class of models $\mClass{C}_1 \cap \dots \cap \mClass{C}_n$source.

Proof

By induction on length of proofs. For brevity, put $\mClass{C} = \mClass{C}_1 \cap \dots \cap \mClass{C}_n$source.

1. Induction Basis: If $!B$source has a proof of length $1$source, then it is either a tautological instance, an instance of AxK, or of Dual, or an instance of one of $!A_1$source, dots, $!A_n$source. In the first case, $!B$source is valid in $\mClass{C}$source, since tautological instance are valid in any class of models, by the proposition that tautological instances are valid. Similarly in the second case, by the proposition that axiom K is valid and the proposition that the duality schema is valid . Finally in the third case, since $!B$source is valid in $\mClass{C}_i$source and $\mClass{C} \subseteq \mClass{C}_i$source, we have that $!B$source is valid in $\mClass{C}$source as well by the proposition preserving validity under subclasses of models.

2. Inductive step: Suppose $!B$source has a proof of length $k>1$source. If $!B$source is a tautological instance or an instance of one of $!A_1$source, dots, $!A_n$source, we proceed as in the previous step. So suppose $!B$source is obtained by MP from previous formulas $!C \lif !B$source and $!C$source. Then $!C \lif !B$source and $!C$source have proofs of length $<k$source, and by inductive hypothesis they are valid in $\mClass{C}$source. By the soundness of modus ponens, $!B$source is valid in $\mClass{C}$source as well. Finally suppose $!B$source is obtained by Nec from $!C$source (so that $!B = \Box!C$source). By inductive hypothesis, $!C$source is valid in $\mClass{C}$source, and by the validity-preservation rule for necessitation so is $!B$source.

K D is a proper subsystem of K T

$\Log{KD} \subsetneq \Log{KT}$source

Proof

This is the syntactic counterpart to the semantic fact that all reflexive relations are serial. To show $\Log{KD} \subseteq \Log{KT}$source we need to see that $\Log{KD} \Proves !B$source implies $\Log{KT} \Proves !B$source, which follows from $\Log{KT} \Proves \Log{D}$source, as shown in the proposition listing modal-system derivability factsthe item stating that K T derives axiom D. To show that the inclusion is proper, by Soundness (the soundness theorem for modal systems), it suffices to exhibit a model of LogKD where AxT, i.e., $\Box p \lif p$source, fails (an easy task left as an exercise), for then by Soundness $\Log{KD} \Proves/ \Box p \lif p$source.

K B differs from K four

$\Log{KB} \neq \Log{K4}$source.

Proof

We construct a symmetric model where some instance of Ax4 fails; since obviously the instance is derivable for LogK4 but not in LogKB, it will follow $\Log{K4} \nsubseteq \Log{KB}$source. Consider the symmetric model $\mModel{M}$source of the symmetric countermodel to axiom four. Since the model is symmetric, AxK and AxB are true in $\mModel{M}$source (by the proposition that axiom K is valid and the theorem connecting modal schemata with accessibility conditions, respectively). However, $\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$source.

K T B derives neither four nor five

$\Log{KTB} \Proves/ \Log{4}$source and $\Log{KTB} \Proves/ \Log{5}$source.

Proof

By the theorem connecting modal schemata with accessibility conditions we know that all instances of AxT and AxB are true in every reflexive symmetric model (respectively). So by soundness, it suffices to find a reflexive symmetric model containing a world at which some instance of Ax4 fails, and similarly for Ax5. We use the same model for both claims. Consider the symmetric, reflexive model in the reflexive symmetric countermodel to axioms four and five. Then $\mSat/{M}{\Box p \to \Box \Box p}[w_1]$source, so Ax4 fails at $w_1$source. Similarly, $\mSat/{M}{\Diamond \lnot p \lif \Box \Diamond \lnot p}[w_2]$source, so the instance of Ax5 with $!A = \lnot p$source fails at $w_2$source.

K D five differs from S four

$\Log{KD5} \neq \Log{KT4} = \Log{S4}$source.

Proof

By the theorem connecting modal schemata with accessibility conditions we know that all instances of AxD and Ax5 are true in all serial euclidean models. So it suffices to find a serial euclidean model containing a world at which some instance of Ax4 fails. Consider the model of the serial Euclidean countermodel to axiom four, and notice that $\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$source.