Chapter 43 Natural deduction for ML

We start with a particularly simple system called $𝐊$, in honour of the philosopher and logician Saul Kripke. $𝐊$ includes all of the natural deduction rules from TFL, including the derived rules as well as the basic ones. $𝐊$ then adds a special kind of subproof, plus two new basic rules for $\mathrm{\square }$.

The special kind of subproof looks like an ordinary subproof, except it has a $\mathrm{\square }$in its assumption line instead of a formula. We call them strict subproofs—they allow as to reason and prove things about alternate possibilities. What we can prove inside a strict subproof holds in any alternate possibility, in particular, in alternate possibilities where the assumptions in force in our proof may not hold. In a strict subproofs, all assumptions are disregarded, and we are not allowed to appeal to any lines outside the strict subproof (except as allowed by the modal rules given below).

The $\mathrm{\square }$I rule allows us to derive a formula $\mathrm{\square }𝒜$ if we can derive $𝒜$ inside a strict subproof. It is our fundamental method of introducing $\mathrm{\square }$ into proofs. The basic idea is simple enough: if $𝒜$ is a theorem, then $\mathrm{\square }𝒜$ should be a theorem too. (Remember that to call $𝒜$ a theorem is to say that we can prove $𝒜$ without relying on any undischarged assumptions.)

Suppose we wanted to prove $\mathrm{\square }(A\to A)$. The first thing we need to do is prove that $A\to A$ is a theorem. You already know how to do that using TFL. You simply present a proof of $A\to A$ which doesn’t start with any premises, like this:

It is essential to emphasize that in strict subproof you cannot use any rule which appeals to anything you proved outside of the strict subproof. There are exceptions, e.g., the $\mathrm{\square }$E rule below. These rules will explicitly state that they can be used inside strict subproofs and cite lines outside the strict subproof. This restriction is essential, otherwise we would get terrible results. For example, we could provide the following proof to vindicate $A\therefore \mathrm{\square }A$:

We said above that a strict subproof allows us to reason about arbitrary alternate possible situations. What can be proved in a strict subproof holds in all alternate possible situtations, and so is necessary. This is the idea behind the $\mathrm{\square }$I rule. On the other hand, if we’ve assumed that something is necessary, we have therewith assumed that it is true in all alternate possbile situations. Hence, we have the rule $\mathrm{\square }$E:

$\mathrm{\square }$E allows you to assert $𝒜$ inside a strict subproof if you have $\mathrm{\square }𝒜$ outside the strict subproof. The restriction means that you can only do this in the first strict subproof, you cannot apply the $\mathrm{\square }$E rule inside a nested strict subproof. So the following is not allowed:

Let’s begin with an example.

The rules $\mathrm{\square }$I and $\mathrm{\square }$E look simple enough, and indeed $𝐊$ is a very simple system! But $𝐊$ is more powerful than you might have thought. You can prove a fair few things in it.

In the last subsection, we looked at all of the basic rules for $𝐊$. But you might have noticed that all of these rules were about necessity, $\mathrm{\square }$, and none of them were about possibility, $\mathrm{◇}$. That’s because we can define possibility in terms of necessity:

In other words, to say that $𝒜$ is possibly true, is to say that $𝒜$ is not necessarily false. As a result, it isn’t really essential to add a $\mathrm{◇}$, a special symbol for possibility, into system $𝐊$. Still, the system will be much easier to use if we do, and so we will add the following definitional rules:

Importantly, you should not think of these rules as any real addition to $𝐊$: they just record the way that $\mathrm{◇}$ is defined in terms of $\mathrm{\square }$.

If we wanted, we could leave our rules for $𝐊$ here. But it will be helpful to add some Modal Conversion rules, which give us some more ways of flipping between $\mathrm{\square }$ and $\mathrm{◇}$:

These Modal Conversion Rules are also no addition to the power of $𝐊$, because they can be derived from the basic rules, along with the definition of $\mathrm{◇}$.

In system $𝐊$, using Def$\mathrm{◇}$ (or the modal conversion rules), one can prove $\mathrm{◇}A\leftrightarrow \neg \mathrm{\square }\neg A$. When laying out system $𝐊$, we started with $\mathrm{\square }$ as our primitive modal symbol, and then defined $\mathrm{◇}$ in terms of it. But if we had preferred, we could have started with $\mathrm{◇}$ as our primitive, and then defined $\mathrm{\square }$ as follows: $\mathrm{\square }𝒜{=}_{df}\neg \mathrm{◇}\neg 𝒜$. There is, then, no sense in which necessity is somehow more fundamental than possibility. Necessity and possibility are exactly as fundamental as each other.

