Natural Deduction Proofs in SL

This chapter introduces a dierent proof system in SL, separate from the tree method. The tree method has advantages and disadvantages. One advantage of trees is that, for the most part, they can be produced in a purely mechanical way---one need rely only on a rigorous application of a well-defined procedure; no 'flash of insight' is necessary. Another advantage is that, when a tree remains open, the tree method gives us a recipe for constructing an interpretation that satisfies the root. One disadvantage is that they do not always emphasize in an intuitive way why a conclusion follows from a set of premises; they show that something must be the case, on pain of contradiction, but they don’t always demonstrate, in a way closely connected to natural reasoning, why some things follow from other things.

The natural deduction system of this chapter will differ from the tree method in all of these respects. It is intended to model human reasoning in a closer way, illustrating the connections between various claims; consequently, working through a natural deduction proof requires a bit more insight and inspiration than a tree proof does.

Natural deduction proofs can be used to prove that an argument is valid; if an argument is invalid, our natural deduction system will not necessarily make that obvious. We won't have the equivalent to a completed open tree --- a proof of invalidity. It will turn out that there is a natural deduction derivation corresponding to every valid argument in SL --- i.e., like the tree method, this method is complete. (It is also sound.) But we won't offer a way to prove that there is no proof, and so natural deduction can't be used by itself to prove invalidity.

7.1 Natural Deduction: the basic idea

The general idea of a natural deduction proof is simple. You begin by writing down the premises you're beginning with, each on its own numbered line. Then you add a new numbered line, adding sentences that you can demonstrate to follow logically from what you have already written. (A formal list of rules gives the legal options for how to develop the proof.) If, following the rules, you manage to derive the conclusion from the premises, then you've shown that the argument form from those premises to that conclusion is valid.

Formally, a proof is a numbered sequence of sentences. The first sentences of the sequence are assumptions; these are the premises of the argument. Every sentence later in the sequence is derived from earlier sentences by one of the rules of proof. The final sentence of the sequence is the conclusion of the argument.

Consider these two SL argument forms (Modus Ponens and Disjunctive Syllogism):

Both are valid; you could confirm this with a four-line truth table. Either would demonstrate that there is no interpretation satisfying both premises, while falsifying the conclusion. The truth table method does not distinguish between these argument forms; it simply shows that they are both valid. There is, however, an interesting and important difference between these two argument forms, gestured at by their labels. The first argument, Modus Ponens, has a distinctive syntactic form: its premises are a conditional and the antecedent of that conditional, and the conclusion is the consequent; the second has a different form.

