Understanding the modal necessitation rule

I understand that the modal necessitation rule is:

$\vdash p \Rightarrow \vdash \Box p$

That is, if p is a theorem then necessarily p is a theorem.

But I don't quite understand what this means, or how I could use it in a modal proof. Obviously if I derive $x$ on a line I cannot then move to necessarily $x$. (Just because it's actually raining does not imply that it's raining in all possible worlds.)

Does the rule mean that only if $p$ is a tautology then I can move to necessarily $p$? Just trying to figure out exactly what is meant by "theorem" and how i can use the necessitation rule in a proof. Thanks.

• Your puzzlement about "what this means" may be a philosophical question rather than a mathematical one. If so, you might want to have a look at, say, W.V.Quine's "The Ways of Paradox" which contains papers like "Three Grades of Modal Involvement." But don't expect any clear and definite answers -- it's not math! Commented May 22, 2013 at 14:10
• Let me add a question for clarification: how is it different and if so why preferable to just having p⇒□p as an axiom? Commented Feb 7, 2021 at 5:38

The rule is that if $$\varphi$$ is provable from no assumptions [other than logical axioms], i.e. if $$\varphi$$ is a theorem, then $$\Box\varphi$$ is also a theorem. That's a plausible rule to have in the modal logic of necessity: it formally echoes the idea that if something is demonstrable by logical reflection alone it is necessarily true.

Thus, the following is a proof in standard modal systems:

1. $$(p \lor \neg p)$$

2. $$\Box(p \lor \neg p)$$

3. $$\Box\Box(p \lor \neg p)$$

where the first line is a tautology derivable from no assumptions [other than axioms], so using necessitation we can infer (2). But note that (2) is still derived from no assumptions (logical reflection alone is required to see it is true) so we can use necessitation again to infer (3) in turn.

The input to an application of the necessitation rule has to be a theorem but needn't be a truth-functional tautology.

[There are some wonderful books on elementary modal logic which will explain this very clearly -- there are some suggestions in §2.2 of the Teach Yourself Logic Guide you can download here.]

• To add just a little bit to that, since the OP mentioned possible worlds: since (in typical interpretations, including Kripke semantics) every possible world is logically consistent (i.e., even though the truth of contingent sentences, e.g., $A \lor B$, might not be the same), any theorem $\phi$ (i.e., $\vdash \phi$) is derivable in any of the possible worlds, which is exactly what $\Box\phi$ means. Commented May 22, 2013 at 16:15
• This is great, thanks very much! One point of clarification: What if we have a premise in a proof; say, a --> b. I presume then then we cannot derive $\Box$ (a --> b )?
– MDog
Commented May 22, 2013 at 17:38
• You presume correctly. Commented May 22, 2013 at 21:31

Actually, $p$ has to be a tautology.

For the sake of completeness, let's consider an example about how it can be used in a proof.

