Chapter 17 Basic rules for TFL
We will develop a natural deduction system. For each connective, there will be introduction rules, that allow us to prove a sentence that has that connective as the main logical operator, and elimination rules, that allow us to prove something given a sentence that has that connective as the main logical operator.
17.1 The idea of a formal proof
A formal proof or derivation is a sequence of sentences, some of which are marked as being initial assumptions (or premises). The last line of the formal proof is the conclusion. (Henceforth, we will simply call these ‘proofs’ or ‘derivations’, but be aware that there are informal proofs too.)
As an illustration, consider:
We will start a proof by writing the premise:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\mathrm{\neg}(A\vee B)$

PR

Note that we have numbered the premise, since we will want to refer back to it. Indeed, every line of the proof is numbered, so that we can refer back to it.
Note also that we have drawn a line underneath the premise. Everything written above the line is an assumption. Everything written below the line will either be something which follows from the assumptions, or it will be some new assumption. We are hoping to conclude ‘$\mathrm{\neg}A\wedge \mathrm{\neg}B$’; so we are hoping ultimately to conclude our proof with
Line number

Subproof level

Formula

Justification


$n$ 
0

$\mathrm{\neg}A\wedge \mathrm{\neg}B$


for some number $n$. It doesn’t matter what line number we end on, but we would obviously prefer a short proof to a long one.
Similarly, suppose we wanted to consider:
The argument has three premises, so we start by writing them all down, numbered, and drawing a line under them:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\vee B$

PR

$2$ 
0

$\mathrm{\neg}(A\wedge C)$

PR

$3$ 
0

$\mathrm{\neg}(B\wedge \mathrm{\neg}D)$

PR

and we are hoping to conclude with some line:
Line number

Subproof level

Formula

Justification


$n$ 
0

$\mathrm{\neg}C\vee D$


All that remains to do is to explain each of the rules that we can use along the way from premises to conclusion. The rules are broken down by our logical connectives.
17.2 Reiteration
The very first rule is so breathtakingly obvious that it is surprising we bother with it at all.
If you already have shown something in the course of a proof, the reiteration rule allows you to repeat it on a new line. For example:
Line number

Subproof level

Formula

Justification


$4$ 
0

$A\wedge B$


0

$\mathrm{\vdots}$



$10$ 
0

$A\wedge B$

R $4$

This indicates that we have written ‘$A\wedge B$’ on line $4$. Now, at some later line—line $10$, for example—we have decided that we want to repeat this. So we write it down again. We also add a citation which justifies what we have written. In this case, we write ‘R’, to indicate that we are using the reiteration rule, and we write ‘$4$’, to indicate that we have applied it to line $4$.
Here is a general expression of the rule:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

R $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

The point is that, if any sentence $\mathcal{A}$ occurs on some line, then we can repeat $\mathcal{A}$ on later lines. Each line of our proof must be justified by some rule, and here we have ‘R $m$’. This means: Reiteration, applied to line $m$.
Two things need emphasizing. First ‘$\mathcal{A}$’ is not a sentence of TFL. Rather, it a symbol in the metalanguage, which we use when we want to talk about any sentence of TFL (see chapter 8). Second, and similarly, ‘$m$’ is not a symbol that will appear on a proof. Rather, it is a symbol in the metalanguage, which we use when we want to talk about any line number of a proof. In an actual proof, the lines are numbered ‘$1$’, ‘$2$’, ‘$3$’, and so forth. But when we define the rule, we use variables like ‘$m$’ to underscore the point that the rule may be applied at any point.
17.3 Conjunction
Suppose we want to show that Ludwig is both reactionary and libertarian. One obvious way to do this would be as follows: first we show that Ludwig is reactionary; then we show that Ludwig is libertarian; then we put these two demonstrations together, to obtain the conjunction.
Our natural deduction system will capture this thought straightforwardly. In the example given, we might adopt the following symbolization key:
 $R$:

Ludwig is reactionary
 $L$:

Ludwig is libertarian
Perhaps we are working through a proof, and we have obtained ‘$R$’ on line $8$ and ‘$L$’ on line $15$. Then on any subsequent line we can obtain ‘$R\wedge L$’ thus:
Line number

Subproof level

Formula

Justification


$8$ 
0

$R$


$15$ 
0

$L$


0

$R\wedge L$

$\wedge $I $8$, $15$

Note that every line of our proof must either be an assumption, or must be justified by some rule. We cite ‘$\wedge $I $8$, $15$’ here to indicate that the line is obtained by the rule of conjunction introduction ($\wedge $I) applied to lines $8$ and $15$. We could equally well obtain:
Line number

Subproof level

Formula

Justification


$8$ 
0

$R$


$15$ 
0

$L$


0

$L\wedge R$

$\wedge $I $15$, $8$

with the citation reversed, to reflect the order of the conjuncts. More generally, here is our conjunction introduction rule:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$