The natural deduction method is based in the recognition of particular kinds of valid forms. They also correspond reasonably well to familiar forms of informal reasoning. If you know a conditional, and you also know its antecedent, it is easy to infer its consequent. (Imagine being sure that if I ate the chilli, I'll get sick, and also being sure that I ate the chilli. You will surely infer that I will get sick.) Modus ponens is the name of this kind of conditional reasoning, and there is a special rule for it in our natural deduction system.

7.2 Our first rule: Conditional Elimination (modus ponens)

Many different arguments demonstrate the modus ponens pattern; all of them are valid:

All of these arguments are similar in an important way to the modus ponens argument above, and different from the disjunctive syllogism one. But the truth table proof of the validity for each of these arguments will go the same way: it will simply produce a truth table, and show that there is no row where the premises are all true and the conclusion is false. The truth table method does not illuminate what the modus ponens inferences all have in common.

Another way of making this point is to observe that the method of truth tables does not clearly show why an argument is valid. If you were to do a 1024-line truth table for an argument that contains ten sentence letters, then you could check to see if there were any lines on which the premises were all true and the conclusion were false. If you did not see such a line, and you were sure that you made no mistakes in constructing the table, then you would know that the argument was valid. Yet you might not be able to say anything further about why this particular argument was a valid argument form.

The natural deduction system of this chapter will include an inference rule corresponding to modus ponens. Natural deduction proofs of these validities, then, will all share something important in common: they will use that inference rule. Here, in its formal presentation, is the rule:

As has been the case throughout this book, the Greek letters Φ and Ψ are variables that can represent any SL sentence. The m and n here are variables ranging over line numbers. What this rule says is that if you have a conditional Φ ⊃ Ψ on line m, and you also have Φ, the antecedent of that conditional, on line n, you can write the consequent Ψ on a new line.

The notation off to the right in the new line, ''⊃ E m, n,'' is the justification for the new line. ''⊃ E'' stands for ''Conditional Elimination,'' which is our official name for the modus ponens rule. (We call it an 'elimination' rule because it begins with a conditional statement, and ends up deriving a statement that is not a conditional.)

With this rule, we can prove that any of the modus ponens arguments mentioned above is valid. Here are proofs of two of them:

Notice that these two proofs share just the same structure. We start by listing the premises as lines 1 and 2. We include a horizontal line under those premises to indicate that subsequent lines will need to be derived via rules; so we apply the conditional elimination rule to get the conclusion. We justify that conclusion by citing Conditional Elimination, and lines 1 and 2.

One can produce more complicated proofs via the same rule. Let's prove that this SL argument form is valid:

A
A ⊃ B
B ⊃ C
C ⊃ (¬P≡(Q∨R))
¬P ≡ (Q∨R)

We begin by writing our four premises on numbered lines:

We also include the 'want' notation off to the right, indicating what conclusion we are attempting to establish. (This is not strictly required as part of our proof, but it is helpful in keeping things organized.) We will complete the proof when we derive ¬P ≡ (Q∨R) --- i.e., when, while following the rules for how proofs may be developed, we write that sentence down on its own line. We cannot use conditional elimination to get to that sentence directly from our premises. We do have, on line 4, a conditional with that sentence as a consequent, but we don't have C, the antecedent, on its own line. However, we can get there via two steps of our inference rule. From lines 1 and 2, we can get B, and then, from there and 3, we can get to C. Finally, a third instance of conditional elimination lets us derive the intended conclusion:

Here are three things to notice about this proof.

First, every line after the premises needs to include a justification, citing a rule and the applicable previous line numbers. (So far Conditional Elimination is our only rule, but we will learn more very soon.) You can only write a new line if you have a rule that shows how it follows from previous lines.

Second, once you have derived something from the premises, that new line is available to help justify future lines. Once we derive line 5, for example, we're able to use it with line 3 to derive line 6.

Third, the Conditional Elimination rule requires that you have a conditional and its antecedent; it doesn't matter what order they are listed in. (In other words, when the rule says you need to have a conditional on line m, and its antecedent on line n, it does not matter whether m < n.) It also does not matter whether they are on consecutive lines. They just have to be on some lines up above, before performing the rule. So it is fine, for instance, that in justifying line 5, we cite a conditional on line 2, and its antecedent on line 1.

7.3 Exact Matches

Conditional Elimination, as well as all of our other natural deduction rules, are syntactically defined. That is to say, the application of the rules depends on the exact shape of the SL sentences in question. Here, again, is the formal statement of the rule:

It says that any time one has, on one line, a sentence made up of some sentence Φ, followed by the '⊃' symbol, followed by some sentence Ψ, where one also has Φ on another line, one may derive Ψ. This is the only pattern of inference that this rule permits. Φ and Ψ can be any sentences of SL, but a line justified by Conditional Elimination must fit this pattern exactly. It is not enough that one can 'just see' that a given sentence follows via a similar pattern of inference.

For example, this is not a legal derivation in our system:

The Conditional Elimination rule requires that the new sentence derived be the consequent of the conditional cited. But in this example, B is not the consequent of P ⊃ (A&B) --- A&B is. It is true that B obviously follows from A&B, but the Conditional Elimination rule doesn't allow you to derive things just because they obviously follow. (Neither does any other rule in our formal system.) To derive B from these premises we'll need to use another rule. (In particular, we will want to use the Conjunction Elimination rule, given below.)

To check to make sure you are applying the rules correctly, one good heuristic is to think about whether you are relying on the rule itself, or on your intuitive understanding of the meanings of the symbols we use in SL. Your intuitive understanding is a good way to think about which rules to use, but to check to make sure you're using the rules properly, think about whether the rules' exact formulations could explain why it is permissible to extend the derivation in the exact way you're working with. Pretend, for instance, that you have no idea what the `\supset' symbol means, but you know only that if you have two sentences joined by it on one line, and the first of those two sentences on another line, then you are allowed to copy down the second sentence exactly on a new line. This --- and no more --- is what the Conditional Elimination rule permits you to do. (This is what we mean when we say the rule is syntactically defined.)

7.4 Our Second Rule: modus tollens

Here is another rule one can use with conditionals:

If you have a conditional on one numbered line, and the negation of its consequent on another line, you may derive the negation of its antecedent on a new line. We abbreviate the justification for this rule as 'MT' for modus tollens. If you know that if she found the treasure, she is happy, and you also know that she isn't happy, then you can very sensibly infer that she didn't find the treasure.

You may notice an asymmetry between the labels we use for modus ponens and modus tollens: in the former case, we use Conditional Elimination (⊃ E) as its official name, but in the latter case, we call the rule Modus Tollens (MT). We'll explain in more detail why we use the labels in this way when we discuss 'basic' and 'derived' rules in Section 7.8 below. For now, the important thing is to understand how to use the rule.

Here is an example employing Modus Tollens several times over. We will derive ¬A from {A ⊃ B, B ⊃ C, C ⊃ D, ¬D}:

At each of lines 5--7, we cite a conditional and the negation of its consequent to infer the negation of its antecedent.

7.5 Disjunction Elimination

Recall this argument form from the Introduction:

We noted above that this is a different argument form from one that uses modus ponens; instead, it uses a kind of derivation that is specific to disjunction. From a disjunction like P ∨ Q alone, you can't conclude either disjunct, but you can conclude that at least one of the two disjuncts is true. So if you have also established that one of the disjuncts is false --- i.e., its negation is true --- then you can conclude the other disjunct, as in the argument above.

This inference form is sometimes called 'Disjunctive Syllogism'. In our system, it will be our official Disjunction Elimination (∨E) rule. If you have a disjunction and also the negation of one of its disjuncts, you may conclude the other disjunct.

We represent two different inference patterns here, because the rule allows you to conclude either disjunct from the negation of the other. If we'd only listed the left version of the rule above, then  ∨ E would've only permited one to conclude the first disjunct from the negation of the second one, along with the disjunction. Our rule lets us work with either disjunction. (If you want to be very fussy about it, you could think of these as two different rules with a strong conceptual similarity that happen to have the same name.)

Now that we have several rules, we are in a position to see how they can interact to construct more interesting proofs. Consider for example this argument form:

The two premises match the requirements for Conditional Elimination (modus ponens). And once that is done, we will be in a position to use Disjunction Elimination to derive the desired conclusion:

Via Conditional Elimination, we can derive J ∨ L from lines 1 and 2. Then from J ∨ L and ¬L, we can derive J, by Disjunction Elimination.

In this example, unlike the others we've seen so far, we used the premise on line 2 twice --- notice that the 2 appears in the justification for both line 3 and line 4. There is no limit to how many times you can make use of a given line in a natural deduction proof; once something is established, you can make use of it as often as you like.

7.6 Conjunction Introduction

Here is another rule. It is our Conjunction Introduction rule, which we abbreviate '&I':

This rule says that if you have some sentence Φ, and you also have some sentence Ψ, you may derive their conjunction, (Φ & Ψ). It is called Conjunction Introduction because it derives a conjunction from sentences that are not conjunctions.

Recall again that it is not a requirement either conjunct be an atom, or that m and n be consecutive lines, or that they appear in the order listed here. We require only that each line has been established somewhere above in the proof. If you have K on line 15 and L on line 8, you can prove (K & L) at some later point in the proof with the justification '&I 8, 15.'

7.7 Conjunction Elimination

We have just seen that Conjunction Introduction allows you derive a conjunction from a non-conjunction; Conjunction Elimination lets you do the converse. From a conjunction, you may derive either of its conjuncts. From (A & (P∨Q)), for instance, you may derive A, or you may derive (P∨Q). (Or you could even apply Conjunction Elimination twice and derive both.)

Because it lets you work on either conjunct, we formalize it twice over, much as we did with Disjunction Elimination. This will be our Conjunction Elimination rule, which we abbreviate '&E':

The &E rule requires only one sentence, so we write one line number as the justification for applying it.

Here is an example illustrating our two conjunction rules working together. Consider this argument.

[(A∨B)⊃(C∨D)] & [(E∨F)⊃(G∨H)]
[(E∨F)⊃(G∨H)] & [(A∨B)⊃(C∨D)]

The main logical operator in both the premise and conclusion is conjunction. Since conjunction is symmetric, the argument is obviously valid. In order to provide a proof, we begin by writing down the premise. After the premises, we draw a horizontal line --- everything below this line must be justified by a rule of proof. So the beginning of the proof looks like this:

From the premise, we can get each of the conjuncts by &E. The proof now looks like this:

The rule &I requires that we have each of the conjuncts available somewhere in the proof. They can be separated from one another, and they can appear in any order. So by applying the &I rule to lines 3 and 2, we arrive at the desired conclusion. The finished proof looks like this:

This proof may not look terribly interesting or surprising, but it shows how we can use rules of proof together to demonstrate the validity of an argument form. Note also that using a truth table to show that this argument is valid would have required a staggering 256 lines, since there are eight sentence letters in the argument. A proof via trees would be less unwieldy than that, but it would be less simple and elegant than this one. (Constructing such a proof would be a good exercise for tree review.)

7.8 Basic and derived rules

We have so far introduced five rules: Conditional Elimination, modus tollens, Disjunction Elimination, Conjunction Elimination, and Conjunction Introduction. There are still more rules still to learn, but it is helpful first to pause and draw a distinction between different kinds of rules.

Many of our rules, we have seen, carry the name 'Elimination' or 'Introduction', along with the name of one of our SL connectives. In fact, every rule except modus tollens has had such a name. Such rules are the basic rules in our natural deduction system. The basic rules comprise an Introduction and an Elimination rule for each connective, plus one more rule. Modus tollens is not a basic rule; we will call it a derived rule.

A derived rule is a non-basic rule whose validity we can derive using basic rules only. A useful fact about our natural deduction system is that the basic rules themselves are enough to derive every SL validity. Derived rules are helpful for making some proofs shorter or more intuitive, but one could prove anything provable without them.

We have already seen the Introduction and Elimination rules for conjunction, and the elimination rules for disjunction and conditionals. In the next several sections, we'll finish canvassing the basic rules, then say a bit more about modus tollens and other derived rules.

7.9 The remaining basic rules

7.9.1 Disjunction Introduction

If M is true, then M ∨ N must also be true. In general, the Disjunction Introduction rule (∨I) allows us to derive a disjunction if we already have one of its two disjuncts:

One can introduce a disjunct in either position --- it can be the first disjunct or the second disjunct. Accordingly, both options are listed here. (One is not required to do both; you can just take whichever version you find most helpful.)

As always, Ψ can be any sentence whatsoever. So the following is a legitimate proof:

It may seem odd that just by knowing M we can derive a conclusion that includes sentences like A, B, and the rest --- sentences that have nothing to do with M. Yet the conclusion follows immediately by ∨I. This is as it should be: The truth conditions for the disjunction mean that, if Φ is true, then Φ ∨ Ψ is true regardless of what Ψ is. So the conclusion could not be false if the premise were true; the argument form is valid.

7.9.2 Conditional Introduction

Consider this argument:

R ∨ F
¬R ⊃ F

The argument form seems like it should be valid. (You can confirm this by examining the truth tables.) The Conditional Introduction rule can demonstrate that this is so.

We begin the proof by writing down the premise of the argument, making a note of our intended conclusion, and drawing a horizontal line, like this:

If we had ¬R as a further premise, we could derive F by the ∨E rule. But we do not have ¬R as a premise of this argument, nor can we derive it directly from the premise we do have --- so we cannot simply prove F. What we will do instead is start a subproof, a 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 an assumption for the subproof. This can be anything we want. Here, it will be helpful to assume ¬R. We want to show that, if we did assume that, we would be able to derive F. So we make a new assumption that ¬R, and give ourselves a note that we wish to derive F. Our proof now looks like this:

It is important to emphasize that we are not claiming to have proven ¬R from the premise on line 1. We do not need to write in any justification for the assumption line of a subproof. (The 'want' is a note to ourself, not a justification.) The new vertical line indicates that an assumption is being made. You can think of the subproof as posing the question: What could we show if ¬R were true? We are trying to show that we could derive F. And indeed, we can:

This has shown that if we had ¬R as a premise, then we could prove F. In effect, we have proven ¬R ⊃ F. So the conditional introduction rule (⊃I) will allow us to close the subproof and derive ¬R ⊃ F in the main proof. Our final proof looks like this:

The ⊃I lets us discharge the assumption we'd been making, ending that vertical line. During lines (2) and (3), we were assuming that R; by the time we get to line (4), we are no longer making that assumption.

Notice that the justification for applying the ⊃I rule is the entire subproof. That's why we justify it by reference to a range of lines, instead of a comma-separated list. Usually that will be more than just two lines.

It may seem as if the ability to assume anything at all in a subproof would lead to chaos: Does it allow you to prove any conclusion from any premises? The answer is no, it does not. Consider this proof:

Does this show that one can prove any arbitrary sentence Ψ from any arbitrary premise Φ? After all, we've written Ψ & Φ on a line of a proof that began with Φ, without violating any of the rules of our system. The reason this doesn't have that implication is the vertical line that still extends into line 3. That line indicates that the assumption made at line 2 is still in effect. When the vertical line for the subproof ends, the subproof is closed. In order to complete a proof, you must close all of the subproofs. The conclusion to be proved must not be 'blocked off' by a vertical line; it should be aligned with the premises.

In this example, there is no way to close the subproof and use the R rule again on line 4 to derive in the main proof. Once you close a subproof, you cannot refer back to individual lines inside it. One can only close a subproof via particular rules that allow you to do so; ⊃I is one such rule; &I does not close subproofs. One can't just close a subproof willy-nilly. Closing a subproof is called discharging the assumptions of that subproof. So we can put the point this way: You cannot complete a proof until you have discharged all of the assumptions other than the original premises of the argument.

Of course, it is legitimate to do this:

This should not seem so strange, though. The conclusion on line 4 really does follow from line 1. (Draw a truth table if you need convincing of this.)

Once an assumption has been discharged, any lines that have been shown to follow from that assumption --- i.e., those lines that the vertical line of that assumption continues through --- cannot be cited as justification on further lines. So this development of the proof above, for instance, is not permitted:

Once the assumption made at line 2 has been discharged at line 4, the lines within that assumption --- 2 and 3 --- are unavailable for further justification. So one cannot perform Disjunction Elimination on line 3 at line 5.

Put in its general form, the ⊃I rule looks like this:

When we introduce a subproof, we typically write what we want to derive off to the right. This is just so that we do not forget why we started the subproof if it goes on for five or ten lines. There is no 'want' rule. It is a note to ourselves, and not formally part of the proof.

Although it is always permissible to open a subproof with any assumption you please, there is some strategy involved in picking a useful assumption. Starting a subproof with a random assumption is a terrible strategy. It will just waste lines of the proof. In order to derive a conditional by the ⊃I rule, for instance, you must assume the antecedent of the conditional.

The ⊃I rule also requires that the consequent of the conditional be the last line of the subproof. It is always permissible to close a subproof and discharge its assumptions, but it will not be helpful to do so until you get what you want. This is an illustration of the observation made above, that unlike the tree method, the natural deduction method requires some strategy and thinking ahead.

Never make an assumption without a plan for how to discharge it.

Here is another example of an argument form whose validity we can prove using the conditional rules.

P ⊃ Q
Q ⊃ R
P ⊃ R

We begin the proof by writing the two premises as assumptions. Since the main logical operator in the conclusion is a conditional, we can expect to use the ⊃I rule. For that, we need a subproof --- so we write in the antecedent of the conditional as assumption of a subproof. We make a note that we are aiming for the consequent of that conditional:

We made P available by assuming it in a subproof, allowing us to use ⊃E on the first premise. This gives us Q, which allows us to use ⊃E on the second premise. Having derived R, we close the subproof. By assuming P we were able to prove R, so we apply the ⊃I rule and finish the proof.

7.9.3 Biconditional Introduction

Biconditionals indicate that the two sides have the same truth value. One establishes a biconditional by establishing each direction of it as conditionals. To derive $W \\equiv X$, for instance, you must establish both W ⊃ X and X ⊃ W. Those conditionals may occur in either order; they need not be on consecutive lines. (Compare the shape of the &I rule.) Schematically, the Biconditional Introduction rule works like this:

7.9.4 Biconditional Elimination

The biconditional elimination rule (≡ E) is a generalized version of modus ponens (⊃ E). If you have the left-hand subsentence of the biconditional, you can derive the right-hand subsentence. If you have the right-hand subsentence, you can derive the left-hand subsentence. This is the rule:

As in the case of Disjunction Elimination, we include both versions under the same name, so that you don't need to worry about whether the side you already have is the left-hand side of the biconditional or the right-hand side. Whichever side it is, you may derive the other via Biconditional Elimination.

7.9.5 Reductio and the negation rules

Here is a simple mathematical argument in English:

Assume there is some greatest natural number. Call it A.
That number plus one is also a natural number.
Obviously, A + 1 > A.
So there is a natural number greater than A.
This is impossible, since A is assumed to be the greatest natural number.
∴ There is no greatest natural number.

This argument form is traditionally called a reductio. Its full Latin name is reductio ad absurdum, which means 'reduction to absurdity.' In a reductio, we assume something for the sake of argument --- for example, that there is a greatest natural number. Then we show that the assumption leads to two contradictory sentences --- for example, that A is the greatest natural number and that it is not. In this way, we show that the original assumption must have been false.

The basic rules for negation will allow for arguments like this. Like the Conditional Introduction rule, our negation rules allow us to make new assumptions with no justification --- we draw a new vertical line, and a note to ourselves as to what we are trying to do. If we assume something and show that it leads to contradictory sentences, then we have proven the negation of the assumption. This is the negation introduction (¬ I) rule:

The ¬I rule discharges the assumption for reductio, concluding its negation, when it's shown that some sentence and its negation each follow from the assumption. It cites two (overlapping) ranges: a subproof from the assumption to some sentence Ψ, and a subproof from that same assumption to ¬Ψ. We write 'for reductio' to the right of the assumption, as a note to ourselves, a reminder of why we started the subproof. It is not formally part of the proof, but it is helpful for thinking clearly about the proof.

To see how the rule works, suppose we want to prove an instance of the law of non-contradiction: ¬(G & ¬G). We can prove this without any premises by immediately starting a subproof. We want to apply ¬I to the subproof, so we assume (G & ¬G). We then get an explicit contradiction by &E. The proof looks like this:

The ¬E rule will work in much the same way. If we assume ¬Φ and show that it leads to a sentence and its negation, we have effectively proven Φ. So the rule looks like this:

7.9.6 Reiteration

In addition to the Introduction and Elimination rules for each logical operator, we will also have one more basic rule: Reiteration (R). If you already have shown something in the course of a proof, the Reiteration rule allows you to repeat it on a new line. Put formally:

Obviously, the reiteration rule will not allow us to show anything new. For that, we will need to use rules. Still, Reiteration is a handy rule to have available. Here, for instance, is a proof using Reiteration to help with a Negation Introduction:

Negation Introduction requires that one show that some sentence and its negation are both derivable from the assumption for reductio. In this case, we establish that P and ¬P both follow from the assumption that Q. In the case of ¬P, we can get it directly via Conditional Elimination; the easiest way to get the P that we need is simply to reiterate it from line 1.

You may have noticed that there is another way to prove ¬Q from these premises --- one may do it in a single step via modus tollens. Recall that modus tollens is not one of our basic rules. It is a derived rule that lets us take certain shortcuts. But anything that can be proven with modus tollens can be proven with the basic rules listed above. In fact, the proof we have just seen, using Negation Introduction and Reiteration, provides a template. Anything you could get to with one step via modus tollens, you could also get to in four steps via Negation Introduction, Conditional Elimination, and Reiteration.

7.10 Derived Rules

A derived rule is a rule of proof that does not make any new proofs possible. Anything that can be proven with a derived rule can be proven without it. You can think of a short proof using a derived rule as shorthand for a longer proof that uses only the basic rules.

7.10.1 Modus tollens

We have been discussing modus tollens throughout this chapter, and in Section 7.9.6 we showed how, in the case of one simple proof using modus tollens, we can instead give a slightly longer proof using only basic rules. In fact, we can prove this much more generally, via this proof schema:

As always, Φ and Ψ are meta-variables. They are not symbols of SL, but stand-ins for arbitrary sentences of SL. So this is not, strictly speaking, a proof in SL. It is more like a recipe; no matter what sentences you want to use modus tollens on, if that rule would allow it, this pattern of proof will get you to the same place using basic rules only. This means that modus tollens is not really necessary; we could prove everything we want to prove without it.

Nevertheless, it is a convenient shortcut. We add it to our list of derived rules.

7.10.2 Dilemma

Here is the Dilemma rule:

It might not be immediately obvious that this is a valid inference rule, but if you think about it a minute, you may be able to see why it is a good rule. If you know that two conditionals are true, and they have the same consequent, and you also know that one of the two antecedents is true, then whichever of those two disjunct is true, will license a modus ponens inference to the conclusion.

For example, suppose you know all of the following:

If it is raining, the car is wet.
If it is snowing, the car is wet.
It is raining or it is snowing.

From these premises, you can definitely establish that the car is wet. This is the form that the Dilemma rule captures. We use the label 'dilemma' to convey the idea that, whichever way you pick, you'll be stuck with the same conclusion. (''You're damned if you do, and you're damned if you don't. You do or don't. Therefore you are damned.'')

The Dilemma rule is also derivable from the basic rules. The proof is a bit more complicated, but here it is in schematic form:

To understand this proof, think about the broad outline of it. Ultimately, we derive Ω via Negation Elimination; that's why we assumed ¬Ω on line 4, and worked our way to a contradiction on lines 12--13. The internal lines are subproofs to the intermediate conclusions Ψ and ¬Ψ.

So as in the case of modus tollens, Dilemma doesn't allow us to prove anything we couldn't prove via basic rules. Anytime you wanted to use the Dilemma rule, you could always take ten extra lines and prove the same thing in basic rules. But it's a useful shorthand to include on our list of derived rules.

7.10.3 Hypothetical Syllogism

We also add hypothetical syllogism (HS) as a derived rule.

We have already given a proof of one instance of Hypothetical Syllogism above, in Section 7.9.2. The general proof schema is just the same, but with that P, Q, and R replaced with Φ, Ψ, and Ω, respectively.

7.11 Rules of Replacement

Consider how you would prove this argument valid:

F ⊃ (G & H)
F ⊃ G

Perhaps it is tempting to write down the premise and apply the &E rule to the conjunction (G & H). This is impermissible, however, because the basic rules of proof can only be applied to whole sentences. In order to use &E, we need to get the conjunction (G & H) on a line by itself. Here is a proof:

The rules we have seen so far must apply to wffs that are on a proof line by themselves. We will now introduce some derived rules that may be applied to part of a sentence. These are called rules of replacement, because they can be used to replace part of a sentence with a logically equivalent expression. One simple rule of replacement is commutativity (abbreviated Comm), which says that we can swap the order of conjuncts in a conjunction or the order of disjuncts in a disjunction. We define the rule this way:

(Φ & Ψ) ⇔ (Ψ & Φ)
(Φ∨Ψ) ⇔ (Ψ∨Φ)
(Φ≡Ψ) ⇔ (Ψ≡Φ) Comm

The double arrow means that you can take a subformula on one side of the arrow and replace it with the subformula on the other side. The arrow is double-headed because rules of replacement work in both directions. And replacement rules --- unlike all the rules we've seen so far --- can be applied to wffs that are part of more complex sentences. They don't need to be on their own line.

Consider this argument:

(M∨P) ⊃ (P & M)
(P∨M) ⊃ (M & P)

It is possible to give a proof of this using only the basic rules, but it will be long and inconvenient. With the Comm rule, we can provide a proof easily:

(We need to apply the rule twice, because each application allows one transformation. We transformed the antecedent first, then the consequent. The opposite order would also have been fine.)

Another rule of replacement is Double Negation (DN). With the DN rule, you can remove or insert a pair of negations for any wff in a line, even if it isn't the whole line. This is the rule:

¬¬Φ ⇔ Φ DN

Two more replacement rules are called De Morgan's Laws, named for the 19th-century British logician August De Morgan. (Although De Morgan did formalize and publish these laws, many others discussed them before him.) The rules capture useful relations between negation, conjunction, and disjunction. Here are the rules, which we abbreviate DeM:

¬(Φ∨Ψ) ⇔ (¬Φ & ¬Ψ)
¬(Φ & Ψ) ⇔ (¬Φ∨¬Ψ) DeM

As we have seen, Φ ⊃ Ψ is equivalent to ¬Φ ∨ Ψ. A further replacement rule captures this equivalence. We abbreviate the rule MC, for 'material conditional.' It takes two forms:

(Φ⊃Ψ) ⇔ (¬Φ∨Ψ)
(Φ∨Ψ) ⇔ (¬Φ⊃Ψ) MC

Now consider this argument:

¬(P⊃Q),
∴ P & ¬Q

As always, we could prove this argument valid using only the basic rules. With rules of replacement, though, the proof is much simpler:

A final replacement rule captures the relation between conditionals and biconditionals. We will call this rule biconditional exchange and abbreviate it ≡ex.

[(Φ⊃Ψ) & (Ψ⊃Φ)] ⇔ (Φ≡Ψ)] ≡ ex

