PROOFS WITHOUT TEARS

A Student's Handy Guide to Proving Sequents in the system of Allen/Hand, Logic Primer

The rules of any logical system define what a proof is. They do not, however, tell you how to build one. Here are some procedures that will help you with the latter.

What are you trying to prove?

A proof is a trip from a given destination from a given starting point. The destination is the conclusion; the starting point is the set of premisses. Your task is to discover a route--not the route, since there are many different ones.

A general strategy for getting to where you want to go from where you already are is to work backwards from your destination. If you need to get to Galveston, and you know how to get to Galveston from Houston, then all you have to figure out is how to get from where you are to Houston. If you know how to get from Waller to Houston (and Houston to Galveston), then all you have to do is figure out how to get from where you are to Waller. At each step of this process, you reduce your problem of how to get from where you are to Galveston to the problem of how to get from where you are to somewhere else--hopefully, somewhere closer to where you are. If your strategy works, eventually you reduce your problem to one you already know how to solve: I can get from College Station to Galveston if I can get to Houston, and I can get from College Station to Houston if I can get to Waller, and I can get from College Station to Waller if I can get to Hempstead, and I can get from College Station to Hempstead if I can get to Navasota--but, behold, I know how to get from College Station to Navasota. So, my problem is solved.

This kind of strategy works well in trying to discover proofs. Start with where you want to end up, that is, with the conclusion, and try to figure out how you could get there from something; keep working backwards from the intermediate steps until you find that what you need is something you know how to get.

On What Everything Is

A very, very important point to remember is that, in our formal system, there are just exactly six kinds of thing, and everything is exactly one of those and not two of those. Every wff is:

