chapter7.pandoc

---
base-css:
- https://static.carnap.io/css/tufte.css
- https://static.carnap.io/css/tuftextra.css
---
---
css:
- https://carnap.philosophy.ubc.ca/shared/dave/prettyproofUBC.css
---

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*):



<div class="side-by-side">
<div>
Modus Ponens

```{.PrettyProof}
P \supset Q
P
Q
```
</div>

<div>
Disjunctive Syll.

```{.PrettyProof}
P \vee Q
\neg P
Q
```
</div>
</div>

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:


<div class="side-by-side">
<div>
```{.PrettyProof}
P \supset \neg Q
P
\neg Q
```
</div>

<div>
```{.PrettyProof}
\neg P \supset (A \equiv B))
\neg P
\neg (A \equiv B))
```
</div>
</div>

<div>
```{.PrettyProof}
P \vee Q \supset A
P \vee Q
\neg A
```
</div>

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:



<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi \supset \Psi$</div>
    <div>$\Phi$</div>
    <div>$\Psi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\supset$E m,n</div>
  </div>
</div>

As has been the case throughout this book, the Greek letters $\Phi$ and $\Psi$ 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 $\Phi \supset \Psi$ on line $m$, and you also have $\Phi$, the antecedent of that conditional, on line $n$, you can write the consequent $\Psi$ on a new line.

The notation off to the right in the new line, ''$\supset$ E $m, n$,'' is the justification for the new line. ''$\supset$ 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:

<div class="side-by-side">
<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$P \supset \neg Q$</div>
    <div class="last-premise">$P$</div>
    <div>$\neg Q$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\supset$E 1,2</div>
  </div>
</div>

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$(P \lor Q) \supset A$</div>
    <div class="last-premise">$P \lor Q$</div>
    <div>$A$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\supset$E 1,2</div>
  </div>
</div>
</div>




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:


> | <span class="premise"> $A$</span>
> | <span class="premise"> $A \supset B$</span>
> | <span class="premise"> $B \supset C$</span>
> | <span class="premise"> $C \supset (\neg P \equiv (Q \lor R))$</span>
> | <span class="conclusion"> $\neg P \equiv (Q \lor R)$</span>

We begin by writing our four premises on numbered lines:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div>$A$</div>
    <div>$A \supset B$</div>
    <div>$B \supset C$</div>
    <div class="last-premise">$C \supset (\neg P \equiv (Q \lor R))$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>want $\neg P \equiv (Q \lor R)$</div>
  </div>