To be clear, the statement of the rule is schematic. It is not itself a proof. ‘$\mathcal{A}$’ and ‘$\mathcal{B}$’ are not sentences of TFL. Rather, they are symbols in the metalanguage, which we use when we want to talk about any sentence of TFL (see chapter 8). Similarly, ‘$m$’ and ‘$n$’ are not numerals that will appear in any actual proof. Rather, they are symbols in the metalanguage, which we use when we want to talk about any line number of any proof. In an actual proof, the lines are numbered ‘$1$’, ‘$2$’, ‘$3$’, and so forth, but when we define the rule, we use variables to emphasize that the rule may be applied at any point. The rule requires only that we have both conjuncts available to us somewhere earlier in the proof. They can be separated from one another, and they can appear in any order.
The rule is called ‘conjunction introduction’ because it introduces the symbol ‘$\wedge $’ into our proof where it may have been absent. Correspondingly, we have a rule that eliminates that symbol. Suppose you have shown that Ludwig is both reactionary and libertarian. You are entitled to conclude that Ludwig is reactionary. Equally, you are entitled to conclude that Ludwig is libertarian. Putting this together, we obtain our conjunction elimination rule(s):
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

and equally:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

The point is simply that, when you have a conjunction on some line of a proof, you can obtain either of the conjuncts by $\wedge $E. One point is worth emphasising: you can only apply this rule when conjunction is the main logical operator. So you cannot infer ‘$D$’ just from ‘$C\vee (D\wedge E)$’!
Even with just these two rules, we can start to see some of the power of our formal proof system. Consider:

$[(A\vee B)\to (C\vee D)]\wedge [(E\vee F)\to (G\vee H)]$

∴
$[(E\vee F)\to (G\vee H)]\wedge [(A\vee B)\to (C\vee D)]$
The main logical operator in both the premise and conclusion of this argument is ‘$\wedge $’. In order to provide a proof, we begin by writing down the premise, which is our assumption. We draw a line below this: everything after this line must follow from our assumptions by (repeated applications of) our rules of inference. So the beginning of the proof looks like this:
Line number

Subproof level

Formula

Justification


$1$ 
0

$[(A\vee B)\to (C\vee D)]\wedge [(E\vee F)\to (G\vee H)]$

PR

From the premise, we can get each of the conjuncts by $\wedge $E. The proof now looks like this:
Line number

Subproof level

Formula

Justification


$1$ 
0

$[(A\vee B)\to (C\vee D)]\wedge [(E\vee F)\to (G\vee H)]$

PR

$2$ 
0

$[(A\vee B)\to (C\vee D)]$

$\wedge $E $1$

$3$ 
0

$[(E\vee F)\to (G\vee H)]$

$\wedge $E $1$

So by applying the $\wedge $I rule to lines 3 and 2 (in that order), we arrive at the desired conclusion. The finished proof looks like this:
Line number

Subproof level

Formula

Justification


$1$ 
0

$[(A\vee B)\to (C\vee D)]\wedge [(E\vee F)\to (G\vee H)]$

PR

$2$ 
0

$[(A\vee B)\to (C\vee D)]$

$\wedge $E $1$

$3$ 
0

$[(E\vee F)\to (G\vee H)]$

$\wedge $E $1$

$4$ 
0

$[(E\vee F)\to (G\vee H)]\wedge [(A\vee B)\to (C\vee D)]$

$\wedge $I $3$, $2$

This is a very simple proof, but it shows how we can chain rules of proof together into longer proofs. In passing, note that investigating this argument with a truth table would have required 256 lines; our formal proof required only four lines.
It is worth giving another example. Back in section 11.3, we noted that this argument is valid:
To provide a proof corresponding to this argument, we start by writing:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\wedge (B\wedge C)$

PR

From the premise, we can get each of the conjuncts by applying $\wedge $E twice. We can then apply $\wedge $E twice more, so our proof looks like:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\wedge (B\wedge C)$

PR

$2$ 
0

$A$

$\wedge $E $1$

$3$ 
0

$B\wedge C$

$\wedge $E $1$

$4$ 
0

$B$

$\wedge $E $3$

$5$ 
0

$C$

$\wedge $E $3$

But now we can merrily reintroduce conjunctions in the order we wanted them, so that our final proof is:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\wedge (B\wedge C)$

PR

$2$ 
0

$A$

$\wedge $E $1$

$3$ 
0

$B\wedge C$

$\wedge $E $1$

$4$ 
0

$B$

$\wedge $E $3$

$5$ 
0

$C$

$\wedge $E $3$

$6$ 
0

$A\wedge B$

$\wedge $I $2$, $4$

$7$ 
0

$(A\wedge B)\wedge C$

$\wedge $I $6$, $5$

Recall that our official definition of sentences in TFL only allowed conjunctions with two conjuncts. The proof just given suggests that we could drop inner brackets in all of our proofs. However, this is not standard, and we will not do this. Instead, we will maintain our more austere bracketing conventions. (Though we will still allow ourselves to drop outermost brackets, for legibility.)
Let’s give one final illustration. When using the $\wedge $I rule, there is no requirement to apply it to different sentences. So, if we want, we can formally prove ‘$A\wedge A$’ from ‘$A$’ thus:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
0

