# Appropriate formulation of the necessitation rule from modal logic

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)?

• You correctly quoted the 'necessitation rule for system K' as formulated at the SEP entry (which is indeed not careful enough). In other systems such as M, B, T, S4 and S5, also mentioned in the same section of that entry, you indeed need to rephrase the rule of necessitation accordingly: for each modal system L, the rule should say that 'if A is a theorem of L, then so is □A' (so, in particular, the necessitation rule applies to the axioms of L). Thus, in answer to your question: The Wikipedia formulation is the appropriate one. – J Marcos Nov 12 '13 at 15:11
• On what concerns the difference in semantics between rules that apply to 'theorems' (which have 'axioms' as particular cases) and 'deductions from a premise', you might want to distinguish between the truth-preserving class of inference rules and the validity-preserving class of deduction rules. Why is this distinction sometimes overlooked in the modal literature? I ventured a few explanatory hypotheses about that here, long ago. – J Marcos Nov 12 '13 at 15:31
• @JMarcos I finally read and understood your link. So the 'deductions from a premise' should definitively use truth-preserving inference rules, unless limitations of the available language force us to use validity-preserving deduction rules. The necessitation rule indeed seems to somehow rely on validity, but I still don't see clearly whether the necessitation rule should be applicable to axiom schemes concerning the inner structure of proposition. – Thomas Klimpel Nov 13 '13 at 0:18
• I think now that as long as the inner structure of propositions is not part of the modal logic system itself, it's better to assume that the necessitation rule doesn't apply directly. For quantified modal logic on the other hand, the inner structure of propositions would be part of the modal logic system, and hence the necessitation rule should apply directly in that case. The minor inconvenience of having to add the corresponding axioms explicitly as additional axiom schemes seems to be offset by the greater conceptual clarity. – Thomas Klimpel Nov 13 '13 at 0:24
• Still concerning the semantics of inference rules and deduction rules, one interesting thing I did not commented upon in the previously mentioned link concerns the connection between the truth-preserving class of derivable rules and the validity-preserving class of admissible rules of a given logical system. This has been much studied in particular in the context of intermediate logics (with Kripke semantics). – J Marcos Nov 13 '13 at 15:25

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).

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?

• The question asks for the "appropriate formulation" of the necessitation rule, and the SEP article doesn't even try to use an appropriate formulation. Hence □(□A→A) is not a theorem of M according to the formulation of the SEP article, because □A→A is not a theorem of K. This purpose of this example is to explain that coming up with an appropriate formulation of the necessitation rule is challenging. Appendix: Your suggestion to replace "premise" by "hypothesis" in the question is probably a good idea. – Thomas Klimpel Nov 12 '13 at 8:57