# Chapter 43 Natural deduction for ML

Now that we know how to make sentences in ML, we can look at how to prove things in ML. We will use $\vdash$ to express provability. So $\mathscr{A}_{1},\mathscr{A}_{2},\dots\mathscr{A}_{n}\vdash\mathscr{C}$ means that $\mathscr{C}$ can be proven from $\mathscr{A}_{1},\mathscr{A}_{2},\dots\mathscr{A}_{n}$. However, we will be looking at a number of different systems of ML, and so it will be useful to add a subscript to indicate which system we are working with. So for example, if we want to say that we can prove $\mathscr{C}$ from $\mathscr{A}_{1},\mathscr{A}_{2},\dots\mathscr{A}_{n}$ in system $\mathbf{K}$, we will write: $\mathscr{A}_{1},\mathscr{A}_{2},\dots\mathscr{A}_{n}\vdash_{\mathbf{K}}% \mathscr{C}$.

## 43.1 System $\mathbf{K}$

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

The special kind of subproof looks like an ordinary subproof, except it has a $\Box$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 $\Box$I rule allows us to derive a formula $\Box\mathscr{A}$ if we can derive $\mathscr{A}$ inside a strict subproof. It is our fundamental method of introducing $\Box$ into proofs. The basic idea is simple enough: if $\mathscr{A}$ is a theorem, then $\Box\mathscr{A}$ should be a theorem too. (Remember that to call $\mathscr{A}$ a theorem is to say that we can prove $\mathscr{A}$ without relying on any undischarged assumptions.)

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

Line number
Subproof level
Formula
Justification
$1$
open subproof, 1
$A$
AS
$2$
1
$A$
R $1$
$3$
close subproof, 0
$A\rightarrow A$
$\rightarrow$I $1$$2$

But to apply $\Box$I, we need to have proven the formula inside a strict subproof. Since our proof of $A\rightarrow A$ makes use of no assumptions at all, this is possible.

Line number
Subproof level
Formula
Justification
$1$
open subproof, 1
$\Box$
AS
$2$
open subproof, 2
$A$
AS
$3$
2
$A$
R $2$
$4$
close subproof, 1
$A\rightarrow A$
$\rightarrow$I $2$$3$
$5$
close subproof, 0
$\Box(A\rightarrow A)$
$\Box$I $1$$4$
Line number
Subproof level
Formula
Justification
$m$
open subproof, 1
$\Box$
AS
$n$
1
$\mathscr{A}$
close subproof, 0
$\Box\mathscr{A}$
$\Box$I $m$$n$

No line above line $m$ may be cited by any rule within the strict subproof begun at line $m$ unless the rule explicitly allows it.

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 $\Box$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\Box A$:

Line number
Subproof level
Formula
Justification
$1$
0
$A$
PR
$2$
open subproof, 1
$\Box$
AS
$3$
1
$A$
incorrect use of R $1$
$4$
close subproof, 0
$\Box A$
$\Box$I $2$$3$

This is not a legitimate proof, because at line 3 we appealed to line 1, even though line 1 comes before the beginning of the strict subproof at line 2.

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 $\Box$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 $\Box$E:

Line number
Subproof level
Formula
Justification
$m$
0
$\Box\mathscr{A}$

open subproof, 1
$\Box$
AS
$n$
1
$\mathscr{A}$
$\Box$E $m$

$\Box$E can only be applied if line $m$ (containing $\Box A$) lies outside of the strict subproof in which line $n$ falls, and this strict subproof is not itself part of a strict subproof not containing $m$.

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

Line number
Subproof level
Formula
Justification
$1$
0
$\Box\mathscr{A}$
$2$
open subproof, 1
$\Box$
AS
$3$
open subproof, 2
$\Box$
AS
$4$
2
$\mathscr{A}$
incorrect use of $\Box$E $1$

The incorrect use of $\Box$E on line $4$ violates the condition, because although line $1$ lies outside the strict subproof in which line $4$ falls, the strict subproof containing line $4$ lies inside the strict subproof beginning on line $2$ which does not contain line $1$.