</div>

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 $\neg P \equiv (Q \lor 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:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
    <div>6</div>
    <div>7</div>
  </div>
  <div class="proof">
    <div>$A$</div>
    <div>$A \supset B$</div>
    <div>$B \supset C$</div>
    <div class="last-premise">$C \supset (\neg P \equiv (Q \lor R))$</div>
    <div>$B$</div>
    <div>$C$</div>
    <div>$\neg P \equiv (Q \lor R)$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>want $\neg P \equiv (Q \lor R)$</div>
    <div> $\supset$E 1, 2</div>
    <div> $\supset$E 3, 5</div>
    <div> $\supset$E 4, 6</div>
  </div>
</div>


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:

<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi \supset \Psi$</div>
    <div>$\Phi$</div>
    <div>$\Psi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\supset$E m,n</div>
  </div>
</div>

It says that any time one has, on one line, a sentence made up of some sentence $\Phi$, followed by the '$\supset$' symbol, followed by some sentence $\Psi$, where one also has $\Phi$ on another line, one may derive $\Psi$. This is the only pattern of inference that this rule permits. $\Phi$ and $\Psi$ 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:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
  </div>
  <div class="proof">
    <div>$P \supset (A\ \&\ B)$</div>
    <div class="last-premise">$P$</div>
    <div>$B$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\supset$E 1,2</div>
  </div>
</div>


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\supset (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:



<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi \supset \Psi$</div>
    <div>$\neg \Psi$</div>
    <div>$\neg \Phi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>MT m,n</div>
  </div>
</div>


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 ($\supset$ 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 $\neg A$ from $\{A \supset B, B \supset C, C \supset D, \neg D\}$:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
    <div>6</div>
    <div>7</div>
  </div>
  <div class="proof">
    <div>$A \supset B$</div>
    <div>$B \supset C$</div>
    <div>$C \supset D$</div>
    <div class="last-premise">$\neg D$</div>
    <div>$\neg C$</div>
    <div>$\neg B$</div>
    <div>$\neg A$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>want $\neg A$</div>
    <div> MT 3, 4</div>
    <div> MT 2, 5</div>
    <div> MT 1, 6</div>
  </div>
</div>

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:


<div>
```{.PrettyProof}
P \vee Q
\neg P
Q
```
</div>


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 \lor 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 ($\lor$E) rule. If you have a disjunction and also the negation of one of its disjuncts, you may conclude the other disjunct.


<div class="side-by-side">
  <div class="tri-proof">
    <div class="num">
      <div>m</div>
      <div>n</div>
      <div>&nbsp;</div>
    </div>
    <div class="proof">
      <div>$\Phi \vee \Psi$</div>
      <div>$\neg \Psi$</div>
      <div>$\Phi$</div>
    </div>
    <div class="justification">
      <div>&nbsp;</div>
      <div>&nbsp;</div>
      <div>$\vee$E m,n</div>
    </div>
  </div>
  <div class="tri-proof">
    <div class="num">
      <div>m</div>
      <div>n</div>
      <div>&nbsp;</div>
    </div>
    <div class="proof">
      <div>$\Phi \vee \Psi$</div>
      <div>$\neg \Phi$</div>
      <div>$\Psi$</div>
    </div>
    <div class="justification">
      <div>&nbsp;</div>
      <div>&nbsp;</div>
      <div>$\vee$E m,n</div>
    </div>
  </div>
</div>

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 $\vee 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:



<div>
```{.PrettyProof}
\neg L \supset (J \vee L)
\neg L
J
```
</div>

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:



<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div>$\neg L \supset (J \lor L)$</div>
    <div class="last-premise">$\neg L$</div>
    <div>$J \lor L$</div>
    <div>$J$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>want $J$</div>
    <div>$\supset$E 1, 2;</div>
    <div>$\lor$E 2, 3</div>
  </div>
</div>


Via Conditional Elimination, we can derive $J \lor L$ from lines 1 and 2. Then from $J \lor L$ and $\neg 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':


<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi$</div>
    <div>$\Psi$</div>
    <div>$\Phi$ & $\Psi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&I m,n</div>
  </div>
</div>

This rule says that if you have some sentence $\Phi$, and you also have some sentence $\Psi$, you may derive their conjunction, $(\Phi\ \&\ \Psi)$. 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 \lor Q))$, for instance, you may derive $A$, or you may derive $(P \lor 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':


<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi$ & $\Psi$</div>
    <div>$\Phi$</div>
    <div>$\Psi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&E m</div>
    <div>&E m</div>
  </div>
</div>


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.


```{.PrettyProof}
[(A \vee B) \supset (C \vee D)] & [(E \vee F) \supset (G\vee H)]
[(E \vee F) \supset (G \vee H)] & [(A \vee B)\supset (C\vee 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:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
  </div>
  <div class="proof">
    <div class="last-premise">$[(A \vee B) \supset (C \vee D)]$ & $[(E \vee F) \supset (G\vee H)]$</div>
  </div>
</div>

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

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
  </div>
  <div class="proof">
    <div class="last-premise">$[(A \vee B) \supset (C \vee D)]$ & $[(E \vee F) \supset (G\vee H)]$</div>
    <div>$[(A \vee B) \supset (C \vee D)]$</div>
    <div>$[(E \vee F) \supset (G\vee H)]$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&E 1</div>
    <div>&E 1</div>
  </div>
</div>

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:



<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div class="last-premise">$[(A \vee B) \supset (C \vee D)]$ & $[(E \vee F) \supset (G\vee H)]$</div>
    <div>$[(A \vee B) \supset (C \vee D)]$</div>
    <div>$[(E \vee F) \supset (G\vee H)]$</div>
    <div>$[(E \vee F) \supset (G\vee H)]$ & $[(A \vee B) \supset (C \vee D)]$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&E 1</div>
    <div>&E 1</div>
    <div>&I 2,3</div>
  </div>
</div>

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 \lor N$ must also be true. In general, the Disjunction Introduction rule ($\lor$I) allows us to derive a disjunction if we already have one of its two disjuncts:


<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi$</div>
    <div>$\Phi \vee \Psi$</div>
    <div>$\Psi \vee \Phi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>$\vee$I m</div>
    <div>$\vee$I m</div>
  </div>
</div>


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, $\Psi$ can be *any* sentence whatsoever. So the following is a legitimate proof:



<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
  </div>
  <div class="proof">
    <div class="last-premise">$M$</div>
    <div>$M \vee ([(A \equiv B) \supset (C$ & $D)] \equiv [E$ & $F])$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>$\vee$I 1</div>
  </div>
</div>


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 $\lor$I. This is as it should be: The truth conditions for the disjunction mean that, if $\Phi$ is true, then $\Phi \lor \Psi$ is true regardless of what $\Psi$ 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:

```{.PrettyProof}
R \vee F
\neg R \supset 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:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
  </div>
  <div class="proof">
    <div class="last-premise">$R \vee F$</div>
  </div>
  <div class="justification">
    <div>want $\neg R \supset F$</div>
  </div>
</div>


If we had $\neg R$ as a further premise, we could derive $F$ by the $\lor$E rule. But we do not have $\neg 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 $\neg 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 $\neg R$, and give ourselves a note that we wish to derive $F$. Our proof now looks like this:



<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
  </div>
  <div class="proof">
    <div class="last-premise">$R \vee F$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\neg R$</div>
      </div>
    </div>
  </div>
  <div class="justification">
    <div>want $\neg R \supset F$</div>
    <div>want $F$</div>
  </div>
</div>



It is important to emphasize that we are not claiming to have proven $\neg 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* $\neg R$ were true? We are trying to show that we could derive $F$. And indeed, we can:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
  </div>
  <div class="proof">
    <div class="last-premise">$R \vee F$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\neg R$</div>
        <div>F</div>
      </div>
    </div>
  </div>
  <div class="justification">
    <div>want $\neg R \supset F$</div>
    <div>want $F$</div>
    <div>$\vee$E 1,2</div>
  </div>
</div>



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

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div class="last-premise">$R \vee F$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\neg R$</div>
        <div>F</div>
      </div>
    </div>
    <div>$\neg R \supset F$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>want $F$</div>
    <div>$\vee$E 1,2</div>
    <div>$\supset$I 2-3</div>
  </div>
</div>




The $\supset$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 $\supset$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:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
  </div>
  <div class="proof">
    <div>$\Phi$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\Psi$</div>
        <div>$\Psi\ \&\ \Phi$</div>
      </div>
    </div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&I 1, 2</div>
  </div>
</div>




Does this show that one can prove any arbitrary sentence $\Psi$ from any
arbitrary premise $\Phi$? After all, we've written $\Psi\ \&\ \Phi$ on a line of a proof that
began with $\Phi$, 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; $\supset$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:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div>$\Phi$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">$\Psi$</div>
        <div>$\Psi\ \&\ \Phi$</div>
      </div>
    </div>
    <div>$\Psi \supset (\Psi\ \&\ \Phi)$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&I 1, 2</div>
    <div>$\supset$I 2-3</div>
  </div>
</div>

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:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
  </div>
  <div class="proof">
    <div class="last-premise">$R \vee F$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\neg R$</div>
        <div>F</div>
      </div>
    </div>
    <div>$\neg R \supset F$</div>
    <div>$F \lor A$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>want $F$</div>
    <div>$\vee$E 1,2</div>
    <div>$\supset$I 2-3</div>
    <div>$\lor$I 3</div>
  </div>
</div>

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 $\supset$I rule looks like this:

<div class="tri-proof">
 <div class="num">
   <div>m</div>
   <div>n</div>
   <div>&nbsp;</div>
 </div>
 <div class="proof">
   <div class="tri-proof">
     <div class="num">
       <div>&nbsp;</div>
       <div>&nbsp;</div>
     </div>
     <div class="proof">
       <div  class="last-premise">$\Phi$</div>
       <div>$\Psi$</div>
     </div>
   </div>
   <div>$\Phi \supset \Psi$</div>
 </div>
 <div class="justification">
   <div>want $\Psi$</div>
   <div>&nbsp;</div>
   <div>$\supset$I m-n</div>
 </div>
</div>

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 $\supset$I rule, for instance, you must assume the antecedent of the conditional.

The $\supset$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.


```{.PrettyProof}
P \supset Q
Q \supset R
P \supset 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 $\supset$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:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
  </div>
  <div class="proof">
    <div>P $\supset$ Q</div>
    <div class="last-premise">Q $\supset$ R</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">P</div>
      </div>
    </div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>want R</div>
  </div>
</div>


We made $P$ available by assuming it in a subproof, allowing us to use $\supset$E
on the first premise. This gives us $Q$, which allows us to use $\supset$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 $\supset$I rule and finish the
proof.

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
    <div>6</div>
  </div>
  <div class="proof">
    <div>P $\supset$ Q</div>
    <div class="last-premise">Q $\supset$ R</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">P</div>
        <div>Q</div>
        <div>R</div>
      </div>
    </div>
    <div>P $\supset$ R</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>want R</div>
    <div>$\supset$E 1,3</div>
    <div>$\supset$E 2,4</div>
    <div>$\supset$I 3-5</div>
  </div>
</div>


### **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 \supset X$ and $X \supset 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:

<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi \supset \Psi$</div>
    <div>$\Psi \supset \Phi$</div>
    <div>$\Phi \equiv \Psi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\equiv$I m,n</div>
  </div>
</div>


### **7.9.4 Biconditional Elimination**


The biconditional elimination rule ($\equiv$ E) is a generalized version of
*modus ponens* ($\supset$ 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:

<div class="side-by-side">
  <div class="tri-proof">
    <div class="num">
      <div>m</div>
      <div>n</div>
      <div>&nbsp;</div>
    </div>
    <div class="proof">
      <div>$\Phi \equiv \Psi$</div>
      <div>$\Phi$</div>
      <div>$\Psi$</div>
    </div>
    <div class="justification">
      <div>&nbsp;</div>
      <div>&nbsp;</div>
      <div>$\equiv$E m,n</div>
    </div>
  </div>
  <div class="tri-proof">
     <div class="num">
      <div>m</div>
      <div>n</div>
      <div>&nbsp;</div>
    </div>
    <div class="proof">
      <div>$\Phi \equiv \Psi$</div>
      <div>$\Psi$</div>
      <div>$\Phi$</div>
    </div>
    <div class="justification">
      <div>&nbsp;</div>
      <div>&nbsp;</div>
      <div>$\equiv$E m,n</div>
    </div>
  </div>
</div>


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.
> | $\therefore$ 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 ($\neg$ I) rule:

<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>o</div>
    <div>p</div>
  </div>
  <div class="proof">
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">$\Phi$</div>
        <div>$\Psi$</div>
        <div>$\neg \Psi$</div>
      </div>
    </div>
    <div>$\neg \Phi$</div>
  </div>
  <div class="justification">
    <div>(for reductio)</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\neg$I m-n, m-o</div>
  </div>
</div>


The $\neg$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 $\Psi$, and a subproof from that
same assumption to $\neg \Psi$. 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: $\neg(G$ & $\neg G)$. We can prove this
without any premises by immediately starting a subproof. We want to
apply $\neg$I to the subproof, so we assume $(G$ & $\neg G)$. We then get
an explicit contradiction by &E. The proof looks like this:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">G & $\neg$G</div>
        <div>G</div>
        <div>$\neg$G</div>
      </div>
    </div>
    <div>$\neg$(G & $\neg$G)</div>
  </div>
  <div class="justification">
    <div>for reductio</div>
    <div>&E 1</div>
    <div>&E 1</div>
    <div>$\neg$I 1-2, 1-3</div>
  </div>
</div>

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

<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>o</div>
    <div>p</div>
  </div>
  <div class="proof">
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">$\neg \Phi$</div>
        <div>$\Psi$</div>
        <div>$\neg \Psi$</div>
      </div>
    </div>
    <div>$\Phi$</div>
  </div>
  <div class="justification">
    <div>for reductio</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>$\neg$E m-n, m-o</div>
  </div>
</div>


### **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:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
  </div>
  <div class="proof">
    <div>$\Phi$</div>
    <div>$\Phi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>R 1</div>
  </div>
</div>


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:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
    <div>6</div>
  </div>
  <div class="proof">
    <div>P</div>
    <div class="last-premise">Q $\supset \neg$ P</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">Q</div>
        <div>$\neg$ P</div>
        <div>P</div>
      </div>
    </div>
    <div>$\neg$ Q</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>want $\neg$ Q</div>
    <div>for reductio</div>
    <div>$\supset$E 2, 3</div>
    <div>R 1</div>
    <div>$\neg$I 3-4, 3-5</div>
  </div>
</div>

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 $\neg P$ both follow from the assumption that $Q$. In the case of $\neg 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 $\neg 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:



<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
    <div>6</div>
  </div>
  <div class="proof">
    <div>$\Phi$</div>
    <div class="last-premise">$\Psi \supset \neg \Phi$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\Psi$</div>
        <div>$\neg \Phi$</div>
        <div>$\Phi$</div>
      </div>
    </div>
    <div>$\neg \Psi$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>want $\neg$ Q</div>
    <div>for reductio</div>
    <div>$\supset$E 2, 3</div>
    <div>R 1</div>
    <div>$\neg$I 3-4, 3-5</div>
  </div>
</div>

As always,  $\Phi$ and $\Psi$ 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:


<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>o</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi \vee \Psi$</div>
    <div>$\Phi \supset \Omega$</div>
    <div>$\Psi \supset \Omega$</div>
    <div>$\Omega$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>DIL m, n, o</div>
  </div>
</div>

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:

> | <span class="premise"> If it is raining, the car is wet.</span>
> | <span class="premise"> If it is snowing, the car is wet.</span>
> | <span class="premise"> It is raining or it is snowing.</span>

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:



<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
    <div>6</div>
    <div>7</div>
    <div>8</div>
    <div>9</div>
    <div>10</div>
    <div>11</div>
    <div>12</div>
    <div>13</div>
    <div>14</div>
  </div>
  <div class="proof">
    <div>$\Phi \vee \Psi$</div>
    <div>$\Phi \supset \Omega$</div>
    <div class="last-premise">$\Psi \supset \Omega$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div  class="last-premise">$\neg \Omega$</div>
        <div class="tri-proof">
          <div class="num">
            <div>&nbsp;</div>
            <div>&nbsp;</div>
            <div>&nbsp;</div>
          </div>
          <div class="proof">
            <div  class="last-premise">$\Phi$</div>
            <div>$\Omega$</div>
            <div>$\neg \Omega$</div>
          </div>
        </div>
        <div>$\neg \Phi$</div>
        <div class="tri-proof">
          <div class="num">
            <div>&nbsp;</div>
            <div>&nbsp;</div>
            <div>&nbsp;</div>
          </div>
          <div class="proof">
            <div  class="last-premise">$\Psi$</div>
            <div>$\Omega$</div>
            <div>$\neg \Omega$</div>
          </div>
        </div>
        <div>$\Psi$</div>
        <div>$\neg \Psi$</div>
      </div>
    </div>
    <div>$\Omega$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>want $\Omega$</div>
    <div>for reductio</div>
    <div>for reductio</div>
    <div>$\supset$E 2, 5</div>
    <div>R 4</div>
    <div>$\neg$I 5-6, 5-7</div>
    <div>for reductio</div>
    <div>$\supset$E 3, 9</div>
    <div>R 4</div>
    <div>$\vee$E 1, 8</div>
    <div>$\neg$I 9-10, 9-11</div>
    <div>$\neg$E 4-12, 4-13</div>
  </div>
</div>


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

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.

<div class="tri-proof">
  <div class="num">
    <div>m</div>
    <div>n</div>
    <div>&nbsp;</div>
  </div>
  <div class="proof">
    <div>$\Phi \supset \Psi$</div>
    <div>$\Psi \supset \Omega$</div>
    <div>$\Phi \supset \Omega$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>&nbsp;</div>
    <div>HS m, n</div>
  </div>
</div>

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 $\Phi$, $\Psi$, and $\Omega$, respectively.



**7.11 Rules of Replacement**
----------------

Consider how you would prove this argument valid:

```{.PrettyProof}
F\supset(G & H)
F\supset 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:

<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
    <div>5</div>
  </div>
  <div class="proof">
    <div class="last-premise">$F \supset (G$ & $H)$</div>
    <div class="tri-proof">
      <div class="num">
        <div>&nbsp;</div>
        <div>&nbsp;</div>
        <div>&nbsp;</div>
      </div>
      <div class="proof">
        <div class="last-premise">$\neg F$</div>
        <div>$G$ & $H$</div>
        <div>$G$</div>
      </div>
    </div>
    <div>$F \supset G$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>want G</div>
    <div>$\supset$E 1, 2</div>
    <div>&E 3</div>
    <div>$\supset$I 2-4</div>
  </div>
</div>

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:

> | $(\Phi$ & $\Psi) \Longleftrightarrow (\Psi$ & $\Phi)$
> | $(\Phi \vee \Psi) \Longleftrightarrow (\Psi \vee \Phi)$
> | $(\Phi \equiv \Psi) \Longleftrightarrow (\Psi \equiv \Phi)$ 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:

```{.PrettyProof}
(M \vee P) \supset (P & M)
(P \vee M) \supset (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:


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
  </div>
  <div class="proof">
    <div class="last-premise">$(M \vee P) \supset (P\ \&\ M)$</div>
    <div>$(P \vee M) \supset (P\ \&\ M)$</div>
    <div>$(P \vee M) \supset (M\ \&\ P)$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>Comm 1</div>
    <div>Comm 2</div>
  </div>
</div>

(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:

> | $\neg \neg \Phi \Longleftrightarrow \Phi$ 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:

> | $\neg(\Phi \vee \Psi) \Longleftrightarrow (\neg\Phi$ & $\neg\Psi)$
> | $\neg(\Phi$ & $\Psi) \Longleftrightarrow (\neg\Phi \vee \neg\Psi)$ DeM


As we have seen, $\Phi \supset \Psi$ is equivalent to
$\neg\Phi \vee \Psi$. A further replacement rule captures this
equivalence. We abbreviate the rule MC, for 'material conditional.' It
takes two forms:

> | $(\Phi \supset \Psi) \Longleftrightarrow (\neg \Phi \vee \Psi)$
> | $(\Phi \vee \Psi) \Longleftrightarrow (\neg\Phi \supset \Psi)$ MC

Now consider this argument:
> | $\neg(P \supset Q)$,
> | $\therefore P$ & $\neg Q$

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


<div class="tri-proof">
  <div class="num">
    <div>1</div>
    <div>2</div>
    <div>3</div>
    <div>4</div>
  </div>
  <div class="proof">
    <div class="last-premise">$\neg (P \supset Q)$</div>
    <div>$\neg (\neg P \lor Q)$</div>
    <div>$\neg \neg P\ \&\ \neg Q$</div>
    <div>$P\ \&\ \neg Q$</div>
  </div>
  <div class="justification">
    <div>&nbsp;</div>
    <div>MC 1</div>
    <div>DeM 2</div>
    <div>DN 3</div>
  </div>
</div>

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

> | $[(\Phi \supset \Psi)$ & $(\Psi \supset \Phi)] \Longleftrightarrow (\Phi \equiv \Psi)]$ $\equiv$ 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 $\Phi \supset\Psi$,
plan to use the $\supset$I rule. This requires starting a subproof in which you
assume $\Phi$. In the subproof, you want to derive $\Psi$.

**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 $\Phi \supset \Psi$, and you also have $\Phi$, $\supset$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 $\Phi \vee\Psi$, it is often
easier to show $\neg\Phi \supset \Psi$ 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
'$\vdash$' to indicate provability. Provability is relative to a proof
system, so the meaning of the '$\vdash$' 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 '$\vdash_{T}$' stand for provability in the tree
system, and '$\vdash_{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 '$\vdash$' to mean '$\vdash_{ND}$'.

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

When we write $\{\Phi_{1},\Phi_{2},\ldots\} \vdash_{ND} \Psi$,
this means that it is possible to give a natural deduction proof of $\Psi$ with
$\Phi_{1}$,$\Phi_{2}$,$\ldots$ as premises. With just one premise,
we leave out the curly braces, so $\Phi \vdash \Psi$ means that
there is a proof of $\Psi$ with $\Phi$ as a premise. Naturally, $\vdash\Phi$ means
that there is a proof of $\Phi$ that has no premises. You can think of it as
shorthand for $\emptyset \vdash \Phi$.

For notational completeness, we can understand $\chi \vdash \bot$
to mean that from $\chi$, we could prove an arbitrary contradiction. In other
words, $\chi$ is an inconsistent set.

Logical proofs are sometimes called *derivations*. So
$\Phi \vdash \Psi$ can be read as '$\Psi$ is derivable from $\Phi$.'

A **theorem** is a sentence that is derivable without any premises; i.e., $\Phi$ is a
theorem if and only if $\vdash \Phi$.

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 $\neg(P$ & $\neg P)$, which shows
that $(P$ & $\neg 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., $\Phi \vdash \Psi$ and $\Psi \vdash \Phi$.

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 $\Phi$ and $\Psi$ were provably equivalent?)

The set of sentences $\{\Phi_{1}, \Phi_{2}, \ldots\}$ is **provably inconsistent** if and only
if contradictory sentences are derivable from it; i.e., for some
sentence $\Psi$, $\{\Phi_{1}, \Phi_{2}, \ldots\} \vdash \Psi$ and
$\{\Phi_{1}, \Phi_{2}, \ldots\} \vdash \neg\Psi$. This is
equivalent to $\{\Phi_{1},\Phi_{2}, \ldots\} \vdash \bot$.

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 $\vdash \Phi$ and thus show that it is a
theorem, it follows that $\Phi$ is a tautology; i.e., $\models \Phi$.
Similarly, if we construct a model in which $\Phi$ is false and thus show that
it is not a tautology, it follows that $\Phi$ is not a theorem.

In general, $\Phi \vdash \Psi$ if and only if
$\Phi \models \Psi$. 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.



--------------------------------------------------------------------------------
                           YES                                 NO
-------------------------  ----------------------------------- -----------------------------
Is $\Phi$ a tautology?     -prove $\vdash \Phi$                 -give a model in which

                                                                $\Phi$ is false

Is $\Phi$ a contradiction? -prove $\vdash \neg \Phi$            -give a model in which

                                                                $\Phi$ is true

Is $\Phi$ contingent?       -*construct two models*,            -either prove $\vdash \Phi$

                           one in which $\Phi$ is               or  $\neg \Phi$

                           true and another in which

                           $\Phi$ is false

Are $\Phi$ and $\Psi$      -prove $\Phi\vdash \Psi$             -give a model in which

equivalent?                and $\Psi\vdash \Phi$                $\Phi$ and $\Psi$ have

                                                                different truth values

Is the set $\mathbb{A}$    -give a model  in                    -taking the sentences

consistent?                which all sentences in               in $\mathbb{A}$, prove

                           $\mathbb{A}$ are true                $\Psi$ and $\neg \Psi$

Is the argument            -prove                               -*construct a model* in

$\Phi, \Psi, \dots$        $\Phi, \Psi, \dots \vdash \Omega$    which $\mathcal{P}$ is true

  $\Omega$  valid?                                              and $\Omega$ is false
  --------------------------------------------------------------------------------

<caption>Table 7.1: Sometimes it is easier to show something by providing proofs than it
is by providing models. Sometimes it is the other way round. It
depends on what you are trying to show.</caption>


**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 ($\chi \vdash_{T} \Phi$ only if
$\chi \models \Phi$) and complete ($\chi \models \Phi$ only if
$\chi \vdash_{T} \Phi$). The natural deduction system of this
chapter is also both sound and complete for SL. In other words,
$\chi \vdash_{ND} \Phi$ if and only if
$\chi \models \Phi.$ 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 ($\chi \vdash_{T} \Phi)$ iff
($\chi \vdash_{ND} \Phi$).


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 $\vee 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 $\Phi\models\Psi$ implies
$\Phi\vdash\Psi$? 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 $\vdash\Phi$.

-   Two sentences $\Phi$ and $\Psi$ are **provably equivalent** if and only if $\Phi\vdash\Psi$ and
    $\Psi\vdash\Phi$.

-   $\{\Phi_1,\Phi_2,\ldots\}$ is **provably inconsistent** if and only if, for some
    sentence $\Psi$,
    $\{\Phi_1,\Phi_2,\ldots\}\vdash(\Psi \&\neg \Psi)$.



**Practice Exercises**
----------------------

<a href="./NDInstructions.pandoc">Here</a> is a set of instructions about how to use the natural deduction proof construction/checking tool.

Also, if you click <a href="./chapter7Problems.pandoc">here</a>, 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.



~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
A.1 W>-B, A&W, B\/(J&K) :|-: K
|W>-B :PR
|A&W :PR
|B\/(J&K) :PR
|W
|-B
|J&K
|K
~~~


~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
A.2 L<->-O, L\/-O :|-: L
|L<->-O :PR
|L\/-O :PR
| -L :AS
| -O
| L
| -L
|L
~~~



~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
A.3 Z->(C&-N), -Z -> (N&-C) :|-: N\/C
|Z->(C&-N) :PR
|-Z -> (N&-C) :PR
| -(N\/C) :AS
| -N&-C
|   Z :AS
|   C&-N
|   C
|   -C
| -Z
| N& -C
| N
| -N
|N\/C
~~~


**Part B** Give a proof for each argument in SL.

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
B.1 K&L :|-: K<->L
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
B.2 A->(B->C) :|-: (A&B)->C
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
B.3 P&(Q\/R), P->-R :|-: Q\/E
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
B.4 (C&D)\/E :|-: E\/D
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
B.5 -F-> G, F->H :|-: G\/H
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
B.6 (X&Y)\/(X&Z), -(X&D), (D\/M) :|-: M
~~~


**Part C** Give a proof for each argument in SL.

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.1 Q->(Q&-Q) :|-: -Q
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.2 J->-J :|-: -J
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.3 E\/F, F\/G, -F :|-: E&G
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.4 A<->B, B<->C :|-: A<->C
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.5 M\/(N->M) :|-: -M->-N
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.6 S<->T :|-: S<->(T\/S)
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.7 (M\/N)&(O\/P),N->P,-P :|-: M&O
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
C.8 (Z&K)\/(K&M),K->D :|-: D
~~~


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

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
D.1 :|-: O->O
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
D.2 :|-: N\/-N
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
D.3  :|-: -(P&-P)
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
D.4  :|-: -(A->-C)->(A->C)
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
D.5 :|-: J <-> [J \/ (L & -L)]
~~~

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


~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.1a ----G :|-: G
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.1b G :|-: ----G
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.2a T->S :|-: -S->-T
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.2b -S->-T :|-: T->S
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.3a R<->E :|-: E<->R
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.3b E<->R :|-: R<->E
~~~

~~~{.ProofChecker .ZachTFL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.4a -G<->H :|-: -(G<->H)
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.4b -(G<->H) :|-: -G<->H
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.5a U-> I :|-: -(U&-I)
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
E.5b -(U&-I) :|-: U-> I
~~~

**Part F** Provide proofs for each of the following


~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
F.1 M&(-N->-M) :|-: (N&M)\/-M
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
F.2 C->(E&G),-C->G :|-: G
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
F.3 (Z&K)<->(Y&M),D&(D->M):|-: Y->Z
~~~

~~~{.ProofChecker .IchikawaJenkinsSL options="fonts popout resize render indent" submission="none" guides="fitch"}
F.4 (W\/X)\/(Y\/Z), X->Y , -Z:|-: W\/Y
~~~


**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: $\Phi\supset\Psi$, $\neg\Psi$, $\therefore \neg \Phi$.
2. Show that Comm is a legitimate rule for the biconditional. Using only the basic rules, prove that $\Phi \equiv \Psi$ and $\Psi \equiv \Phi$ are equivalent.
3. Using only the basic rules, prove the following instance of DeMorgan’s Laws: $(\neg A\ \&\ \neg B)$, $\therefore \neg(A \lor B)$.
4. Show that $\equiv$ex is a legitimate derived rule. Using only the basic rules, prove that $D \equiv E$ and $(D \supset E)\ \&\ (E \supset D)$ are equivalent.


**Part H**

1. If you know that $\Phi \vdash \Psi$, what can you say about $(\Phi\&\Omega) \vdash \Psi$? Explain your answer.
2. If you know that $\Phi\vdash \Psi$, what can you say about $(\Phi \lor \Omega) \vdash \Psi$? Explain your answer.




<script>
  // Get top level div.tri-proof
  let triProofs = [...document.querySelectorAll('article > .tri-proof')];

  triProofs.forEach((triProof) => {
    let lastPremiseRowNums = getLastPremiseRowNumbers(triProof);
    let subProofRowNums = getSubProofRowNumbers(triProof.querySelector('.proof'));
    let nums = triProof.querySelector('.num');
    let justifications = triProof.querySelector('.justification');
    lastPremiseRowNums.forEach((lastPremiseRowNum) => {
      nums && nums.children[lastPremiseRowNum].classList.add('m-lp');
      justifications && justifications.children[lastPremiseRowNum].classList.add('m-lp');
    });
    subProofRowNums.forEach((subProofRowNum) => {
      nums && nums.children[subProofRowNum].classList.add('m-sp');
      justifications && justifications.children[subProofRowNum].classList.add('m-sp');
    });
  });

  function getLastPremiseRowNumbers(root) {
    let q = [];
    q.push(root);
    let rowNumber = -1, rowNumbers = [];
    while (q.length !== 0) {
      let node = q.shift();
      if (node.classList.contains('tri-proof')) {
        q.unshift(node.querySelector('.proof'));
        continue;
      }
      if (node.classList.contains('proof')) {
        q.unshift(...node.children);
        continue;
      }
      rowNumber++;
      if (node.classList.contains('last-premise')) {
        rowNumbers.push(rowNumber);
      }
    }
    return rowNumbers;
  }

  function getSubProofRowNumbers(root) {
    let q = [];
    q.push(root);
    let rowNumber = 0, rowNumbers = [];
    while (q.length !== 0) {
      let node = q.shift();
      if (node.classList.contains('proof')) {
        q.unshift(...node.children)
        if (node.endProof && q.length > 0) {
          q[0].endProof = true;
        }
        continue;
      }
      if (node.classList.contains('tri-proof')) {
        if (q.length > 0) {
          q[0].endProof = true;
        }
        q.unshift(node.querySelector('.proof'));
        rowNumbers.push(rowNumber);
        continue;
      }
      if (node.endProof) {
        rowNumbers.push(rowNumber);
      }
      rowNumber++;
    }
    return rowNumbers;
  }
</script>