Appropriate formulation of the necessitation rule from modal logic

Question

The SEP article on modal logic states the necessitation rule for system K (after Saul Kripke):

Necessitation Rule: If A is a theorem of K, then so is □A.

The wikipedia article on modal logic uses a more careful formulation:

Many modal logics, known collectively as normal modal logics, include the following rule and axiom:

• N, Necessitation Rule: If p is a theorem (of any system invoking N), then □p is likewise a theorem.
• K, Distribution Axiom: □(p→q) → (□p→□q).

The weakest normal modal logic, named K in honor of Saul Kripke, is simply the propositional calculus augmented by □, the rule N, and the axiom K.

For the SEP formulation, if we add the axiom □A→A to system K in order to get system M, it seems like □(□A→A) wouldn't be a theorem of system M. The wikipedia formulation on the other hand makes it clear that □(□A→A) is a theorem of system M. But when we are using system K or M and have a premise p, we certainly don't want to conclude □p from the necessitation rule.

But how to make it clear whether the necessitation rule should be applicable to axiom schemes concerning the inner structure of proposition? Consider the axiom scheme for transitivity of equality (p=q)∧(q=r)⇒(p=r) in a formal system operating on equations between terms (p=q for terms p and q) as basic propositions. Can we deduce □((p=q)∧(q=r)⇒(p=r)) from the necessitation rule, or do we have to add it explicitly as an additional axiom scheme? In case we can deduce it, what is the difference in terms of semantics between a theorem from an axiom scheme (for which the necessitation rule applies) and a deduction from a premise (for which the necessitation rule doesn't apply)?

Answer 1

To maybe put the interrelation between these three rules into perspective, it might be worthwhile to notice that from the point of view of categorical logic, the categorical semantics of a modality (with all three rules N, K and M) is a closure operator, hence a (co-)monad on the system of propositions/of types. Rule M then interprets as the (co-)unit of the (co-)monad. This gives a usefully "global" picture of what the interrelation between these three rules is, or maybe what it should most naturally be taken to be. In particular it means that □(□A→A).

This monadic perspective on modal logic has proven quite fruitful as of late. Generalized from propositions to type theory it leads to modal type theory which is sometimes called computational type theory due to the intimate and practically relevant application of modalities in type theories to encode computational effects in functional programming. One might view the wealth of these applications as evidence that regarding the rules N, K and M in their correct interaction as the encoding of a monad is their natural raison d'être.

Lawvere had pointed out that considering modalities in this sense related to each other such as to make for systems of "adjoint modalities" has profound implications on the re-reading of parts of philosophy to which application of modal logic had never been dreamed of, namely Lawvere points out that adding axioms for systems of adjoint modalities to the intuitionistic type system serves to usefully(!) formalize the "unities of opposites" that infamously govern Hegelian metaphysics.

Recently with the advent of homotopy type theory this monadic perspective on modalities has brought about some developments that seem fairly dramatic compared to the developments in modal logic (to which this still reduces on (-1)-truncated types). In cohesive homotopy type theory we add a triple of adjoint modalities to the logic/the type system and find that this provides a formal context in which a maybe surprisingly large bit of modern higher geometry may be usefully axiomatized.

All this is only possible with reading the rules for N,M,K in the "natural way" (which hopefully is the way that the Wikipedia article describes).

Answer 2

The necessitation rule is not an axiom, but instead a deduction rule. For p to be a theorem it means that it has no hypotheses. Thus, necessitation can be formulated as an rule on sequents:

    |- p
 N --------
    |- □p

Thus, N only applies when p does not contain hypotheses (unbound variables). Therefore, □(□A→A) is a theorem in M (its not clear from your question why you think it wouldn't be). Does that make things more clear?