Let’s begin with an example.

Line number
Subproof level
Formula
Justification
$1$
0
$\Box A$
PR
$2$
0
$\Box B$
PR
$3$
open subproof, 1
$\Box$
AS
$4$
1
$A$
$\Box$E $1$
$5$
1
$B$
$\Box$E $2$
$6$
1
$A\wedge B$
$\wedge$I $4$, $5$
$7$
close subproof, 0
$\Box(A\land B)$
$\Box$I $3$$7$

We can also mix regular subproofs and strict subproofs:

Line number
Subproof level
Formula
Justification
$1$
0
$\Box(A\rightarrow B)$
PR
$2$
open subproof, 1
$\Box A$
AS
$3$
open subproof, 2
$\Box$
AS
$4$
2
$A$
$\Box$E $2$
$5$
2
$A\rightarrow B$
$\Box$E $1$
$6$
2
$B$
$\rightarrow$E $4$, $5$
$7$
close subproof, 1
$\Box B$
$\Box$I $3$$6$
$8$
close subproof, 0
$\Box A\rightarrow\Box B$
$\rightarrow$I $2$$7$

This is called the Distribution Rule, because it tells us that $\Box$ ‘distributes’ over $\rightarrow$.

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

## 43.2 Possibility

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

$\Diamond\mathscr{A}=_{df}\neg\Box\neg\mathscr{A}$

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

Line number
Subproof level
Formula
Justification
$m$
0
$\neg\Box\neg\mathscr{A}$
0
$\Diamond\mathscr{A}$
Def$\Diamond$ $m$
Line number
Subproof level
Formula
Justification
$m$
0
$\Diamond\mathscr{A}$
0
$\neg\Box\neg\mathscr{A}$
Def$\Diamond$ $m$

Importantly, you should not think of these rules as any real addition to $\mathbf{K}$: they just record the way that $\Diamond$ is defined in terms of $\Box$.

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

Line number
Subproof level
Formula
Justification
$m$
0
$\neg\Box\mathscr{A}$
0
$\Diamond\neg\mathscr{A}$
MC $m$
Line number
Subproof level
Formula
Justification
$m$
0
$\Diamond\neg\mathscr{A}$
0
$\neg\Box\mathscr{A}$
MC $m$
Line number
Subproof level
Formula
Justification
$m$
0
$\neg\Diamond\mathscr{A}$
0
$\Box\neg\mathscr{A}$
MC $m$
Line number
Subproof level
Formula
Justification
$m$
0
$\Box\neg\mathscr{A}$
0
$\neg\Diamond\mathscr{A}$
MC $m$

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

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

## 43.3 System $\mathbf{T}$

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

This leads us to a new system, $\mathbf{T}$, which we get by adding the following rule to $\mathbf{K}$:

Line number
Subproof level
Formula
Justification
$m$
0
$\Box\mathscr{A}$
$n$
0
$\mathscr{A}$
R$\mathbf{T}$ $m$

The line $n$ on which rule R$\mathbf{T}$ is applied must not lie in a strict subproof that begins after line $m$.

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

We can prove things in $\mathbf{T}$ which we could not prove in $\mathbf{K}$, e.g., $\Box A\rightarrow A$.

## 43.4 System $\mathbf{S4}$

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

Line number
Subproof level
Formula
Justification
$1$
open subproof, 1
$\Box$
AS
$2$
open subproof, 2
$\Box$
AS
$3$
open subproof, 3
$P$
AS
$4$
3
$P$
R $3$
$5$
close subproof, 2
$P\rightarrow P$
$\rightarrow$I $3$$4$
$6$
close subproof, 1
$\Box(P\rightarrow P)$
$\Box$I $2$$5$
$7$
close subproof, 0
$\Box\Box(P\rightarrow P)$
$\Box$I $1$$6$