7.11 Proof Strategy

There is no simple recipe for proofs, and there is no substitute for practice. Here, though, are some rules of thumb and strategies to keep in mind.

Work backwards from what you want. The ultimate goal is to derive the conclusion. Look at the conclusion and ask what the introduction rule is for its main logical operator. This gives you an idea of what should happen just before the last line of the proof. Then you can treat this line as if it were your goal. Ask what you could do to derive this new goal.

For example: If your conclusion is a conditional Φ ⊃ Ψ, plan to use the ⊃I rule. This requires starting a subproof in which you assume Φ. In the subproof, you want to derive Ψ.

Work forwards from what you have. When you are starting a proof, look at the premises; later, look at the sentences that you have derived so far. Think about the elimination rules for the main operators of these sentences. These will tell you what your options are.

For example: If you have a conditional Φ ⊃ Ψ, and you also have Φ, ⊃E is a pretty natural choice.

For a short proof, you might be able to eliminate the premises and introduce the conclusion. A long proof is formally just a number of short proofs linked together, so you can fill the gap by alternately working back from the conclusion and forward from the premises.

Change what you are looking at. Replacement rules can often make your life easier. If a proof seems impossible, try out some different substitutions.

For example: It is often difficult to prove a disjunction using the basic rules. If you want to show Φ ∨ Ψ, it is often easier to show ¬Φ ⊃ Ψ and use the MC rule.

