Natural Deduction — Read

Example 1

Every assumption on its own is a derivation. So, e.g., $!A$source 46 by itself is a derivation, and so is $!B$source 47 by itself. We can obtain a new derivation from these by applying, say, the $\Intro{\land}$source 48 rule,

These rules are meant to be general: we can replace the $!A$source 56 and $!B$source 56 in it with any sentences, e.g., by $!C$source 57 and $!D$source 57. Then the conclusion would be $!C \land !D$source 58, and so

is a correct derivation. Of course, we can also switch the assumptions, so that $!D$source 66 plays the role of $!A$source 66 and $!C$source 66 that of $!B$source 67. Thus,

is also a correct derivation.

We can now apply another rule, say, $\Intro{\lif}$source 76, which allows us to conclude a conditional and allows us to discharge any assumption that is identical to the antecedent of that conditional. So both of the following would be correct derivations:

They show, respectively, that $!D \Proves !C \lif (!C \land !D)$source 95 and $!C \Proves !D \lif (!C \land !D)$source 96.

Remember that discharging of assumptions is a permission, not a requirement: we don't have to discharge the assumptions. In particular, we can apply a rule even if the assumptions are not present in the derivation. For instance, the following is legal, even though there is no assumption $!A$source 102 to be discharged:

source 45

Example 2

Let's give a derivation of the sentence $(!A \land !B) \lif !A$source 16.

We begin by writing the desired conclusion at the bottom of the derivation.

Next, we need to figure out what kind of inference could result in a sentence of this form. The main operator of the conclusion is $\lif$source 27, so we'll try to arrive at the conclusion using the conditional introduction rule rule. It is best to write down the assumptions involved and label the inference rules as you progress, so it is easy to see whether all assumptions have been discharged at the end of the proof.

We now need to fill in the steps from the assumption $!A \land !B$source 39 to $!A$source 39. Since we only have one connective to deal with, $\land$source 40, we must use the $\land$source 41 elim rule. This gives us the following proof:

We now have a correct derivation of $(!A \land !B) \lif !A$source 49.

source 15

Example 3

Now let's give a derivation of $(\lnot !A \lor !B) \lif (!A \lif !B)$source 54.

We begin by writing the desired conclusion at the bottom of the derivation.

To find a logical rule that could give us this conclusion, we look at the logical connectives in the conclusion: $\lnot$source 64, $\lor$source 65, and $\lif$source 65. We only care at the moment about the first occurrence of $\lif$source 66 because it is the main operator of the sentence in the end-sequent, while $\lnot$source 67, $\lor$source 67 and the second occurrence of $\lif$source 68 are inside the scope of another connective, so we will take care of those later. We therefore start with the conditional introduction rule rule. A correct application must look like this:

This leaves us with two possibilities to continue. Either we can keep working from the bottom up and look for another application of the conditional introduction rule rule, or we can work from the top down and apply a disjunction elimination rule rule. Let us apply the latter. We will use the assumption $\lnot !A \lor !B$source 81 as the leftmost premise of disjunction elimination rule. For a valid application of disjunction elimination rule, the other two premises must be identical to the conclusion $!A \lif !B$source 83, but each may be derived in turn from another assumption, namely one of the two disjuncts of $\lnot !A \lor !B$source 84. So our derivation will look like this:

In each of the two branches on the right, we want to derive $!A \lif !B$source 98, which is best done using conditional introduction rule.

For the two missing parts of the derivation, we need derivations of $!B$source 117 from $\lnot !A$source 117 and $!A$source 117 in the middle, and from $!A$source 118 and $!B$source 118 on the left. Let's take the former first. $\lnot !A$source 118 and $!A$source 119 are the two premises of negation elimination rule:

By using falsehood elimination rule, we can obtain $!B$source 127 as a conclusion and complete the branch.

Let's now look at the rightmost branch. Here it's important to realize that the definition of derivation allows assumptions to be discharged but does not require them to be. In other words, if we can derive $!B$source 152 from one of the assumptions $!A$source 152 and $!B$source 152 without using the other, that's ok. And to derive $!B$source 153 from $!B$source 153 is trivial: $!B$source 154 by itself is such a derivation, and no inferences are needed. So we can simply delete the assumption $!A$source 155.

Note that in the finished derivation, the rightmost conditional introduction rule inference does not actually discharge any assumptions.

source 53

Example 4

So far we have not needed the classical contradiction rule rule. It is special in that it allows us to discharge an assumption that isn't a sub-formula of the conclusion of the rule. It is closely related to the falsehood elimination rule rule. In fact, the falsehood elimination rule rule is a special case of the classical contradiction rule rule—there is a logic called “intuitionistic logic” in which only falsehood elimination rule is allowed. The classical contradiction rule rule is a last resort when nothing else works. For instance, suppose we want to derive $!A \lor \lnot !A$source 186. Our usual strategy would be to attempt to derive $!A \lor \lnot !A$source 187 using $\Intro{\lor}$source 187. But this would require us to derive either $!A$source 188 or $\lnot !A$source 188 from no assumptions, and this can't be done. classical contradiction rule to the rescue!