$A\wedge A$

$\wedge $I $1$, $1$

Simple, but effective.
17.4 Conditional
Consider the following argument:

If Jane is smart then she is fast.

Jane is smart.

∴
Jane is fast.
This argument is certainly valid, and it suggests a straightforward conditional elimination rule ($\to $E):
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$

This rule is also sometimes called modus ponens. Again, this is an elimination rule, because it allows us to obtain a sentence that may not contain ‘$\to $’, having started with a sentence that did contain ‘$\to $’. Note that the conditional $\mathcal{A}\to \mathcal{B}$ and the antecedent $\mathcal{A}$ can be separated from one another in the proof, and they can appear in any order. However, in the citation for $\to $E, we always cite the conditional first, followed by the antecedent.
The rule for conditional introduction is also quite easy to motivate. The following argument should be valid:

Ludwig is reactionary.

∴
If Ludwig is libertarian, then Ludwig is both reactionary and libertarian.
If someone doubted that this was valid, we might try to convince them otherwise by explaining ourselves as follows:
Assume that Ludwig is reactionary. Now, additionally assume that Ludwig is libertarian. Then by conjunction introduction—which we just discussed—Ludwig is both reactionary and libertarian. Of course, that’s conditional on the assumption that Ludwig is libertarian. But this just means that, if Ludwig is libertarian, then he is both reactionary and libertarian.
Transferred into natural deduction format, here is the pattern of reasoning that we just used. We started with one premise, ‘Ludwig is reactionary’, thus:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R$

PR

The next thing we did is to make an additional assumption (‘Ludwig is libertarian’), for the sake of argument. To indicate that we are no longer dealing merely with our original premise (‘$R$’), but with some additional assumption, we continue our proof as follows:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R$

PR

$2$ 
open subproof,
1

$L$

AS

Note that we are not claiming, on line $2$, to have proved ‘$L$’ from line $1$, so we do not write in any justification for the additional assumption on line $2$. We do, however, need to mark that it is an additional assumption. We do this by drawing a line under it (to indicate that it is an assumption) and by indenting it with a further vertical line (to indicate that it is additional).
With this extra assumption in place, we are in a position to use $\wedge $I. So we can continue our proof:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R$

PR

$2$ 
open subproof,
1

$L$

AS

$3$ 
1

$R\wedge L$

$\wedge $I $1$, $2$

So we have now shown that, on the additional assumption, ‘$L$’, we can obtain ‘$R\wedge L$’. We can therefore conclude that, if ‘$L$’ obtains, then so does ‘$R\wedge L$’. Or, to put it more briefly, we can conclude ‘$L\to (R\wedge L)$’:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R$

PR

$2$ 
open subproof,
1

$L$

AS

$3$ 
1

$R\wedge L$

$\wedge $I $1$, $2$

$4$ 
close subproof,
0

$L\to (R\wedge L)$

$\to $I $2$–$3$

Observe that we have dropped back to using one vertical line on the left. We have discharged the additional assumption, ‘$L$’, since the conditional itself follows just from our original assumption, ‘$R$’.
The general pattern at work here is the following. We first make an additional assumption, $\mathcal{A}$; and from that additional assumption, we prove $\mathcal{B}$. In that case, we know the following: If $\mathcal{A}$ is true, then $\mathcal{B}$ is true. This is wrapped up in the rule for conditional introduction:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$ 
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


close subproof,
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$

There can be as many or as few lines as you like between lines $i$ and $j$.
It will help to offer a second illustration of $\to $I in action. Suppose we want to consider the following:
We start by listing both of our premises. Then, since we want to arrive at a conditional (namely, ‘$P\to R$’), we additionally assume the antecedent to that conditional. Thus our main proof starts:
Line number

Subproof level

Formula

Justification


$1$ 
0

$P\to Q$

PR

$2$ 
0

$Q\to R$

PR

$3$ 
open subproof,
1

$P$

AS

Note that we have made ‘$P$’ available, by treating it as an additional assumption, but now, we can use $\to $E on the first premise. This will yield ‘$Q$’. We can then use $\to $E on the second premise. So, by assuming ‘$P$’ we were able to prove ‘$R$’, so we apply the $\to $I rule—discharging ‘$P$’—and finish the proof. Putting all this together, we have:
Line number

Subproof level

Formula

Justification


$1$ 
0

$P\to Q$

PR

$2$ 
0

$Q\to R$

PR

$3$ 
open subproof,
1

$P$

AS

$4$ 
1

$Q$

$\to $E $1$, $3$

$5$ 
1

$R$

$\to $E $2$, $4$

$6$ 
close subproof,
0

$P\to R$

$\to $I $3$–$5$

17.5 Additional assumptions and subproofs
The rule $\to $I invoked the idea of making additional assumptions. These need to be handled with some care. Consider this proof:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
open subproof,
1