So far we have focussed on $𝐊$, which is a very simple modal system. $𝐊$ is so weak that it will not even let you prove $𝒜$ from $\mathrm{\square }𝒜$. But if we are thinking of $\mathrm{\square }$ as expressing necessity, then we will want to be able to make this inference: if $𝒜$ is necessarily true, then it must surely be true!

This leads us to a new system, $𝐓$, which we get by adding the following rule to $𝐊$:

The restriction on rule $𝐓$ is in a way the opposite of the restriction on $\mathrm{\square }$E: you can only use $\mathrm{\square }$E in a nested strict subproof, but you cannot use $𝐓$ in a nested strict subproof.

We can prove things in $𝐓$ which we could not prove in $𝐊$, e.g., $\mathrm{\square }A\to A$.

$𝐓$ allows you to strip away the necessity boxes: from $\mathrm{\square }𝒜$, you may infer $𝒜$. But what if we wanted to add extra boxes? That is, what if we wanted to go from $\mathrm{\square }𝒜$ to $\mathrm{\square }\mathrm{\square }𝒜$? Well, that would be no problem, if we had proved $\mathrm{\square }𝒜$ by applying $\mathrm{\square }$I to a strict subproof of $𝒜$ which itself does not use $\mathrm{\square }$E. In that case, $𝒜$ is a tautology, and by nesting the strict subproof inside another strict subproof and applying $\mathrm{\square }$I again, we can prove $\mathrm{\square }\mathrm{\square }𝒜$. For example, we could prove $\mathrm{\square }\mathrm{\square }(P\to P)$ like this:

This leads us to another new system, $\mathrm{𝐒𝟒}$, which we get by adding the following rule to $𝐓$:

Rule R$\mathrm{𝟒}$ looks just like $\mathrm{\square }$E, except that instead of yielding $𝒜$ from $\mathrm{\square }𝒜$ it yields $\mathrm{\square }𝒜$ inside a strict subproof. The restriction is the same, however: R$\mathrm{𝟒}$ allows us to “import” $\mathrm{\square }𝒜$ into a strict subproof, but not into a strict subproof itself nested inside a strict subproof. However, if that is necessary, an additional application of R$\mathrm{𝟒}$ would have the same result.

Now we can prove even more results. For instance:

In $\mathrm{𝐒𝟒}$, we can always add a box in front of another box. But $\mathrm{𝐒𝟒}$ does not automatically let us add a box in front of a diamond. That is, $\mathrm{𝐒𝟒}$ does not generally permit the inference from $\mathrm{◇}𝒜$ to $\mathrm{\square }\mathrm{◇}𝒜$. But again, that might strike you as a shortcoming, at least if you are reading $\mathrm{\square }$ and $\mathrm{◇}$ as expressing necessity and possibility. It seems intuitive that if $𝒜$ is possibly true, then it couldn’t have failed to be possibly true.

This leads us to our final modal system, $\mathrm{𝐒𝟓}$, which we get by adding the following rule to $\mathrm{𝐒𝟒}$:

This rule allows us to show, for instance, that $\mathrm{◇}\mathrm{\square }A{⊢}_{\mathrm{𝐒𝟓}}\mathrm{\square }A$:

So, as well as adding boxes in front of diamonds, we can also delete diamonds in front of boxes.

We got $\mathrm{𝐒𝟓}$ by adding the rule R$\mathrm{𝟓}$ to $\mathrm{𝐒𝟒}$. In fact, we could have added rule R$\mathrm{𝟓}$ to $𝐓$, left out rule R$\mathrm{𝟒}$, and obtained an equivalent system. That’s because everything we can prove using rule R$\mathrm{𝟒}$ can also be proved using R$𝐓$ together with R$\mathrm{𝟓}$. For instance, here is a proof that shows $\mathrm{\square }A{⊢}_{\mathrm{𝐒𝟓}}\mathrm{\square }\mathrm{\square }A$ without using R$\mathrm{𝟒}$:

The important point about $\mathrm{𝐒𝟓}$ can be put like this: if you have a long string of boxes and diamonds, in any combination whatsoever, you can delete all but the last of them. So for example, $\mathrm{◇}\mathrm{\square }\mathrm{◇}\mathrm{◇}\mathrm{\square }\mathrm{\square }\mathrm{◇}\mathrm{\square }A$ can be simplified down to just $\mathrm{\square }A$.