1. Atomic (a letter all by itself, or
2. a Negation (main connective ~)
3. a Conjunction (main connective &), or
4. a Disjunction (main connective v), or
5. a Conditional (main connective ->), or
6. a Biconditional (main connective <->)

This is the first thing to notice about any wff you're working with, since it determines both the strategies for proving it and the strategies for using it in proving other things.

Some important questions: the Direct Approach

There are several fundamental questions that will help in constructing a strategy. We'll call the strategy they rest on 'the direct approach'.

1. Do I already have it as part of something else?

The wff you need may already be present as a constituent part of something you have.

2. If I do, how do I take that thing apart and get out what I need?

This depends on what kind of wff it is. In general, the Elimination rules are useful here (see below).

3. If I don't, then how do I build what I need?

This depends on what kind of wff it is. In general, the Introduction rules are useful here.

More about Question 2: how to take things apart

More about Question 3: How to Build New Things

The Indirect Approach

Sometimes, the direct approach doesn't work. In that case (or at other times), you can always resort to 'the indirect approach': assume a denial of what you want to get, then try to get a contradictory pair so that you can use RAA.

Some exercises from 1.5.1 and 1.5.2

S12: P->Q, ~Q |- ~P

Since the Middle Ages, this rule has been called 'Modus Tollendo Tollens,' or just Modus Tollens', or just 'MT'

Here, what we want is not a constituent of any premise. So, we need to find a way to build it. ~P is a negation, so we need to introduce a '~'. The rule to do that with is RAA:

Next, we need to figure out what assumption to make (and discharge), and also how to deduce a statement and its denial. A good strategy is just to assume the denial of what we want:

Now, all we need is to get a pair of contradictories. Since we already have ~Q, one way to do this would be to get Q:

In fact, we do already have Q as part of premise 1. So, the next question is: how do we get it? The rule ->E lets us get the consequent of a conditional if we have its antecedent, which in this case is P. So, we could get Q if we could get P. Here, we're in luck: we do have P:

S13-15: These can be done with exactly the same strategy as S12

S13-S15 are variant forms of Modus Tollens

S16: P->Q, Q->R |- P->R

This rule has the name 'hypothetical syllogism', or 'HS'

What we need to get is a conditional, and it doesn't already appear in the premises. So, since we need to introduce an arrow, let's try ->I:

That is: if we can get R after assuming P (line 3), then we can get what we want with ->I and discharge the assumption. Our problem, then, reduces to this: how do we get R? R is found in premise (2) as the consequent of a conditional, so we could get it if we had the antecedent, Q. Once again, then, we've reduced our problem to another:

So now, we need to get Q. We have it on the right side of (1), so we could get it by ->E if we had the left side. But we do: it's (3). So, we're done:

S17: P |- Q->P

What we need to get is a conditional, and all that we have is an atomic sentence. So, we'll have to build the conclusion, and to do that we will need ->I:

All that remains, then, is to figure out how to get P, having assumed Q. But we already have P: it's the first premise. So, we're done:

S18: ~P |- P->Q

This rule is known as 'False Antecedent' (FA). A nice medieval Latin name is 'ex falso quodlibet'

The conclusion is a conditional, and it's not already present as part of any premise, so we should probably try to use ->I:

Of course, to use ->I, we'll have to assume the antecedent of the conditional we want (that is, P), then try to deduce its consequent (that is, Q). So, our proof will need to have this overall structure:

So, how can we get Q? There's an important point of strategy we can notice here. Q does not occur at all in the premises. Thus, we have to find a way to introduce a new atomic sentence in the proof. There are only two rules that allow us to get a conclusion containing a statement letter not found among the premises: vI and RAA. We're not trying to get a disjunction, so vI is not likely to be of much use here. Let's try RAA. The strategy would be to assume a denial of Q, then try to get a contradictory pair:

But wait! we've already got a sentence and its denial (lines (1) and (2)). So, we can fill in the details for RAA and for the rest of the proof:

S22: PvQ -||- ~P->Q

Among the names of this is 'Wedge-Arrow', or 'v->'.

This is a double turnstile, so we need to prove two sequents: PvQ |- ~P->Q and ~P->Q |- PvQ. The first is easy: since we need to build a conditional, we use ->I.

The second is a little harder: look here.

S25: PvQ, P->R, Q->R |-R

The venerable name for this is 'Simple Dilemma'. Please notice how many times 'm' and 'n' respectively do and do not occur in the word 'dilemma'.

We need to get R. Looking over the premises, we see that we could get R if we could get P, and we could also get R if we could get Q (each time using ->E). Which shall we try? Let's start by trying P:

So, the problem is how to get P. There's no rule that lets us get the left side of a conditional, but we could get it from line (1) if we had ~Q, using vE:

So, how could we get ~Q? It's not part of any premise, so the best strategy would be to try RAA. We would then assume Q and try to deduce a pair of contradictory formulas. Before we start down that path, however, let's look where it's leading us. If we look over the premises, the only thing we can get from them in one step with the additional assumption Q is R. There are no negations anywhere in the premises, so we might suspect that it's going to be hard to come up with our contradictory pair. We will probably have to make one or more assumptions in addition to Q.

At this point, we're approaching the condition of aimless floundering. Aimless floundering is, in fact, a strategy of sorts, rather like guessing on a multiple-choice quiz or buying lottery tickets: sometimes, those strategies win. However, when you find that you don't really know what to do next, that's usually a sign that it's time to give up on the direct approach and try the indirect approach. That's particularly apt when the conclusion you want is atomic, as it is in this case. So, let's start over:

So, we need to get a contradictory pair. Notice right away that if we assume either P or Q, we'll get R. This is promising, so let's try it:

Now we have a contradiction (lines (4 and 6). But which assumption do we want to discharge? If we discharge (4), we won't be done, because we'll still have (5) in the assumption set. However, we can discharge (5):

This takes us a little farther. With ~P, we can get Q (by vE, from (1)), and with Q we can get R (by ->E, from (3)). But R is a denial of ~R, so we have what we need.

Notice that we couldn't stop at (9), since there's something besides the premises in the assumption set. However, using RAA, we can get rid of that assumption. Line (10), remember, is the denial of line (4): it just happens to be the same thing as line (9)

S28: ~(PvQ) -||- ~P & ~Q

This is one of the rules known as 'DeMorgan's Law' (after 19th-century logician Augustus DeMorgan).

Left to right: we need to build a conjunction, so we'll use &I. To do that, we need to get both conjuncts, that is, ~P and ~Q. those are both negations, so we will use RAA for each.

Right to left: we need to build a negation, so it's best to try RAA at once. This turns out to be easy:

S44: P->(Q->R) -||- (P&Q) -> R

This is called 'exportation' going left to right and 'importation' right to left. I replaced a redundant pair of parentheses for clarity.

Right to left: we need to build a conditional, so we assume the antecedent. To get R from the premise, we need to get Q->R out first. Again, this is straightforward:

Right to left: a little more subtle. We need to build a conditional, but one side of it is a conditional. What we need to do, then, is assume P and try to get Q->R. Since that's also a conditional, we then assume Q and try to get R. Then, we discharge the two assumptions in reverse order:

S39: P->Q -||- ~Q->~P

For fairly obvious reasons, this is known as 'Transposition'.

For both directions: usual strategy for building a condition, that is, assume the antecedent, try to get the consequent, then use ->I. In each case, the way to get the consequent turns out to be RAA:

You might notice that these two proofs are very similar.

To keep this file from getting any longer, examples will be continued here. If there's nothing there, try again later.