Chapter 18 Constructing proofs
There is no simple recipe for finding proofs, and there is no substitute for practice. Here, though, are some rules of thumb and strategies to keep in mind.
18.1 Working backward from what we want
So you’re trying to find a proof of some conclusion $\mathcal{C}$, which will be the last line of your proof. The first thing you do is look at $\mathcal{C}$ and ask what the introduction rule is for its main logical operator. This gives you an idea of what should happen before the last line of the proof. The justifications for the introduction rule require one or two other sentences above the last line, or one or two subproofs. Moreover, you can tell from $\mathcal{C}$ what those sentences are, or what the assumptions and conclusions of the subproof(s) are. Then you can write down those sentence or outline the subproof(s) above the last line, and treat those as your new goals.
For example: If your conclusion is a conditional $\mathcal{A}\to \mathcal{B}$, plan to use the $\to $I rule. This requires starting a subproof in which you assume $\mathcal{A}$. The subproof ought to end with $\mathcal{B}$. Then, continue by thinking about what you should do to get $\mathcal{B}$ inside that subproof, and how you can use the assumption $\mathcal{A}$.
If your goal is a conjunction, conditional, or negated sentence, you should start by working backward in this way. We’ll describe what you have to do in each of these cases in detail.
Working backward from a conjunction
If we want to prove $\mathcal{A}\wedge \mathcal{B}$, working backward means we should write $\mathcal{A}\wedge \mathcal{B}$ at the bottom of our proof, and try to prove it using $\wedge $I. At the top, we’ll write out the premises of the proof, if there are any. Then, at the bottom, we write the sentence we want to prove. If it is a conjunction, we’ll prove it using $\wedge $I.
Line number

Subproof level

Formula

Justification


$1$ 
0

${\mathcal{P}}_{1}$

PR

0

$\mathrm{\vdots}$



$k$ 
0

${\mathcal{P}}_{k}$

PR

0

$\mathrm{\vdots}$



$n$ 
0

$\mathcal{A}$


0

$\mathrm{\vdots}$



$m$ 
0

$\mathcal{B}$


$m+1$ 
0

$\mathcal{A}\wedge \mathcal{B}$

$\wedge $I $n$, $m$

For $\wedge $I, we need to prove $\mathcal{A}$ first, then prove $\mathcal{B}$. For the last line, we have to cite the lines where we (will have) proved $\mathcal{A}$ and $\mathcal{B}$, and use $\wedge $I. The parts of the proof labelled by the vertical $\mathrm{\cdots}$ have to still be filled in. We’ll mark the line numbers $m$, $n$ for now. When the proof is complete, these placeholders can be replaced by actual numbers.
Working backward from a conditional
If our goal is to prove a conditional $\mathcal{A}\to \mathcal{B}$, we’ll have to use $\to $I. This requires a subproof starting with $\mathcal{A}$ and ending with $\mathcal{B}$. We’ll set up our proof as follows:
Line number

Subproof level

Formula

Justification


$n$ 
open subproof,
1

$\mathcal{A}$


1

$\mathrm{\vdots}$



$m$ 
1

$\mathcal{B}$


$m+1$ 
close subproof,
0

$\mathcal{A}\to \mathcal{B}$

$\to $I $n$–$m$

Again we’ll leave placeholders in the line number slots. We’ll record the last inference as $\to $I, citing the subproof.
Working backward from a negated sentence
If we want to prove $\mathrm{\neg}\mathcal{A}$, we’ll have to use $\mathrm{\neg}$I.
Line number

Subproof level

Formula

Justification


$n$ 
open subproof,
1

$\mathcal{A}$


1

$\mathrm{\vdots}$



$m$ 
1

$\perp $


$m+1$ 
close subproof,
0

$\mathrm{\neg}\mathcal{A}$

$\mathrm{\neg}$I $n$–$m$