$B$

AS

$3$ 
1

$B$

R $2$

$4$ 
close subproof,
0

$B\to B$

$\to $I $2$–$3$

This is perfectly in keeping with the rules we have laid down already, and it should not seem particularly strange. Since ‘$B\to B$’ is a tautology, no particular premises should be required to prove it.
But suppose we now tried to continue the proof as follows:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
open subproof,
1

$B$

AS

$3$ 
1

$B$

R $2$

$4$ 
close subproof,
0

$B\to B$

$\to $I $2$–$3$

$5$ 
0

$B$

naughty attempt to invoke $\to $E $4$, $3$

If we were allowed to do this, it would be a disaster. It would allow us to prove any sentence letter from any other sentence letter. However, if you tell me that Anne is fast (symbolized by ‘$A$’), we shouldn’t be able to conclude that Queen Boudica stood twentyfeet tall (symbolized by ‘$B$’)! We must be prohibited from doing this, but how are we to implement the prohibition?
We can describe the process of making an additional assumption as one of performing a subproof: a subsidiary proof within the main proof. When we start a subproof, we draw another vertical line to indicate that we are no longer in the main proof. Then we write in the assumption upon which the subproof will be based. A subproof can be thought of as essentially posing this question: what could we show, if we also make this additional assumption?
When we are working within the subproof, we can refer to the additional assumption that we made in introducing the subproof, and to anything that we obtained from our original assumptions. (After all, those original assumptions are still in effect.) At some point though, we will want to stop working with the additional assumption: we will want to return from the subproof to the main proof. To indicate that we have returned to the main proof, the vertical line for the subproof comes to an end. At this point, we say that the subproof is closed . Having closed a subproof, we have set aside the additional assumption, so it will be illegitimate to draw upon anything that depends upon that additional assumption. Thus we stipulate:
To cite an individual line when applying a rule:

1.
the line must come before the line where the rule is applied, but

2.
not occur within a subproof that has been closed before the line where the rule is applied.
This stipulation rules out the disastrous attempted proof above. The application of rule $\to $E on line $5$ requires that we cite two individual lines from earlier in the proof. One of these lines (namely, line $3$) occurs within a subproof (lines $2$–$3$). By line $5$, where we have to cite line $3$, the subproof has been closed. This is illegitimate: we are not allowed to cite line $3$ on line $5$.
Closing a subproof is called discharging the assumptions of that subproof. So we can put the point this way: you cannot refer back to anything that was obtained using discharged assumptions.
Subproofs, then, allow us to think about what we could show, if we made additional assumptions. The point to take away from this is not surprising—in the course of a proof, we have to keep very careful track of what assumptions we are making, at any given moment. Our proof system does this very graphically. (Indeed, that’s precisely why we have chosen to use this proof system.)
Once we have started thinking about what we can show by making additional assumptions, nothing stops us from posing the question of what we could show if we were to make even more assumptions? This might motivate us to introduce a subproof within a subproof. Here is an example using only the rules which we have considered so far:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
open subproof,
1

$B$

AS

$3$ 
open subproof,
2

$C$

AS

$4$ 
2

$A\wedge B$

$\wedge $I $1$, $2$

$5$ 
close subproof,
1

$C\to (A\wedge B)$

$\to $I $3$–$4$

$6$ 
close subproof,
0

$B\to (C\to (A\wedge B))$

$\to $I $2$–$5$

Notice that the citation on line $4$ refers back to the initial assumption (on line $1$) and an assumption of a subproof (on line $2$). This is perfectly in order, since neither assumption has been discharged at the time (i.e., by line $4$).
Again, though, we need to keep careful track of what we are assuming at any given moment. Suppose we tried to continue the proof as follows:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
open subproof,
1

$B$

AS

$3$ 
open subproof,
2

$C$

AS

$4$ 
2

$A\wedge B$

$\wedge $I $1$, $2$

$5$ 
close subproof,
1

$C\to (A\wedge B)$

$\to $I $3$–$4$

$6$ 
close subproof,
0

$B\to (C\to (A\wedge B))$

$\to $I $2$–$5$

$7$ 
0

$C\to (A\wedge B)$

naughty attempt to invoke $\to $I $3$–$4$

This would be awful. If we tell you that Anne is smart, you should not be able to infer that, if Cath is smart (symbolized by ‘$C$’) then both Anne is smart and Queen Boudica stood 20 feet tall! But this is just what such a proof would suggest, if it were permissible.
The essential problem is that the subproof that began with the assumption ‘$C$’ depended crucially on the fact that we had assumed ‘$B$’ on line $2$. By line $6$, we have discharged the assumption ‘$B$’: we have stopped asking ourselves what we could show, if we also assumed ‘$B$’. So it is simply cheating, to try to help ourselves (on line $7$) to the subproof that began with the assumption ‘$C$’. Thus we stipulate, much as before, that a subproof can only be cited on a line if it does not occur within some other subproof which is already closed at that line. The attempted disastrous proof violates this stipulation. The subproof of lines $3$–$4$ occurs within a subproof that ends on line $5$. So it cannot be invoked on line $7$.
Here is one further case we have to exclude:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
open subproof,
1