Some replacement rules should become second nature. If you see a negated disjunction, for instance, you should immediately think of DeMorgan's rule.

Do not forget indirect proof. If you cannot find a way to show something directly, try assuming its negation.

Remember that most proofs can be done either indirectly or directly. One way might be easier --- or perhaps one sparks your imagination more than the other --- but either one is formally legitimate.

Repeat as necessary. Once you have decided how you might be able to get to the conclusion, ask what you might be able to do with the premises. Then consider the target sentences again and ask how you might reach them.

Persist. Try different things. If one approach fails, then try something else.

7.12 Proof-theoretic Concepts

As we did in our discussion of trees, we will again use the symbol '⊢' to indicate provability. Provability is relative to a proof system, so the meaning of the '⊢' symbol featured in this chapter should be distinguished from the one we used for trees. When necessary, we can specify the single turnstile with reference to the proof system in question, letting '⊢_T' stand for provability in the tree system, and '⊢_ND' stand for provability in this natural deduction system. For the most part in this chapter, though, we'll be interested in natural deduction, so unless it is specified otherwise, you can understand '⊢' to mean '⊢_ND'.

The double turnstile symbol '⊨', remains unchanged. It stands for semantic entailment, as described in Chapter 4.

When we write {Φ₁, Φ₂, …}⊢_NDΨ, this means that it is possible to give a natural deduction proof of Ψ with Φ₁,Φ₂,… as premises. With just one premise, we leave out the curly braces, so Φ ⊢ Ψ means that there is a proof of Ψ with Φ as a premise. Naturally,  ⊢ Φ means that there is a proof of Φ that has no premises. You can think of it as shorthand for ∅ ⊢ Φ.