For $\mathrm{\neg}$I, we have to start a subproof with assumption $\mathcal{A}$; the last line of the subproof has to be $\perp $. We’ll cite the subproof, and use $\mathrm{\neg}$I as the rule.
When working backward, continue to do so as long as you can. So if you’re working backward to prove $\mathcal{A}\to \mathcal{B}$ and have set up a subproof in which you want to prove $\mathcal{B}$. Now look at $\mathcal{B}$. If, say, it is a conjunction, work backward from it, and write down the two conjuncts inside your subproof. Etc.
Working backward from a disjunction
Of course, you can also work backward from a disjunction $\mathcal{A}\vee \mathcal{B}$, if that is your goal. The $\vee $I rule requires that you have one of the disjuncts in order to infer $\mathcal{A}\vee \mathcal{B}$. So to work backward, you pick a disjunct, infer $\mathcal{A}\vee \mathcal{B}$ from it, and then continue to look for a proof of the disjunct you picked:
Line number

Subproof level

Formula

Justification


0

$\mathrm{\vdots}$



$n$ 
0

$\mathcal{A}$


$n+1$ 
0

$\mathcal{A}\vee \mathcal{B}$

$\vee $I $n$

However, you may not be able to prove the disjunct you picked. In that case you have to backtrack. When you can’t fill in the part labelled by the vertical $\mathrm{\cdots}$, delete everything, and try with the other disjunct:
Line number

Subproof level

Formula

Justification


0

$\mathrm{\vdots}$



$n$ 
0

$\mathcal{B}$


$n+1$ 
0

$\mathcal{A}\vee \mathcal{B}$

$\vee $I $n$

Obviously, deleting everything and starting over is frustrating, so you should avoid it. If your goal is a disjunction, therefore, you should not start by working backward: try working forward first, and apply the $\vee $I strategy only when working forward (and working backward using $\wedge $I, $\to $I, and $\mathrm{\neg}$I) no longer work.
18.2 Work forward from what you have
Your proof may have premises. And if you’ve worked backward in order to prove a conditional or a negated sentence, you will have set up subproofs with an assumption, and be looking to prove a final sentence in the subproof. These premises and assumptions are sentences you can work forward from in order to fill in the missing steps in your proof. That means applying elimination rules for the main operators of these sentences. The form of the rules will tell you what you’ll have to do.
Working forward from a conjunction
To work forward from a sentence of the form $\mathcal{A}\wedge \mathcal{B}$, we use $\wedge $E. That rule allows us to do two things: infer $\mathcal{A}$, and infer $\mathcal{B}$. So in a proof where we have $\mathcal{A}\wedge \mathcal{B}$, we can work forward by writing $\mathcal{A}$ and/or $\mathcal{B}$ immediately below the conjunction:
Line number

Subproof level

Formula

Justification


$n$ 
0

$\mathcal{A}\wedge \mathcal{B}$


$n+1$ 
0

$\mathcal{A}$

$\wedge $E $n$

$n+2$ 
0

$\mathcal{B}$

$\wedge $E $n$

Usually it will be clear in the particular situation you’re in which one of $\mathcal{A}$ or $\mathcal{B}$ you’ll need. It doesn’t hurt, however, to write them both down.
Working forward from a disjunction
Working forward from a disjunction works a bit differently. To use a disjunction, we use the $\vee $E rule. In order to apply that rule, it is not enough to know what the disjuncts of the disjunction are that we want to use. We must also keep in mind what we want to prove. Suppose we want to prove $\mathcal{C}$, and we have $\mathcal{A}\vee B$ to work with. (That $\mathcal{A}\vee B$ may be a premise of the proof, an assumption of a subproof, or something already proved.) In order to be able to apply the $\vee $E rule, we’ll have to set up two subproofs:
Line number

Subproof level

Formula

Justification


$n$ 
0

$\mathcal{A}\vee \mathcal{B}$


$n+1$ 
open subproof,
1

$\mathcal{A}$


1

$\mathrm{\vdots}$



$m$ 
1

$\mathcal{C}$


$m+1$ 
close subproof,
open subproof,
1

$\mathcal{B}$


1

$\mathrm{\vdots}$



$k$ 
1

$\mathcal{C}$


$k+1$ 
close subproof,
0

$\mathcal{C}$

$\vee $E $n$, ($n+1$)–$m$, ($m+1$)–$k$