But what if we didn’t prove $\Box\mathscr{A}$ in this restricted way, but used $\Box$E inside the strict subproof of $\mathscr{A}$. If we put that strict subproof inside another strict subproof, the requirement of rule $\Box$E to not cite a line containing $\Box\mathscr{A}$ which lies in another strict subproof that has not yet concluded, is violated. Or what if $\Box\mathscr{A}$ were just an assumption we started our proof with? Could we infer $\Box\Box\mathscr{A}$ then? Not in $\mathbf{T}$, we couldn’t. And this might well strike you as a limitation of $\mathbf{T}$, at least if we are reading $\Box$ as expressing necessity. It seems intuitive that if $\mathscr{A}$ is necessarily true, then it couldn’t have failed to be necessarily true.

This leads us to another new system, $\mathbf{S4}$, which we get by adding the following rule to $\mathbf{T}$:

Line number
Subproof level
Formula
Justification
$m$
0
$\Box\mathscr{A}$

open subproof, 1
$\Box$
AS
$n$
1
$\Box\mathscr{A}$
R$\mathbf{4}$ $m$

Note that R$\mathbf{4}$ can only be applied if line $m$ (containing $\Box A$) lies outside of the strict subproof in which line $n$ falls, and this strict subproof is not itself part of a strict subproof not containing $m$.

Rule R$\mathbf{4}$ looks just like $\Box$E, except that instead of yielding $\mathscr{A}$ from $\Box\mathscr{A}$ it yields $\Box\mathscr{A}$ inside a strict subproof. The restriction is the same, however: R$\mathbf{4}$ allows us to “import” $\Box\mathscr{A}$ 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$\mathbf{4}$ would have the same result.

Now we can prove even more results. For instance:

Line number
Subproof level
Formula
Justification
$1$
open subproof, 1
$\Box A$
AS
$2$
open subproof, 2
$\Box$
AS
$3$
2
$\Box A$
R$\mathbf{4}$ $1$
$4$
close subproof, 1
$\Box\Box A$
$\Box$I $2$$3$
$5$
close subproof, 0
$\Box A\rightarrow\Box\Box A$
$\rightarrow$I $1$$6$

Similarly, we can prove $\Diamond\Diamond A\rightarrow\Diamond A$. This shows us that as well as letting us add extra boxes, $\mathbf{S4}$ lets us delete extra diamonds: from $\Diamond\Diamond\mathscr{A}$, you can always infer $\Diamond\mathscr{A}$.

## 43.5 System $\mathbf{S5}$

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

This leads us to our final modal system, $\mathbf{S5}$, which we get by adding the following rule to $\mathbf{S4}$:

Line number
Subproof level
Formula
Justification
$m$
0
$\neg\Box\mathscr{A}$

open subproof, 1
$\Box$
AS
$n$
1
$\neg\Box\mathscr{A}$
R$\mathbf{5}$ $m$

Rule R$\mathbf{5}$ can only be applied if line $m$ (containing $\neg\Box\mathscr{A}$) lies outside of the strict subproof in which line $n$ falls, and this strict subproof is not itself part of a strict subproof not containing line $m$.

This rule allows us to show, for instance, that $\Diamond\Box A\vdash_{\mathbf{S5}}\Box A$:

Line number
Subproof level
Formula
Justification
$1$
0
$\Diamond\Box A$
PR
$2$
0
$\neg\Box\neg\Box A$
Def$\Diamond$ $1$
$3$
open subproof, 1
$\neg\Box A$
AS
$4$
open subproof, 2
$\Box$
AS
$5$
2
$\neg\Box A$
R$\mathbf{5}$ $3$
$6$
close subproof, 1
$\Box\neg\Box A$
$\Box$I $4$$5$
$7$
1
$\bot$
$\neg$E $2$, $6$
$8$
close subproof, 0
$\Box A$
IP $3$$7$

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

We got $\mathbf{S5}$ by adding the rule R$\mathbf{5}$ to $\mathbf{S4}$. In fact, we could have added rule R$\mathbf{5}$ to $\mathbf{T}$, left out rule R$\mathbf{4}$, and obtained an equivalent system. That’s because everything we can prove using rule R$\mathbf{4}$ can also be proved using R$\mathbf{T}$ together with R$\mathbf{5}$. For instance, here is a proof that shows $\Box A\vdash_{\mathbf{S5}}\Box\Box A$ without using R$\mathbf{4}$:

Line number
Subproof level
Formula
Justification
$1$
0
$\Box A$
PR
$2$
open subproof, 1
$\Box\neg\Box A$
AS
$3$
1
$\neg\Box A$
R$\mathbf{T}$ $2$
$4$
1
$\bot$
$\neg$E $1$, $3$
$5$
close subproof, 0
$\neg\Box\neg\Box A$
$\neg$I $2$$4$
$6$
open subproof, 1
$\Box$
AS
$7$
open subproof, 2
$\neg\Box A$
AS
$8$
open subproof, 3
$\Box$
AS
$9$
3
$\neg\Box A$
R$\mathbf{5}$ $7$
$10$
close subproof, 2
$\Box\neg\Box A$
$\Box$I $8$$9$
$11$
2
$\neg\Box\neg\Box A$
R$\mathbf{5}$ $5$
$12$
2
$\bot$
$\neg$E $10$, $11$
$13$
close subproof, 1
$\Box A$
IP $7$$12$
$14$
close subproof, 0
$\Box\Box A$
$\Box$I $6$$13$

$\mathbf{S5}$ is strictly stronger than $\mathbf{S4}$: there are things which can be proved in $\mathbf{S5}$, but not in $\mathbf{S4}$ (e.g., $\Diamond\Box A\rightarrow\Box A$).

The important point about $\mathbf{S5}$ 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, $\Diamond\Box\Diamond\Diamond\Box\Box\Diamond\Box A$ can be simplified down to just $\Box A$.

## Practice exercises

A. Provide proofs for the following:

1. 1.

$\Box(A\wedge B)\vdash_{\mathbf{K}}\Box A\wedge\Box B$

2. 2.

$\Box A\wedge\Box B\vdash_{\mathbf{K}}\Box(A\wedge B)$

3. 3.

$\Box A\vee\Box B\vdash_{\mathbf{K}}\Box(A\vee B)$

4. 4.

$\Box(A\leftrightarrow B)\vdash_{\mathbf{K}}\Box A\leftrightarrow\Box B$

B. Provide proofs for the following (without using Modal Conversion!):

1. 1.

$\neg\Box A\vdash_{\mathbf{K}}\Diamond\neg A$

2. 2.

$\Diamond\neg A\vdash_{\mathbf{K}}\neg\Box A$

3. 3.

$\neg\Diamond A\vdash_{\mathbf{K}}\Box\neg A$

4. 4.

$\Box\neg A\vdash_{\mathbf{K}}\neg\Diamond A$

C. Provide proofs of the following (and now feel free to use Modal Conversion!):

1. 1.

$\Box(A\rightarrow B),\Diamond A\vdash_{\mathbf{K}}\Diamond B$

2. 2.

$\Box A\vdash_{\mathbf{K}}\neg\Diamond\neg A$

3. 3.

$\neg\Diamond\neg A\vdash_{\mathbf{K}}\Box A$

D. Provide proofs for the following:

1. 1.

$P\vdash_{\mathbf{T}}\Diamond P$

2. 2.

$\vdash_{\mathbf{T}}(A\wedge B)\vee(\neg\Box A\vee\neg\Box B)$

E. Provide proofs for the following:

1. 1.

$\Box(\Box A\rightarrow B),\Box(\Box B\rightarrow C),\Box A\vdash_{\mathbf{S4}}% \Box\Box C$

2. 2.

$\Box A\vdash_{\mathbf{S4}}\Box(\Box A\vee B)$

3. 3.

$\Diamond\Diamond A\vdash_{\mathbf{S4}}\Diamond A$

F. Provide proofs in $\mathbf{S5}$ for the following:

1. 1.

$\neg\Box\neg A,\Diamond B\vdash_{\mathbf{S5}}\Box(\Diamond A\wedge\Diamond B)$

2. 2.

$A\vdash_{\mathbf{S5}}\Box\Diamond A$

3. 3.

$\Diamond\Diamond A\vdash_{\mathbf{S5}}\Diamond A$