Distribution axiom (K)

Question

What is the reason for taking the following as the axiom in normal modal logics: □(p → q) → (□p → □q)? What is special about this formula that makes it an axiom? Does it express some kind of tautology? For example, the following is an axiom of propositional logic and is clearly a tautology: (p → (q → s)) → ((p → q) → (p → s)). I wonder if there are similar justifications for the distribution axiom as well.

Answer 1

Yes, it is valid in every Kripke model. So, if we want our deduction system to be complete with respect to Kripke semantics, it needs to be derivable, and for that we can simply put it as an axiom.

To prove it holds in an arbitrary Kripke model $(W, R, \Vdash)$, we use that $w\Vdash (a\to b)$ for a world $w\in W$ iff whenever $w\Vdash a$, we also have $w\Vdash b$. (In other words, $w\not\Vdash (a\to b)\ $ iff $\ w\Vdash a$ and $w\not\Vdash b$.)
Now assume $\def\box{\Box} w\Vdash \box(p\to q)$, then we want $w\Vdash \box p\to\box q$, so assume also $w\Vdash \box p$.

Using Kripke semantics for $\box$, these mean that for all worlds $w'\in W$ that is seen from $w$ (i.e. $w\, R\, w'$) we have both $w'\Vdash p\to q$ and $w'\Vdash p$.
But then it follows that $w'\Vdash q$, and as this holds for all $w'$ which satisfy $w\, R\, w'$, we get $w\Vdash \box q$.