The first subproof starts with the first disjunct, $\mathcal{A}$, and ends with the sentence we’re looking for, $\mathcal{C}$. The second subproof starts with the other disjunct, $\mathcal{B}$, and also ends with the goal sentence $\mathcal{C}$. Each of these subproofs have to be filled in further. We can then justify the goal sentence $\mathcal{C}$ by using $\vee $E, citing the line with $\mathcal{A}\vee \mathcal{B}$ and the two subproofs.
Working forward from a conditional
In order to use a conditional $\mathcal{A}\to \mathcal{B}$, you also need the antecedent $\mathcal{A}$ in order to apply $\to $E. So to work forward from a conditional, you will derive $\mathcal{B}$, justify it by $\to $E, and set up $\mathcal{A}$ as a new subgoal.
Line number

Subproof level

Formula

Justification


$n$ 
0

$\mathcal{A}\to \mathcal{B}$


0

$\mathrm{\vdots}$



$m$ 
0

$\mathcal{A}$


$m+1$ 
0

$\mathcal{B}$

$\to $E $n$, $m$

Working forward from a negated sentence
Finally, to use a negated sentence $\mathrm{\neg}\mathcal{A}$, you would apply $\mathrm{\neg}$E. It requires, in addition to $\mathrm{\neg}\mathcal{A}$, also the corresponding sentence $\mathcal{A}$ without the negation. The sentence you’ll get is always the same: $\perp $. So working forward from a negated sentence works especially well inside a subproof that you’ll want to use for $\mathrm{\neg}$I (or IP). You work forward from $\mathrm{\neg}\mathcal{A}$ if you already have $\mathrm{\neg}\mathcal{A}$ and you want to prove $\perp $. To do it, you set up $\mathcal{A}$ as a new subgoal.
Line number

Subproof level

Formula

Justification


$n$ 
0

$\mathrm{\neg}\mathcal{A}$


0

$\mathrm{\vdots}$



$m$ 
0

$\mathcal{A}$


$m+1$ 
0

$\perp $

$\mathrm{\neg}$E $n$, $m$

18.3 Strategies at work
Suppose we want to show that the argument $(A\wedge B)\vee (A\wedge C)\therefore A\wedge (B\vee C)$ is valid. We start the proof by writing the premise and conclusion down. (On a piece of paper, you would want as much space as possible between them, so write the premises at the top of the sheet and the conclusion at the bottom.)
Line number

Subproof level

Formula

Justification


$1$ 
0

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

PR

0

$\mathrm{\vdots}$



$n$ 
0

$A\wedge (B\vee C)$


We now have two options: either work backward from the conclusion, or work forward from the premise. We’ll pick the second strategy: we use the disjunction on line $1$, and set up the subproofs we need for $\vee $E. The disjunction on line $1$ has two disjuncts, $A\wedge B$ and $A\wedge C$. The goal sentence you want to prove is $A\wedge (B\vee C)$. So in this case you have to set up two subproofs, one with assumption $A\wedge B$ and last line $A\wedge (B\vee C)$, the other with assumption $A\wedge C$ and last line $A\wedge (B\vee C)$. The justification for the conclusion on line $n$ will be $\vee $E, citing the disjunction on line $1$ and the two subproofs. So your proof now looks like this:
Line number

Subproof level

Formula

Justification


$1$ 
0

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

PR

$2$ 
open subproof,
1

$A\wedge B$

AS

1

$\mathrm{\vdots}$



$n$ 
1

$A\wedge (B\vee C)$


$n+1$ 
close subproof,
open subproof,
1

$A\wedge C$

AS

1

$\mathrm{\vdots}$



$m$ 
1

$A\wedge (B\vee C)$


$m+1$ 
close subproof,
0

$A\wedge (B\vee C)$

$\vee $E $1$, $2$–$n$, ($n+1$)–$m$

You now have two separate tasks, namely to fill in each of the two subproofs. In the first subproof, we now work backward from the conclusion $A\wedge (B\vee C)$. That is a conjunction, so inside the first subproof, you will have two separate subgoals: proving $A$, and proving $B\vee C$. These subgoals will let you justify line $n$ using $\wedge $I. Your proof now looks like this:
Line number

Subproof level

Formula

Justification


$1$ 
0

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

PR

$2$ 
open subproof,
1

$A\wedge B$

AS