$B$

AS

$3$ 
open subproof,
2

$C$

AS

$4$ 
2

$B\wedge C$

$\wedge $I $2$, $3$

$5$ 
2

$C$

$\wedge $E $4$

$6$ 
close subproof,
0

$B\to C$

naughty attempt to invoke $\to $I $2$–$5$

Here we are trying to cite a subproof that begins on line $2$ and ends on line $5$—but the sentence on line $5$ depends not only on the assumption on line $2$, but also on one another assumption (line $3$) which we have not discharged at the end of the subproof. The subproof started on line $3$ is still open at line $3$. But $\to $I requires that the last line of the subproof only relies on the assumption of the subproof being cited, i.e., the subproof beginning on line $2$ (and anything before it), and not on assumptions of any subproofs within it. In particular, the last line of the subproof cited must not itself lie within a nested subproof.
One last point to emphasize how rules can be applied: where a rule requires you to cite an individual line, you cannot cite a subproof instead; and where it requires you to cite a subproof, you cannot cite an individual line instead. So for instance, this is incorrect:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A$

PR

$2$ 
open subproof,
1

$B$

AS

$3$ 
open subproof,
2

$C$

AS

$4$ 
2

$B\wedge C$

$\wedge $I $2$, $3$

$5$ 
2

$C$

$\wedge $E $4$

$6$ 
close subproof,
1

$C$

naughty attempt to invoke R $3$–$5$

$7$ 
close subproof,
0

$B\to C$

$\to $I $2$–$6$

Here, we have tried to justify $C$ on line $6$ by the reiteration rule, but we have cited the subproof on lines $3$–$5$ with it. That subproof is closed and can in principle be cited on line $6$. (For instance, we could use it to justify $C\to C$ by $\to $I.) But the reiteration rule R requires you to cite an individual line, so citing the entire subproof is inadmissible (even if that subproof contains the sentence $C$ we want to reiterate).
It is always permissible to open a subproof with any assumption. However, there is some strategy involved in picking a useful assumption. Starting a subproof with an arbitrary, wacky assumption would just waste lines of the proof. In order to obtain a conditional by $\to $I, for instance, you must assume the antecedent of the conditional in a subproof.
Equally, it is always permissible to close a subproof (and discharge its assumptions). However, it will not be helpful to do so until you have reached something useful. Once the subproof is closed, you can only cite the entire subproof in any justification. Those rules that call for a subproof or subproofs, in turn, require that the last line of the subproof is a sentence of some form or other. For instance, you are only allowed to cite a subproof for $\to $I if the line you are justifying is of the form $\mathcal{A}\to \mathcal{B}$, $\mathcal{A}$ is the assumption of your subproof, and $\mathcal{B}$ is the last line of your subproof.
17.6 Biconditional
The rules for the biconditional will be like doublebarrelled versions of the rules for the conditional.
In order to prove ‘$F\leftrightarrow G$’, for instance, you must be able to prove ‘$G$’ on the assumption ‘$F$’ and prove ‘$F$’ on the assumption ‘$G$’. The biconditional introduction rule ($\leftrightarrow $I) therefore requires two subproofs. Schematically, the rule works like this:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$ 
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$k$}$ 
close subproof,
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$l$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


close subproof,
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$k$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$l$}$

There can be as many lines as you like between $i$ and $j$, and as many lines as you like between $k$ and $l$. Moreover, the subproofs can come in any order, and the second subproof does not need to come immediately after the first.
The biconditional elimination rule ($\leftrightarrow $E) lets you do a bit more than the conditional rule. If you have the lefthand subsentence of the biconditional, you can obtain the righthand subsentence. If you have the righthand subsentence, you can obtain the lefthand subsentence. So we allow:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$

and equally:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$

Note that the biconditional, and the right or left half, can be separated from one another, and they can appear in any order. However, in the citation for $\leftrightarrow $E, we always cite the biconditional first.
17.7 Disjunction
Suppose Ludwig is reactionary. Then Ludwig is either reactionary or libertarian. After all, to say that Ludwig is either reactionary or libertarian is to say something weaker than to say that Ludwig is reactionary.
Let’s emphasize this point. Suppose Ludwig is reactionary. It follows that Ludwig is either reactionary or a kumquat. Equally, it follows that either Ludwig is reactionary or kumquats are the only fruit. Equally, it follows that either Ludwig is reactionary or God is dead. Many of these are strange inferences to draw, but there is nothing logically wrong with them (even if they maybe violate all sorts of implicit conversational norms).
Armed with all this, we present the disjunction introduction rule(s):
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

and
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

Notice that $\mathcal{B}$ can be any sentence whatsoever, so the following is a perfectly acceptable proof:
Line number