For notational completeness, we can understand χ ⊢ ⊥ to mean that from χ, we could prove an arbitrary contradiction. In other words, χ is an inconsistent set.

Logical proofs are sometimes called derivations. So Φ ⊢ Ψ can be read as 'Ψ is derivable from Φ.'

A theorem is a sentence that is derivable without any premises; i.e., Φ is a theorem if and only if  ⊢ Φ.

It is not too hard to show that something is a theorem --- you just have to give a proof of it. How could you show that something is not a theorem? If its negation is a theorem, then you could provide a proof. For example, it is easy to prove ¬(P & ¬P), which shows that (P & ¬P) cannot be a theorem. For a sentence that is neither a theorem nor the negation of a theorem, however, there is no easy way to show this. You would have to demonstrate not just that certain proof strategies fail, but that no proof is possible. Even if you fail in trying to prove a sentence in a thousand different ways, perhaps the proof is just too long and complex for you to make out. As we've emphasized already, this is a difference between our natural deduction system and the tree method.

Two sentences and are provably equivalent if and only if each can be derived from the other; i.e., Φ ⊢ Ψ and Ψ ⊢ Φ.

It is relatively easy to show that two sentences are provably equivalent --- it just requires a pair of proofs. Showing that sentences are not provably equivalent would be much harder. It would be just as hard as showing that a sentence is not a theorem. (In fact, these problems are interchangeable. Can you think of a sentence that would be a theorem if and only if Φ and Ψ were provably equivalent?)

