Is the necessitation inference rule necessary?

Question

In The Handbook of Epistemic Logic, they define a basic system K to be an extention of propositional logic, as

• All propositional tautologies
• $\square(p \to q) \to \square p \to \square q$
• $p \to q, p\vdash q$ (MP)
• $p\vdash \square p$ (NEC)

where $p,q$ range over propositions. I do not understand the NEC rule in the sense that it's presented as a rule and not as an axiom. Wouldn't it be equivalent to having the axiom $p\to \square p$ for the same reason $\square(p \to q) \to \square p \to \square q$ is an axiom? You could only ever apply $p \to \square p$ if $p$ was derivable from the axioms, so how would this differ from having this as an inference rule? The only reasoning that I could come up with was because when it is in the form of an axiom $p \to \square p$, it would have equivalent forms $\neg p \vee \square p$, $\neg \square p \to \neg p$, and others that would loose the sense of what the rule means.

I guess this leads to the more general question about why you would opt to define a rule $$ \frac{p_1 \quad \ldots \quad p_n}{q} $$ in addition to modes ponens, rather than just adding $$ (p_1\wedge\ldots\wedge p_n) \to q $$ as an axiom?

Answer 1

We can see the difference without invoking formal semantics.

$p\rightarrow\square p$ tells us that if (or, whenever) $p$ holds, it holds necessarily. An utterly deterministic Weltanschauung; a very difficult position to defend.

$p\vdash\square p$ tells us that if $p$ is assumed (or, shown) to be a valid formula (i.e., true whatever the case is), then it is accepted to hold necessarily. Not uncontroversial, but validity preservation is quite a defensible position.

Answer 2

The equivalence between the provability of $p \vdash q$ and $\vdash p \to q$ is the deduction theorem. It is a property of a logic that needs to be proved. I don't think it is intended that the deduction theorem holds in system $K$.

Answer 3

The problem with taking $p \rightarrow \Box p$ as an axiom is that this formula defines the class of frames $(W, R)$ with $R(w) \in \{ \varnothing, \{w\}\}$, for every $w \in W$ ($R(w)$ being the set of $R$-successors of $w$). Since there are frames that invalidate the formula, adding the formula to $K$ yields a system that is not sound with respect to the class of all frames. Since $K$ is sound with respect to that class, the expanded system is distinct from $K$. On the other hand, the necessitation rule preserves validity on the class of all frames.

As an aside, this shows that the deduction theorem does not hold for basic modal logic under a global notion of logical consequence, that is, consequence conceived of as preservation of validity on frames.