Subproof level

Formula

Justification


$1$ 
0

$M$

PR

$2$ 
0

$M\vee ([(A\leftrightarrow B)\to (C\wedge D)]\leftrightarrow [E\wedge F])$

$\vee $I $1$

Using a truth table to show this would have taken 128 lines.
The disjunction elimination rule is slightly trickier. Suppose that either Ludwig is reactionary or he is libertarian. What can you conclude? Not that Ludwig is reactionary; it might be that he is libertarian instead. Equally, not that Ludwig is libertarian; for he might merely be reactionary. Disjunctions, just by themselves, are hard to work with.
But suppose that we could somehow show both of the following: first, that Ludwig’s being reactionary entails that he is an Austrian economist; second, that Ludwig’s being libertarian entails that he is an Austrian economist. Then if we know that Ludwig is either reactionary or libertarian, then we know that, whichever he is, Ludwig is an Austrian economist. This insight can be expressed in the following rule, which is our disjunction elimination ($\vee $E) rule:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$ 
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{C}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$k$}$ 
close subproof,
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$l$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{C}$}$


close subproof,
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{C}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$k$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$l$}$

This is obviously a bit clunkier to write down than our previous rules, but the point is fairly simple. Suppose we have some disjunction, $\mathcal{A}\vee \mathcal{B}$. Suppose we have two subproofs, showing us that $\mathcal{C}$ follows from the assumption that $\mathcal{A}$, and that $\mathcal{C}$ follows from the assumption that $\mathcal{B}$. Then we can infer $\mathcal{C}$ itself. As usual, there can be as many lines as you like between $i$ and $j$, and as many lines as you like between $k$ and $l$. Moreover, the subproofs and the disjunction can come in any order, and do not have to be adjacent.
Some examples might help illustrate this. Consider this argument:
An example proof might run thus:
Line number

Subproof level

Formula

Justification


$1$ 
0

$(P\wedge Q)\vee (P\wedge R)$

PR

$2$ 
open subproof,
1

$P\wedge Q$

AS

$3$ 
1

$P$

$\wedge $E $2$

$4$ 
close subproof,
open subproof,
1

$P\wedge R$

AS

$5$ 
1

$P$

$\wedge $E $4$

$6$ 
close subproof,
0

$P$

$\vee $E $1$, $2$–$3$, $4$–$5$

Here is a slightly harder example. Consider:
Here is a proof corresponding to this argument:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\wedge (B\vee C)$

PR

$2$ 
0

$A$

$\wedge $E $1$

$3$ 
0

$B\vee C$

$\wedge $E $1$

$4$ 
open subproof,
1

$B$

AS

$5$ 
1

$A\wedge B$

$\wedge $I $2$, $4$

$6$ 
1

$(A\wedge B)\vee (A\wedge C)$

$\vee $I $5$

$7$ 
close subproof,
open subproof,
1

$C$

AS

$8$ 
1

$A\wedge C$

$\wedge $I $2$, $7$

$9$ 
1

$(A\wedge B)\vee (A\wedge C)$

$\vee $I $8$

$10$ 
close subproof,
0

$(A\wedge B)\vee (A\wedge C)$

$\vee $E $3$, $4$–$6$, $7$–$9$

Don’t be alarmed if you think that you wouldn’t have been able to come up with this proof yourself. The ability to come up with novel proofs comes with practice, and we’ll cover some strategies for finding proofs in chapter 18. The key question at this stage is whether, looking at the proof, you can see that it conforms to the rules that we have laid down. That just involves checking every line, and making sure that it is justified in accordance with the rules we have laid down.
17.8 Contradiction and negation
We have only one connective left to deal with: negation. But to tackle it, we must connect negation with contradiction.
An effective form of argument is to argue your opponent into contradicting themselves. At that point, you have them on the ropes. They have to give up at least one of their assumptions. We are going to make use of this idea in our proof system, by adding a new symbol, ‘$\perp $’, to our proofs. This should be read as something like ‘contradiction!’ or ‘reductio!’ or ‘but that’s absurd!’ The rule for introducing this symbol is that we can use it whenever we explicitly contradict ourselves, i.e., whenever we find both a sentence and its negation appearing in our proof:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\perp $}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$n$}$

It does not matter what order the sentence and its negation appear in, and they do not need to appear on adjacent lines. However, we always cite the line number of the negation first, followed by that of the sentence it is a negation of.
There is obviously a tight link between contradiction and negation. The rule $\mathrm{\neg}$E lets us proceed from two contradictory sentences—$\mathcal{A}$ and its negation $\mathrm{\neg}\mathcal{A}$—to an explicit contradiction $\perp $. We choose the label for a reason: it is the most basic rule that lets us proceed from a premise containing a negation, i.e., $\mathrm{\neg}\mathcal{A}$, to a sentence not containing it, i.e., $\perp $. So it is a rule that eliminates $\mathrm{\neg}$.
We have said that ‘$\perp $’ should be read as something like ‘contradiction!’ but this does not tell us much about the symbol. There are, roughly, three ways to approach the symbol.