The set of sentences {Φ₁, Φ₂, …} is provably inconsistent if and only if contradictory sentences are derivable from it; i.e., for some sentence Ψ, {Φ₁, Φ₂, …} ⊢ Ψ and {Φ₁, Φ₂, …} ⊢ ¬Ψ. This is equivalent to {Φ₁, Φ₂, …} ⊢ ⊥.

It is easy to show that a set is provably inconsistent: You just need to assume the sentences in the set and prove a contradiction. Showing that a set is not provably inconsistent will be much harder. It would require more than just providing a proof or two; it would require showing that proofs of a certain kind are impossible.

7.13 Proof-theoretic Concepts

As you might already suspect, there is a connection between theorems and tautologies.

There is a formal way of showing that a sentence is a theorem: Prove it. For each line, we can check to see if that line follows by the cited rule. It may be hard to produce a twenty line proof, but it is not so hard to check each line of the proof and confirm that it is legitimate --- and if each line of the proof individually is legitimate, then the whole proof is legitimate. Showing that a sentence is a tautology, though, requires reasoning in English about all possible models. There is no formal way of checking to see if the reasoning is sound. Given a choice between showing that a sentence is a theorem and showing that it is a tautology, it would be easier to show that it is a theorem.

By contrast, there is no formal way of showing that a sentence is not a theorem. We would need to reason in English about all possible proofs. Yet there is a formal method for showing that a sentence is not a tautology. We need only construct a model in which the sentence is false. Given a choice between showing that a sentence is not a theorem and showing that it is not a tautology, it would be easier to show that it is not a tautology.

