To help us reason with modal notions, we may intuitively appeal
to the notion of a possible world, i.e., a way things might have gone.
Our world is just one possible world of an infinite number of such
worlds. For now, let us suppose this idea is well-understood (in
*Principia Metaphysica* it can be precisely defined). Using
the notion of a possible world, we may intuitively think of the claim:

**Instance of Axiom 1**:

**Instance of Axiom 2**:

**Instance of Axiom 3**:

**Instances of Axiom 4: Barcan Formulas**:

**Metatheorem: Derived Rule of Necessitation (RN)**:
For convenience, we reproduce the item Logic/Rule of Necessitation
from *Principia Metaphysica*:

In the usual formulation of modal logic, the Rule of
Necessitation is taken as a primitive rule of inference. The axioms
of the system do *not* include the modal closures of the logical
axioms. In such formulations, it is assumed that all of the logical
axioms are necessary truths. So anything derivable solely from such
necessary truths will themselves be necessary, and so RN never takes
us from truth to falsehood. However, when formulating a modal logic
in which one of the logical axioms is not a necessary truth, RN must
be restricted. It works normally in any proof where the conclusion
rests only on logical axioms that are necessary, but when the
conclusion rests on a logical axiom that is not necessary, the
application of RN is invalid. For example, on one construal, the
conditional claim *if it is actually the case that p (is true),
then p (is true)* is a logical truth but not a necessary truth.
This conditional is logically true because it is part of the very
meaning of the operator *it is actually the case that* that any
proposition it applies to is true. However, to see that it is not a
necessary truth suppose that *p* is true in the actual world
and consider a different world where *p* is false. At that
world, call it *w*, the antecedent, *it is actually the case
that p is true*, is still true there, because on this construal,
the operator *it is actually the case that* looks back to the
actual world to see whether *p* is true (and since, by
hypothesis, we are assuming that *p* is true at the actual
world, *it is actually the case that p* is true at world
*w*). But the consequence *p is true* is false at world
*w*, by hypothesis. Since there is a possible world, namely,
*w*, where our conditional is false, it is not a necessary
truth. So we do not want to be able to use the Rule of Necessitation
upon the logical truth *if it is actually the case that p, then
p*, because this is not a necessary truth. Any system that allows
such an operator has to restrict RN.

But modal logic can easily accomodate such contingent, nonmodal
logical axioms and still remain classical. The technique is simply to
include as axioms all of the modal closures of the `modal' logical
axioms. Then the Rule of Necessitation can be derived. The proof is
in *Principia Metaphysica* (in the Appendix, look for the item
number that currently corresponds to the item Logic/Rule of
Necessitation). RN behaves classically in cases where the derivation
involves only necessary truths. Notice that our formulation of RN
allows us to apply the rule to consequences derived from non-logical
premises, as long as those non-logical premises are also necessary.
We may not apply the rule to consequences of contingent premises. For
example, it is a contingent fact that *Clinton is a
politician*. But we may not use RN to give us a
proof of *Necessarily, Clinton is a politician* from the
contingent premise *Clinton is a politician*.

**Derived Theorem: Rule K**

**Theorem: Modal Modus Ponens**

Consider an arbitrary worldThe present theorem underlies and grounds this kind of reasoning.w. Sinceif p then qis a necessary truth, it is true at all possible worlds, and so it is true atw. Sincepis also a necessary truth, it too is true at all possible worlds and so is true atw. But since bothif p then qandpare true atw,qis true atw(since the modal laws of logic apply to every possible world. But we have just proved thatqis true at an arbitrarily chosen possible world. Soqis true at every possible world, and so is a necessary truth. ThusNecessarily q.

It is easy to prove Modal Modus Ponens, given Axiom 1 of modal logic. Consider the following sequence of formulas:

**(Logical) Theorems: **

Given the premiseThe first theorem, therefore, guarantees the validity of this sort of reasoning. From it, we may derive the logical theorem listed immediately below it, by using the Deduction Theorem.Possibly p, we know thatpis true at some possible world. So pick an arbitrary world wherepis true (we know there must be at least one) and call itw. Since our other premise isNecessarily, if p then q, we know that the conditionalif p then qis true at every possible world, and in particular, it is true atw. But since bothif p then qandpare true atw,qis true atw. Sincewwas an arbitrarily chosen world, we know that from the point of view of the actual world thatqis true at some possible world. SoPossibly q.

**Logical Theorem: Converse Barcan Formula**

Since Axiom 4 tells us that the domains of quantification at other possible worlds do not increase in size over (i.e., do not contain objects not already in) the domain of quantification at the actual world, and the present theorem tells us that the domain of quantification at other possible worlds do not decrease in size from the domain of the actual world, we know that the domain of quantification stays fixed from world to world. This `fixed domain' of quantification is the simplest kind of quantified modal logic.

**Logical Theorems: Equivalent Expression of the Barcan
Formula **