1.
We might regard ‘$\perp $’ as a new atomic sentence of TFL, but one which can only ever have the truth value False.

2.
We might regard ‘$\perp $’ as an abbreviation for some canonical contradiction, such as ‘$A\wedge \mathrm{\neg}A$’. This will have the same effect as the above—obviously, ‘$A\wedge \mathrm{\neg}A$’ only ever has the truth value False—but it means that, officially, we do not need to add a new symbol to TFL.

3.
We might regard ‘$\perp $’, not as a symbol of TFL, but as something more like a punctuation mark that appears in our proofs. (It is on a par with the line numbers and the vertical lines, say.)
There is something very philosophically attractive about the third option, but here we will officially adopt the first. ‘$\perp $’ is to be read as a sentence letter that is always false. This means that we can manipulate it, in our proofs, just like any other sentence.
We still have to state a rule for negation introduction. The rule is very simple: if assuming something leads you to a contradiction, then the assumption must be wrong. This thought motivates the following rule:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$ 
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\perp $}$


close subproof,
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$

There can be as many lines between $i$ and $j$ as you like. To see this in practice, and interacting with negation, consider this proof:
Line number

Subproof level

Formula

Justification


$1$ 
0

$D$

AS

$2$ 
open subproof,
1

$\mathrm{\neg}D$

AS

$3$ 
1

$\perp $

$\mathrm{\neg}$E $2$, $1$

$4$ 
close subproof,
0

$\mathrm{\neg}\mathrm{\neg}D$

$\mathrm{\neg}$I $2$–$3$

If the assumption that $\mathcal{A}$ is true leads to a contradiction, $\mathcal{A}$ cannot be true, i.e., it must be false, i.e., $\mathrm{\neg}\mathcal{A}$ must be true. Of course, if the assumption that $\mathcal{A}$ is false (i.e., the assumption that $\mathrm{\neg}\mathcal{A}$ is true) leads to a contradiction, then $\mathcal{A}$ cannot be false, i.e., $\mathcal{A}$ must be true. So we can consider the following rule:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$ 
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\perp $}$


close subproof,
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

IP $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$

This rule is called indirect proof, since it allows us to prove $\mathcal{A}$ indirectly, by assuming its negation. Formally, the rule is very similar to $\mathrm{\neg}$I, but $\mathcal{A}$ and $\mathrm{\neg}\mathcal{A}$ have changed places. Since $\mathrm{\neg}\mathcal{A}$ is not the conclusion of the rule, we are not introducing $\mathrm{\neg}$, so IP is not a rule that introduces any connective. It also doesn’t eliminate a connective, since it has no freestanding premises which contain $\mathrm{\neg}$, only a subproof with an assumption of the form $\mathrm{\neg}\mathcal{A}$. By contrast, $\mathrm{\neg}$E does have a premise of the form $\mathrm{\neg}\mathcal{A}$: that’s why $\mathrm{\neg}$E eliminates $\mathrm{\neg}$, but IP does not.^{1}^{1} 1 There are logicians who have qualms about IP, but not about $\mathrm{\neg}$E. They are called “intuitionists.” Intuitionists don’t buy our basic assumption that every sentence has one of two truth values, true or false. They also think that $\mathrm{\neg}$ works differently—for them, a proof of $\perp $ from $\mathcal{A}$ guarantees $\mathrm{\neg}\mathcal{A}$, but a proof of $\perp $ from $\mathrm{\neg}\mathcal{A}$ does not guarantee that $\mathcal{A}$, but only $\mathrm{\neg}\mathrm{\neg}\mathcal{A}$. So, for them, $\mathcal{A}$ and $\mathrm{\neg}\mathrm{\neg}\mathcal{A}$ are not equivalent.
Using $\mathrm{\neg}$I, we were able to give a proof of $\mathrm{\neg}\mathrm{\neg}\mathcal{D}$ from $\mathcal{D}$. Using IP, we can go the other direction (with essentially the same proof).
Line number

Subproof level

Formula

Justification


$1$ 
0

$\mathrm{\neg}\mathrm{\neg}D$

PR

$2$ 
open subproof,
1

$\mathrm{\neg}D$

AS

$3$ 
1

$\perp $

$\mathrm{\neg}$E $1$, $2$

$4$ 
close subproof,
0

$D$

IP $2$–$3$

We need one last rule. It is a kind of elimination rule for ‘$\perp $’, and known as explosion.^{2}^{2} 2 The Latin name for this principle is ex contradictione quodlibet, “from contradiction, anything.” If we obtain a contradiction, symbolized by ‘$\perp $’, then we can infer whatever we like. How can this be motivated, as a rule of argumentation? Well, consider the English rhetorical device ‘…and if that’s true, I’ll eat my hat’. Since contradictions simply cannot be true, if one is true then not only will I eat my hat, I’ll have it too. Here is the formal rule:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\perp $}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$