Fortunately, a sentence is a theorem if and only if it is a tautology. If we provide a proof of  ⊢ Φ and thus show that it is a theorem, it follows that Φ is a tautology; i.e.,  ⊨ Φ. Similarly, if we construct a model in which Φ is false and thus show that it is not a tautology, it follows that Φ is not a theorem.

In general, Φ ⊢ Ψ if and only if Φ ⊨ Ψ. As such:

• An argument is valid if and only if the conclusion is derivable from the premises.

• Two sentences are logically equivalent if and only if they are provably equivalent.

• A set of sentences is consistent if and only if it is not provably inconsistent.

You can pick and choose when to think in terms of proofs and when to think in terms of models, doing whichever is easier for a given task. Table 7.1 summarizes when it is best to give proofs and when it is best to give models.

In this way, proofs and models give us a versatile toolkit for working with arguments. If we can translate an argument into SL, then we can measure its logical weight in a purely formal way. If it is deductively valid, we can give a formal proof; if it is invalid, we can provide a formal counterexample.

7.14 Soundness and Completeness

Chapter 6 considered the soundness and completeness of the tree method at length; it proved that this method was both sound (χ⊢_TΦ only if χ ⊨ Φ) and complete (χ ⊨ Φ only if χ⊢_TΦ). The natural deduction system of this chapter is also both sound and complete for SL. In other words, χ⊢_NDΦ if and only if χ ⊨ Φ. Given the soundness and completeness of the tree method, this also means that our two proof systems are equivalent in the sense that anything provable in one is also provable in the other (χ⊢_TΦ) iff (χ⊢_NDΦ).