1

$\mathrm{\vdots}$



$i$ 
1

$A$


1

$\mathrm{\vdots}$



$n1$ 
1

$B\vee C$


$n$ 
1

$A\wedge (B\vee C)$

$\wedge $I $i$, $n1$

$n+1$ 
close subproof,
open subproof,
1

$A\wedge C$

AS

1

$\mathrm{\vdots}$



$m$ 
1

$A\wedge (B\vee C)$


$m+1$ 
close subproof,
0

$A\wedge (B\vee C)$

$\vee $E $1$, $2$–$n$, ($n+1$)–$m$

We immediately see that we can get line $i$ from line $2$ by $\wedge $E. So line $i$ is actually line $3$, and can be justified with $\wedge $E from line $2$. The other subgoal $B\vee C$ is a disjunction. We’ll apply the strategy for working backward from a disjunctions to line $n1$. We have a choice of which disjunct to pick as a subgoal, $B$ or $C$. Picking $C$ wouldn’t work and we’d end up having to backtrack. And you can already see that if you pick $B$ as a subgoal, you could get that by working forward again from the conjunction $A\wedge B$ on line $2$. So we can complete the first subproof as follows:
Line number

Subproof level

Formula

Justification


$1$ 
0

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

PR

$2$ 
open subproof,
1

$A\wedge B$

AS

$3$ 
1

$A$

$\wedge $E $2$

$4$ 
1

$B$

$\wedge $E $2$

$5$ 
1

$B\vee C$

$\vee $I $4$

$6$ 
1

$A\wedge (B\vee C)$

$\wedge $I $3$, $5$

$7$ 
close subproof,
open subproof,
1

$A\wedge C$

AS

1

$\mathrm{\vdots}$



$m$ 
1

$A\wedge (B\vee C)$


$m+1$ 
close subproof,
0

$A\wedge (B\vee C)$

$\vee $E $1$, $2$–$6$, $7$–$m$

Like line $3$, we get line $4$ from $2$ by $\wedge $E. Line $5$ is justified by $\vee $I from line $4$, since we were working backward from a disjunction there.
That’s it for the first subproof. The second subproof is almost exactly the same. We’ll leave it as an exercise.
Remember that when we started, we had the option of working forward from the premise, or working backward from the conclusion, and we picked the first option. The second option also leads to a proof, but it will look different. The first steps would be to work backward from the conclusion and set up two subgoals, $A$ and $B\vee C$, and then work forward from the premise to prove them, e.g.,
Line number

Subproof level

Formula

Justification


$1$ 
0

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

PR

$2$ 
open subproof,
1

$A\wedge B$

AS

1

$\mathrm{\vdots}$



$k$ 
1

$A$


$k+1$ 
close subproof,
open subproof,
1

$A\wedge C$

AS

1

$\mathrm{\vdots}$



$n1$ 
1

$A$


$n$ 
close subproof,
0

$A$

$\vee $E $1$, $2$–$k$, ($k+1$)–($n1$)

$n+1$ 
open subproof,
1

$A\wedge B$

AS

1

$\mathrm{\vdots}$



$l$ 
1

$B\vee C$


$l+1$ 
close subproof,
open subproof,
1

$A\wedge C$

AS

1

$\mathrm{\vdots}$



$m1$ 
1

$B\vee C$


$m$ 
close subproof,
0

$B\vee C$

$\vee $E $1$, ($n+1$)–$l$, ($l+1$)–($m1$)

$m+1$ 
0

$A\wedge (B\vee C)$

$\wedge $I $n$, $m$

We’ll leave you to fill in the missing pieces indicated by $\mathrm{\vdots}$.
Let’s give another example to illustrate how to apply the strategies to deal with conditionals and negation. The sentence $(A\to B)\to (\mathrm{\neg}B\to \mathrm{\neg}A)$ is a tautology. Let’s see if we can find a proof of it, from no premises, using the strategies. We first write the sentence at the bottom of a sheet of paper. Since working forward is not an option (there is nothing to work forward from), we work backward, and set up a subproof to establish the sentence we want, $(A\to B)\to (\mathrm{\neg}B\to \mathrm{\neg}A)$, using $\to $I. Its assumption must be the antecedent of the conditional we want to prove, i.e., $A\to B$, and its last line the consequent, $\mathrm{\neg}B\to \mathrm{\neg}A$.
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