X $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

Note that $\mathcal{A}$ can be any sentence whatsoever.
The explosion rule is a bit odd. It looks like $\mathcal{A}$ arrives in our proof like a bunny out of a hat. When trying to find proofs, it is very tempting to try to use it everywhere, since it seems so powerful. Resist this temptation: you can only apply it when you already have $\perp $! And you get $\perp $ only when your assumptions are contradictory.
Still, isn’t it odd that from a contradiction anything whatsoever should follow? Not according to our notion of entailment and validity. For $\mathcal{A}$ entails $\mathcal{B}$ iff there is no valuation of the sentence letters which makes $\mathcal{A}$ true and $\mathcal{B}$ false at the same time. Now $\perp $ is a contradiction—it is never true, whatever the valuation of the sentence letters. Since there is no valuation which makes $\perp $ true, there of course is also no valuation that makes $\perp $ true and $\mathcal{B}$ false! So according to our definition of entailment, $\perp \models \mathcal{B}$, whatever $\mathcal{B}$ is. A contradiction entails anything.^{3}^{3} 3 There are some logicians who don’t buy this. They think that if $\mathcal{A}$ entails $\mathcal{B}$, there must be some relevant connection between $\mathcal{A}$ and $\mathcal{B}$—and there isn’t one between $\perp $ and some arbitrary sentence $\mathcal{B}$. So these logicians develop other, “relevant” logics in which you aren’t allowed the explosion rule.
These are all of the basic rules for the proof system for TFL.
Practice exercises
A. The following two ‘proofs’ are incorrect. Explain the mistakes they make.
Line number

Subproof level

Formula

Justification


$1$ 
0

$(\mathrm{\neg}L\wedge A)\vee L$

PR

$2$ 
open subproof,
1

$\mathrm{\neg}L\wedge A$

AS

$3$ 
1

$\mathrm{\neg}L$

$\wedge $E $3$

$4$ 
1

$A$

$\wedge $E $1$

$5$ 
close subproof,
open subproof,
1

$L$

AS

$6$ 
1

$\perp $

$\mathrm{\neg}$E $3$, $5$

$7$ 
1

$A$

X $6$

$8$ 
close subproof,
0

$A$

$\vee $E $1$, $2$–$4$, $5$–$7$

Line number

Subproof level

Formula

Justification


$1$ 
0

$A\wedge (B\wedge C)$

PR

$2$ 
0

$(B\vee C)\to D$

PR

$3$ 
0

$B$

$\wedge $E $1$

$4$ 
0

$B\vee C$

$\vee $I $3$

$5$ 
0

$D$

$\to $E $4$, $2$

B. The following three proofs are missing their citations (rule and line numbers). Add them, to turn them into bona fide proofs. Additionally, write down the argument that corresponds to each proof.
Line number

Subproof level

Formula

Justification


$1$ 
0

$P\wedge S$


$2$ 
0

$S\to R$


$3$ 
0

$P$


$4$ 
0

$S$


$5$ 
0

$R$


$6$ 
0

$R\vee E$


Line number

Subproof level

Formula

Justification


$1$ 
0

$A\to D$


$2$ 
open subproof,
1

$A\wedge B$


$3$ 
1

$A$


$4$ 
1

$D$


$5$ 
1

$D\vee E$


$6$ 
close subproof,
0

$(A\wedge B)\to (D\vee E)$


Line number

Subproof level

Formula

Justification


$1$ 
0

$\mathrm{\neg}L\to (J\vee L)$


$2$ 
0

$\mathrm{\neg}L$


$3$ 
0

$J\vee L$


$4$ 
open subproof,
1

$J$


$5$ 
1

$J\wedge J$


$6$ 
1

$J$


$7$ 
close subproof,
open subproof,
1

$L$


$8$ 
1

$\perp $


$9$ 
1

$J$


$10$ 
close subproof,
0

$J$


C. Give a proof for each of the following arguments:

1.
$J\to \mathrm{\neg}J\therefore \mathrm{\neg}J$

2.
$Q\to (Q\wedge \mathrm{\neg}Q)\therefore \mathrm{\neg}Q$

3.
$A\to (B\to C)\therefore (A\wedge B)\to C$

4.
$K\wedge L\therefore K\leftrightarrow L$

5.
$(C\wedge D)\vee E\therefore E\vee D$

6.
$A\leftrightarrow B,B\leftrightarrow C\therefore A\leftrightarrow C$

7.
$\mathrm{\neg}F\to G,F\to H\therefore G\vee H$

8.
$(Z\wedge K)\vee (K\wedge M),K\to D\therefore D$

9.
$P\wedge (Q\vee R),P\to \mathrm{\neg}R\therefore Q\vee E$

10.
$S\leftrightarrow T\therefore S\leftrightarrow (T\vee S)$

11.
$\mathrm{\neg}(P\to Q)\therefore \mathrm{\neg}Q$

12.
$\mathrm{\neg}(P\to Q)\therefore P$