How can we know that our natural deduction method is sound? A proof system is sound if there are no derivations corresponding to invalid arguments. Demonstrating that the proof system is sound would require showing that any possible proof in our system is the proof of a valid argument. There is a fairly simple way of approaching this in a step-wise fashion. If using the &E rule on the last line of a proof could never change a valid argument into an invalid one, then using the rule many times could not make an argument invalid. Similarly, if using the &E and  ∨ E rules individually on the last line of a proof could never change a valid argument into an invalid one, then using them in combination could not either.

The strategy is to show for every rule of inference that it alone could not make a valid argument into an invalid one. It follows that the rules used in combination would not make a valid argument invalid. Since a proof is just a series of lines, each justified by a rule of inference, this would show that every provable argument is valid.

Consider, for example, the I rule. Suppose we use it to add to a valid argument. In order for the rule to apply, and must already be available in the proof. Since the argument so far is valid, and are either premises of the argument or valid consequences of the premises. As such, any model in which the premises are true must be a model in which and are true. According to the definition of , this means that is also true in such a model. Therefore, validly follows from the premises. This means that using the I rule to extend a valid proof produces another valid proof.

In order to show that the proof system is sound, we would need to show this for the other inference rules. Since the derived rules are consequences of the basic rules, it would suffice to provide similar arguments for the 16 other basic rules. The reasoning is extremely similar to that given in the soundness proof for trees in the previous chapter. We will not go through it in detail here.

Given a proof that the proof system is sound, it follows that every theorem is a tautology.

What of completeness? Why think that every valid argument is an argument that can be proven in our natural deduction system? That is, why think that Φ ⊨ Ψ implies Φ ⊢ Ψ? Our system is also complete, but the completeness proof for natural deduction is a bit more complex than the completeness proof for trees. (In the case of trees, we had a mechanical method that was guaranteed to find proofs if they exist; we have seen no such method here, which makes proving these general results harder.) This proof is beyond the scope of this book.

The important point is that, happily, the proof system for SL is both sound and complete. Consequently, we may freely use this natural deduction method to draw conclusions about models in SL.

Summary of definitions

• A sentence is a theorem if and only if  ⊢ Φ.

• Two sentences Φ and Ψ are provably equivalent if and only if Φ ⊢ Ψ and Ψ ⊢ Φ.

• {Φ₁, Φ₂, …} is provably inconsistent if and only if, for some sentence Ψ, {Φ₁, Φ₂, …} ⊢ (Ψ&¬Ψ).

Practice Exercises

Here is a set of instructions about how to use the natural deduction proof construction/checking tool.

Also, if you click here, you can find a slightly more user-friendly version (including real-time rendering of your proofs) of the below exercises.

Part A Provide a justification (rule and line numbers) for each line of proof that requires one.

Part B Give a proof for each argument in SL.

Part C Give a proof for each argument in SL.

Part D Show that each of the following sentences is a theorem in SL.

Part E Show that each of the following pairs of sentences are provably equivalent in SL.

Part F Provide proofs for each of the following

Part G For the following, provide proofs using only the basic rules. The proofs will be longer than proofs of the same claims would be using the derived rules.

1. Show that MT is a legitimate derived rule. Using only the basic rules, prove the following: Φ ⊃ Ψ, ¬Ψ, ∴ ¬Φ.
2. Show that Comm is a legitimate rule for the biconditional. Using only the basic rules, prove that Φ ≡ Ψ and Ψ ≡ Φ are equivalent.
3. Using only the basic rules, prove the following instance of DeMorgan’s Laws: (¬A & ¬B), ∴ ¬(A∨B).
4. Show that ≡ex is a legitimate derived rule. Using only the basic rules, prove that D ≡ E and (D⊃E) & (E⊃D) are equivalent.

Part H

1. If you know that Φ ⊢ Ψ, what can you say about (Φ&Ω) ⊢ Ψ? Explain your answer.
2. If you know that Φ ⊢ Ψ, what can you say about (Φ∨Ω) ⊢ Ψ? Explain your answer.