Assume the following axioms and inference rules:
A1. All tautologies of propositional calculus
A2. $(\square_i \phi \land \square_i (\phi \Rightarrow \psi) \Rightarrow \square_i \psi \hspace{1cm}i=1,\cdots, n$ $\hspace{1cm}$ [Distribution Axiom]
R1. From $\phi$ and $\phi \Rightarrow \psi$ infer $\psi$ $\hspace{4.5cm}$ [MP]
R2. From $\phi$ infer $\square_i \phi$

Theorem:
$\square (p \land q) \Rightarrow \square p$

Proof:
1. $(p \land q) \Rightarrow p$ $\hspace{13.3cm}$ (A1)
2. $\square ((p \land q) \Rightarrow p)$ $\hspace{12.5cm}$ (1,R2)
3. $(\square ((p \land q) \land \square ((p \land q) \Rightarrow p)) \Rightarrow \square p$ $\hspace{8.9cm}$ (A2)
4. $((\square ((p \land q) \land \square ((p \land q) \Rightarrow p)) \Rightarrow \square p) \Rightarrow (\square ((p \land q) \Rightarrow p)\Rightarrow (\square (p \land q) \Rightarrow \square p))$ $\hspace{1.1cm}$ (A1)
5. $\square ((p \land q) \Rightarrow p)\Rightarrow (\square (p \land q) \Rightarrow \square p)$ $\hspace{8.5cm}$ (3,4,R1)
6. $\square (p \land q) \Rightarrow \square p$ $\hspace{12.2cm}$ (2,5,R1)

• No, the input to the necessitation rule doesn't have to be a tautology. Commented May 22, 2013 at 12:37
• ... and the necessitation rule R2 is mis-stated, for it is a rule of proof. Commented May 22, 2013 at 14:13
• Thanks for the reference! Just wondering, what is the meaning of "the input to an application of the necessitation rule has to be a theorem but needn't be a tautology in the usual sense"? Commented May 22, 2013 at 14:14
• The rule is if $\varphi$ is a theorem, then so is $\Box\varphi$; that doesn't require $\varphi$ to be a truth-table tautology. For example $\Box P \to P$ is a modal theorem but not a tautology; and we can use necessitation to derive $\Box(\Box P \to P)$. Commented May 22, 2013 at 14:18

Generally in Modal Logic; If $p$ is a theorem; $M^{C}$ , it is true in all worlds in models of the model class; or true in all models in the model class where for a modal logic, for a proposition to be true or satisfied in that model simpliciter, is for for $p$ to be true in all worlds that in that model,$M$;

Then it is true or satisfied in all models,

$M$ in the model class $M^{C}$
$$\forall (M_y;M_y\in M^{C});[\,I^{M}_{y}=\text{dom}(M_y);\forall( w_t) \in I^{M}_{y};[ v^{M_y}(p,w_t) =1]]$$

It is generally meant that $p$ true at all of atomic elements/atomic propositions, in the model's domain $$\forall w \in I^{M}$$ .

For a modal logic, (akin to probability theory) this generally means that, the proposition $p$ is true, in all maximally consistent state of affairs in the model,which are generally taken to be the worlds.

That is the set of all 'p worlds'$[p]$, can be identified with the 'universal set of all worlds' $I^{M}; [p]^{M}=I^{M}$

That is for all worlds $w; w\in I^{M}$ in the domain of the model,$I^{M}$ , $p$ is the case.

$$\forall w \in I^{M}\,; [v(p,w)]=1$$. where $v(p,w)$ is the truth valuation function which determines whether $p$ is true in that world.

The nature of the proposition indicates that the kind of access relation used, and in this, as its an extensional proposition, it only trivial set ${w}$ where $w$ only accesses itself $w$ to determine whether the proposition holds (in all worlds in that set) which is just $w$ (if, its not a modal proposition, for example, but it would generalize regardless), $$p\in [p]^M \subset M^{M}$$

So generally to be a theorem, the proposition is true at all worlds, in all Models, in the Model Class.

As a result $$\Box P$$

Is generally considered to be a theorem (true in all models, in all worlds), even if its not an $S5$ modal logic.

As $p$ is a theorem, and thus is true in every world, in all models, in the model class.

Then for all models, $M$ in the model class, $M^{C}$, it is the case, that:

For every world,$w^{M}$ in the set of all worlds in that model's ($M$) domain,

$$I^{M} ;\forall w^{M} ; w^{M}\in I^{M}$$

Where;

$$w^{M}\in I^{M}$$;

That is, there will be some subset of worlds, call it

$$[,w]^M; [,w]^M\in \mathbb{P}(I^{M})$$

in that set,$I^{M}$ that $w^{M}$ accesses; where in accordance with that model's access relation.

Now regardless of whether that world, $w^{M}$ accesses every other world,$w_j^{M}$ in that model, $M$ or not(or no world at all); it will be the case that $\Box p$ will be true, in all worlds, $w_j^{M}\in$[,w]^M$, in that model. That is, in all worlds$w^{M}$in the model's, domain, It is the case, that for all worlds$w_j^{M}$accessible to that world$w^{M}$,$p$will be true. This,is what meant for$\Box p$true at that world$w^{M}$And this applies to every world in the model. That is, for all worlds in the model, and, the worlds, these worlds access,$w_j^{M}$, are elements of a subset of$I^{M}$,the same set, as the worlds are elements of the domain/the same or same set of worlds in the same model; and$p$is true at every world/element$\in I^{M}$This is because every world,$w_j^{M}$, that$w^{M}$could access, is in that class,$I^{M}$; they are both elements of the domain of the same model • .Thus, it will either be the case that$w^{M}$, accesses some 'non empty subset' of all worlds in$I^{M}$and thus$p$be true in all of its w's accessible worlds and$\Box p$will be true in that world, as its true in all of its accessible worlds (which is what meant by$\Box p$) Commented May 3, 2017 at 9:10 • Or,$p$will be trivially true at$w^{M}$insofar as there are no counter-examples to its truth; Much like in classical logic, or explosion. Commented May 3, 2017 at 9:10 • There exist no accessible worlds to$w^{M}$, and so there exists no possible/accessible$\neg p$worlds for$w^{M}$(no accessible worlds to$w^{M}$in which the proposition$p$is false). Commented May 3, 2017 at 9:11 • So in some sense,$p$is true in all accessible worlds to$w^{M}$, namely the set of all accessible worlds to$w^{M}$and$p$worlds in that model are the same; $$\text{that, is, the empty set}$$ .And so$Box p$will be true, for that world, in that model. But but for similar reasons it will be true in all worlds, in that model; as the set of worlds each world accesses is the same, and it will either entirely consist of$p$worlds as$[p]^{M}=I^{M}$or the empty set, and will be trivially true and$\Box p$will be true$\in$all worlds$w$in that model$M$. Commented May 3, 2017 at 9:11 • That, is for all worlds$wj$, in that model's domain$I^{M}$,$p$is true in every$w_i\in I^{M}$that$wj$accesses. Thus$\Box p$will be true or satisfied in that model (for every world in the models domain,$p$is in worlds accessible that world)And this generalized to every model in the model class. As by assumption it held for all worlds IN ALL Models in that Class,$[,w]^M$]\subset$I^{M}\$, where is the set of all worlds in the model, that the world access, and p is true in all such worlds Commented May 3, 2017 at 9:11

I just wanted to leave a short note related to ByteEater's comment (because it was something I wondered and brought me to this question!):

Let me add a question for clarification: how is it different and if so why preferable to just having p⇒□p as an axiom?

There is a linked question which (imo) was trying to get to the crux of this question, and I think it was inadequately addressed by reference here.

First of all, note that even in the rather strong modal logic S5 it does not hold true that the necessitation rule yields the rule $$\vdash p\to\square p$$. Why is this? Well you can actually come up with a counterexample! To not suck the fun out of it, I leave it as an exercise here:

Find a counterexample to $$\vdash p\to\square p$$ by defining a Kripke model $$\langle W,R,\vDash\rangle$$ in which $$p\to\square p$$ is not a valid formula. For more practice, show that it's not possible in each of modal logics K, T, S4, or S5.

In order to do this exercise, you only need to carefully follow the definition for a Kripke model, and then also just be open to trying new things. :)

Now why does this not work if we have $$p\vdash\square p$$? Should this not automatically suggest that we have $$\vdash p\to\square p$$? Not without a modal version of the Deduction Theorem! This apparently is something we don't have.