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.
Best Answer
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:
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.]