$A\to B$

AS

1

$\mathrm{\vdots}$



$n$ 
1

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


$n+1$ 
close subproof,
0

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

$\to $I $1$–$n$

The new goal, $\mathrm{\neg}B\to \mathrm{\neg}A$ is itself a conditional, so working backward we set up another subproof:
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

$A\to B$

AS

$2$ 
open subproof,
2

$\mathrm{\neg}B$

AS

2

$\mathrm{\vdots}$



$n1$ 
2

$\mathrm{\neg}A$


$n$ 
close subproof,
1

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

$\to $I $2$–($n1$)

$n+1$ 
close subproof,
0

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

$\to $I $1$–$n$

From $\mathrm{\neg}A$ we again work backward. To do this, look at the $\mathrm{\neg}$I rule. It requires a subproof with $A$ as assumption, and $\perp $ as its last line. So the proof is now:
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

$A\to B$

AS

$2$ 
open subproof,
2

$\mathrm{\neg}B$

AS

$3$ 
open subproof,
3

$A$


3

$\mathrm{\vdots}$



$n2$ 
3

$\perp $


$n1$ 
close subproof,
2

$\mathrm{\neg}A$

$\mathrm{\neg}$I $3$–($n2$)

$n$ 
close subproof,
1

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

$\to $I $2$–($n1$)

$n+1$ 
close subproof,
0

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

$\to $I $1$–$n$

Now our goal is to prove $\perp $. We said above, when discussing how to work forward from a negated sentence, that the $\mathrm{\neg}$E rule allows you to prove $\perp $, which is our goal in the innermost subproof. So we look for a negated sentence which we can work forward from: that would be $\mathrm{\neg}B$ on line $2$. That means we have to derive $B$ inside the subproof, since $\mathrm{\neg}$E requires not just $\mathrm{\neg}B$ (which we have already), but also $B$. And $B$, in turn, we get by working forward from $A\to B$, since $\to $E will allow us to justify the consequent of that conditional, $B$, by $\to $E. The rule $\to $E also requires the antecedent $A$ of the conditional, but that is also already available (on line $3$). So we finish with:
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

$A\to B$

AS

$2$ 
open subproof,
2

$\mathrm{\neg}B$

AS

$3$ 
open subproof,
3

$A$


$4$ 
3

$B$

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

$5$ 
3

$\perp $

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

$6$ 
close subproof,
2

$\mathrm{\neg}A$

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

$7$ 
close subproof,
1

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

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

$8$ 
close subproof,
0

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

$\to $I $1$–$7$

18.4 Working forward from $\perp $
When applying the strategies, you will sometimes find yourself in a situation where you can justify $\perp $. Using the explosion rule, this would allow you to justify anything. So $\perp $ works like a wildcard in proofs. For instance, suppose you want to give a proof of the argument $A\vee B,\mathrm{\neg}A\therefore B$. You set up your proof, writing the premises $A\vee B$ and $\mathrm{\neg}A$ at the top on lines $1$ and $2$, and the conclusion $B$ at the bottom of the page. $B$ has no main connective, so you can’t work backward from it. Instead, you must work forward from $A\vee B$: That requires two subproofs, like so:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\vee B$

PR

$2$ 
0

$\mathrm{\neg}A$

PR

$3$ 
open subproof,
1

$A$

AS

1

$\mathrm{\vdots}$



$m$ 
1

$B$


$m+1$ 
close subproof,
open subproof,
1

$B$

AS

1

$\mathrm{\vdots}$



$k$ 
1

$B$


$k+1$ 
close subproof,
0

$B$

$\vee $E $1$, $3$–$m$, ($m+1$)–$k$

Notice that you have $\mathrm{\neg}A$ on line $2$ and $A$ as the assumption of your first subproof. That gives you $\perp $ using $\mathrm{\neg}$E, and from $\perp $ you get the conclusion $B$ of the first subproof using X. Recall that you can repeat a sentence you already have by using the reiteration rule R. So our proof would be:
Line number

Subproof level