Now we're looking for a derivation of $\lfalse$source 196 from $\lnot(!A \lor \lnot !A)$source 196. Since $\lfalse$source 197 is the conclusion of $\Elim{\lnot}$source 197 we might try that:

Our strategy for finding a derivation of $\lnot !A$source 209 calls for an application of $\Intro{\lnot}$source 210:

Here, we can get $\lfalse$source 223 easily by applying $\Elim{\lnot}$source 223 to the assumption $\lnot(!A \lor \lnot !A)$source 224 and $!A \lor \lnot !A$source 224 which follows from our new assumption $!A$source 225 by $\Intro{\lor}$source 225:

On the right side we use the same strategy, except we get $!A$source 242 by classical contradiction rule:

source 178

Example 5

When dealing with quantifiers, we have to make sure not to violate the eigenvariable condition, and sometimes this requires us to play around with the order of carrying out certain inferences. In general, it helps to try and take care of rules subject to the eigenvariable condition first (they will be lower down in the finished proof).

Let's see how we'd give a derivation of the formula $\lexists[x][\lnot !A(x)] \lif \lnot \lforall[x][!A(x)]$source 21. Starting as usual, we write

We start by writing down what it would take to justify that last step using the conditional introduction rule rule.

Since there is no obvious rule to apply to $\lnot \lforall[x][!A(x)]$source 35, we will proceed by setting up the derivation so we can use the existential quantifier elimination rule rule. Here we must pay attention to the eigenvariable condition, and choose a constant that does not appear in $\lexists[x][!A(x)]$source 39 or any assumptions that it depends on. (Since no constants appear, however, any choice will do fine.)

In order to derive $\lnot \lforall[x][!A(x)]$source 50, we will attempt to use the negation introduction rule rule: this requires that we derive a contradiction, possibly using $\lforall[x][!A(x)]$source 52 as an additional assumption. Of course, this contradiction may involve the assumption $\lnot !A(a)$source 53 which will be discharged by the existential quantifier elimination rule inference. We can set it up as follows:

It looks like we are close to getting a contradiction. The easiest rule to apply is the universal quantifier elimination rule, which has no eigenvariable conditions. Since we can use any term we want to replace the universally quantified $x$source 70, it makes the most sense to continue using $a$source 71 so we can reach a contradiction.

It is important, especially when dealing with quantifiers, to double check at this point that the eigenvariable condition has not been violated. Since the only rule we applied that is subject to the eigenvariable condition was existential quantifier elimination rule, and the eigenvariable $a$source 91 does not occur in any assumptions it depends on, this is a correct derivation.

source 13

Example 6

Sometimes we may derive a formula from other formulas. In these cases, we may have undischarged assumptions. It is important to keep track of our assumptions as well as the end goal.

Let's see how we'd give a derivation of the formula $\lexists[x][!C(x,b)]$source 103 from the assumptions $\lexists[x][(!A(x) \land !B(x))]$source 103 and $\lforall[x][(!B(x) \lif !C(x,b))]$source 104. Starting as usual, we write the conclusion at the bottom.

We have two premises to work with. To use the first, i.e., try to find a derivation of $\lexists[x][!C(x, b)]$source 113 from $\lexists[x][(!A(x) \land !B(x))]$source 113 we would use the existential quantifier elimination rule rule. Since it has an eigenvariable condition, we will apply that rule first. We get the following:

The two assumptions we are working with share $!B$source 124. It may be useful at this point to apply conjunction elimination rule to separate out $!B(a)$source 125.

The second assumption we have to work with is $\lforall[x][(!B(x) \lif !C(x,b))]$source 137. Since there is no eigenvariable condition we can instantiate $x$source 139 with the constant $a$source 139 using universal quantifier elimination rule to get $!B(a) \lif !C(a, b)$source 140. We now have both $!B(a) \lif !C(a,b)$source 140 and $!B(a)$source 141. Our next move should be a straightforward application of the conditional elimination rule rule.

We are so close! One application of existential quantifier introduction rule and we have reached our goal.

Since we ensured at each step that the eigenvariable conditions were not violated, we can be confident that this is a correct derivation.

source 96

Example 7

Give a derivation of the formula $\lnot\lforall[x][!A(x)]$source 185 from the assumptions $\lforall[x][!A(x)] \lif \lexists[y][!B(y)]$source 185 and $\lnot\lexists[y][!B(y)]$source 186. Starting as usual, we write the target formula at the bottom.

The last line of the derivation is a negation, so let's try using negation introduction rule. This will require that we figure out how to derive a contradiction.

So far so good. We can use universal quantifier elimination rule but it's not obvious if that will help us get to our goal. Instead, let's use one of our assumptions. $\lforall[x][!A(x)] \lif \lexists[y][!B(y)]$source 203 together with $\lforall[x][!A(x)]$source 204 will allow us to use the conditional elimination rule rule.

We now have one final assumption to work with, and it looks like this will help us reach a contradiction by using negation elimination rule.

source 183