Understanding the modal necessitation rule

Question

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.

Answer 1

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)

Answer 2

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

Answer 3

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