Formula

Justification


$1$ 
0

$A\vee B$

PR

$2$ 
0

$\mathrm{\neg}A$

PR

$3$ 
open subproof,
1

$A$

AS

$4$ 
1

$\perp $

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

$5$ 
1

$B$

X $4$

$6$ 
close subproof,
open subproof,
1

$B$

AS

$7$ 
1

$B$

R $6$

$8$ 
close subproof,
0

$B$

$\vee $E $1$, $3$–$5$, $6$–$7$

18.5 Proceed indirectly
In very many cases, the strategies of working forward and backward will eventually pan out. But there are cases where they do not work. If you cannot find a way to show $\mathcal{A}$ directly using those, use IP instead. To do this, set up a subproof in which you assume $\mathrm{\neg}\mathcal{A}$ and look for a proof of $\perp $ inside that subproof.
Line number

Subproof level

Formula

Justification


$n$ 
open subproof,
1

$\mathrm{\neg}A$

AS

1

$\mathrm{\vdots}$



$m$ 
1

$\perp $


$m+1$ 
close subproof,
0

$\mathcal{A}$

IP $n$–$m$

Here, we have to start a subproof with assumption $\mathrm{\neg}\mathcal{A}$; the last line of the subproof has to be $\perp $. We’ll cite the subproof, and use IP as the rule. In the subproof, we now have an additional assumption (on line $n$) to work with.
Suppose we used the indirect proof strategy, or we’re in some other situation where we’re looking for a proof of $\perp $. What’s a good candidate? Of course the obvious candidate would be to use a negated sentence, since (as we saw above) $\mathrm{\neg}$E always yields $\perp $. If you set up a proof as above, trying to prove $\mathcal{A}$ using IP, you will have $\mathrm{\neg}\mathcal{A}$ as the assumption of your subproof—so working forward from it to justify $\perp $ inside your subproof, you would next set up $\mathcal{A}$ as a goal inside your subproof. If you are using this IP strategy, you will find yourself in the following situation:
Line number

Subproof level

Formula

Justification


$n$ 
open subproof,
1

$\mathrm{\neg}\mathcal{A}$

AS

1

$\mathrm{\vdots}$



$m1$ 
1

$\mathcal{A}$


$m$ 
1

$\perp $

$\mathrm{\neg}$E $n$, $m1$

$m+1$ 
close subproof,
0

$\mathcal{A}$

IP $n$–$m$

This looks weird: We wanted to prove $\mathcal{A}$ and the strategies failed us; so we used IP as a last resort. And now we find ourselves in the same situation: we are again looking for a proof of $\mathcal{A}$. But notice that we are now inside a subproof, and in that subproof we have an additional assumption ($\mathrm{\neg}\mathcal{A}$) to work with which we didn’t have before. Let’s look at an example.
18.6 Indirect proof of excluded middle
The sentence $A\vee \mathrm{\neg}A$ is a tautology, and so should have a proof even without any premises. But working backward fails us: to get $A\vee \mathrm{\neg}A$ using $\vee $I we would have to prove either $A$ or $\mathrm{\neg}A$—again, from no premises. Neither of these is a tautology, so we won’t be able to prove either. Working forward doesn’t work either, since there is nothing to work forward from. So, the only option is indirect proof.
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

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

AS

1

$\mathrm{\vdots}$



$m$ 
1

$\perp $


$m+1$ 
close subproof,
0

$A\vee \mathrm{\neg}A$

IP $1$–$m$

Now we do have something to work forward from: the assumption $\mathrm{\neg}(A\vee \mathrm{\neg}A)$. To use it, we justify $\perp $ by $\mathrm{\neg}$E, citing the assumption on line $1$, and also the corresponding unnegated sentence $A\vee \mathrm{\neg}A$, yet to be proved.
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

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

AS

1

$\mathrm{\vdots}$



$m1$ 
1

$A\vee \mathrm{\neg}A$


$m$ 
1

$\perp $

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

$m+1$ 
close subproof,
0

$A\vee \mathrm{\neg}A$

IP $1$–$m$

At the outset, working backward to prove $A\vee \mathrm{\neg}A$ by $\vee $I did not work. But we are now in a different situation: we want to prove $A\vee \mathrm{\neg}A$ inside a subproof. In general, when dealing with new goals we should go back and start with the basic strategies. In this case, we should first try to work backward from the disjunction $A\vee \mathrm{\neg}A$, i.e., we have to pick a disjunct and try to prove it. Let’s pick $\mathrm{\neg}A$. This would let us justify $A\vee \mathrm{\neg}A$ on line $m1$ using $\vee $I. Then working backward from $\mathrm{\neg}A$, we start another subproof in order to justify $\mathrm{\neg}A$ using $\mathrm{\neg}$I. That subproof must have $A$ as the assumption and $\perp $ as its last line.
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

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

AS

$2$ 
open subproof,
2

$A$

AS

2

$\mathrm{\vdots}$



$m3$ 
2

$\perp $


$m2$ 
close subproof,
1

$\mathrm{\neg}A$

$\mathrm{\neg}$I $2$–($m3$)

$m1$ 
1

$A\vee \mathrm{\neg}A$

$\vee $I $m2$

$m$ 
1

$\perp $

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

$m+1$ 
close subproof,
0

$A\vee \mathrm{\neg}A$

IP $1$–$m$

Inside this new subproof, we again need to justify $\perp $. The best way to do this is to work forward from a negated sentence; $\mathrm{\neg}(A\vee \mathrm{\neg}A)$ on line $1$ is the only negated sentence we can use. The corresponding unnegated sentence, $A\vee \mathrm{\neg}A$, however, directly follows from $A$ (which we have on line $2$) by $\vee $I. Our complete proof is:
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

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

AS

$2$ 
open subproof,
2

$A$

AS

$3$ 
2

$A\vee \mathrm{\neg}A$

$\vee $I $2$

$4$ 
2

$\perp $

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

$5$ 
close subproof,
1

$\mathrm{\neg}A$

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

$6$ 
1

$A\vee \mathrm{\neg}A$

$\vee $I $5$

$7$ 
1

$\perp $

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

$8$ 
close subproof,
0

$A\vee \mathrm{\neg}A$

IP $1$–$7$

Practice exercises
A. Use the strategies to find proofs for each of the following arguments:

1.
$A\to B,A\to C\therefore A\to (B\wedge C)$

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

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

4.
$A\vee (B\wedge C)\therefore (A\vee B)\wedge (A\vee C)$

5.
$(A\wedge B)\vee (A\wedge C)\therefore A\wedge (B\vee C)$

6.
$A\vee B,A\to C,B\to D\therefore C\vee D$

7.
$\mathrm{\neg}A\vee \mathrm{\neg}B\therefore \mathrm{\neg}(A\wedge B)$

8.
$A\wedge \mathrm{\neg}B\therefore \mathrm{\neg}(A\to B)$
B. Formulate strategies for working backward and forward from $\mathcal{A}\leftrightarrow \mathcal{B}$.
C. Use the strategies to find proofs for each of the following sentences:

1.
$\mathrm{\neg}A\to (A\to \perp )$

2.
$\mathrm{\neg}(A\wedge \mathrm{\neg}A)$

3.
$[(A\to C)\wedge (B\to C)]\to [(A\vee B)\to C]$

4.
$\mathrm{\neg}(A\to B)\to (A\wedge \mathrm{\neg}B)$

5.
$(\mathrm{\neg}A\vee B)\to (A\to B)$
Since these should be proofs of sentences from no premises, you will start with the respective sentence at the bottom of the proof, which will have no premises.
D. Use the strategies to find proofs for each one of the following arguments and sentences:

1.
$\mathrm{\neg}\mathrm{\neg}A\to A$

2.
$\mathrm{\neg}A\to \mathrm{\neg}B\therefore B\to A$

3.
$A\to B\therefore \mathrm{\neg}A\vee B$

4.
$\mathrm{\neg}(A\wedge B)\to (\mathrm{\neg}A\vee \mathrm{\neg}B)$

5.
$A\to (B\vee C)\therefore (A\to B)\vee (A\to C)$

6.
$(A\to B)\vee (B\to A)$

7.
$((A\to B)\to A)\to A$
These all will require the IP strategy. The last three especially are quite hard!