1 of 2

12.2 vElim

vElim is just the formal proof rule that goes with proof by cases. Elim rules are for when you have a connective and need to reason from it, so vElim is for when you know a v and need to make an inference.

We need a way of modeling temporary assumptions in formal proofs.

vElim works just like proof by cases, which means that we need a way of formally modeling temporary assumptions for the cases.

Think of it like this: each case is like a mini-proof inside the main proof, since we need to prove that the conclusion follows in each case. The temporary assumption is like the premise of the mini-proof.

Subproof: a mini proof inside the main proof.

To model this in our proof system, we will just create another proof, called a subproof, inside the main proof.

Let’s see an example. Recall this equivalence:

PvQ ⇔ QvP

In order to prove this equivalence from left to right, we need to show, from the premise PvQ, that QvP follows. So the formal proof will look something like this:

1. PvQ
2. …
    QvP

Premise

We will represent a subproof with a vertical bar “|” before each sentence of BOOL that’s in the subproof.

Since our premise is a v, we need to use vElim. In order to represent subproofs, we will insert vertical bars in front of the sentence of BOOL, like this:

1. PvQ
2. | P
3. | QvP
4. …
?. QvP

Premise
Assume
Rule?

Lines 2 and 3 are the subproof, because they are indented with the subproof bar.

Since line 2 is an assumption, it does not need to be justified by one of the connective Intro or Elim rules, so we just write Assume.

Writing “Assume” for a temporary assumption is a lot like writing “Premise” for a premise.

Writing “Assume” for a temporary assumption is a lot like writing “Premise” for a premise. The difference is that the temporary assumption only holds within the subproof.

Basically, a temporary assumption gives you an “extra” premise to work with, as long as you are in that subproof.

Line 3, QvP, is still within the subproof. But it is not a temporary assumption, so it needs to be justified with a rule.

The proof is only done once we’ve proven the conclusion in the parent proof.

We’ve proven the conclusion in case 1, but we aren’t done yet. The proof is only done once we’ve proven the conclusion in the parent proof.

In order to prove the conclusion in the parent proof, we need to show that it follows in both cases. So we need to end the first subproof and start a new one for case 2.

The final proof looks like this:

1. PvQ
2. | P
3. | QvP
4. | Q
5. | QvP
6. QvP

Premise
Assume
vIntro;2
Assume
vIntro;4
vElim;1,2-3,4-5

Notice how the final conclusion, on line 6, occurs outside the subproofs. That is key. We can’t just show that the conclusion follows inside some subproof. If that were enough, we could have stopped at line 3.

We need to show that the conclusion follows from just the original premise, without relying on additional temporary assumptions.

We need to show that the conclusion follows from just the original premise, without relying on additional temporary assumptions.

Also notice how we cite the last line: it is vElim because we are showing that QvP follows in the main proof from line 1. (And line 1 is a disjunction.)

vElim requires the exact same sentence to appear three times: in each subproof and in the main proof below.

In order for the vElim rule to work, you need the exact same sentence to appear at the end of each subproof, and then you write that same sentence out of the subproofs, on the main proof line. We call this “exporting” the sentence, since you move it out into the main proof.

The rule always requires you to cite at least three things: you must cite the disjunction you are using or “eliminating”, and you need to cite all the subproofs you used for the cases, which will be two or more.

When you cite a subproof with multiple lines, you must use the dash “-“.

When you cite a subproof, you must use the dash “-“, since you are not just citing an individual line. You are citing each subproof as a unit.

Recall from Section 11.1 that we showed you a graphical device  you can add to formal proofs: horizontal and vertical lines.

Now that you know about subproofs, the point of those lines will be clearer. Here’s the graphical version of this proof:

Image showing a picture of the proof just given, with vertical lines showing the extent of each subproof.

The vertical line of the parent proof always extends to the bottom, because the premises govern the whole proof.

Each subproof has mini horizontal and vertical lines, which graphically convey the sense in which a temporary assumption is similar to a premise.

But the vertical line of a subproof always ends, which you can see in the gap between subproofs between lines 3 and 4.

Once that first subproof ends, you are not allowed to cite individual lines of it. Instead, you can only cite the subproof as a whole chunk using a dash “-“, as in vElim;1,2-3,4-5.

When you work on proofs with pen and paper, these graphical lines can help keep your subproofs in order.

When you work on proofs with pen and paper, these graphical lines can help keep your subproofs in order.

Your turn to try one. Here’s the start of the proof of P from (P&Q)v(P&R).

You’ve completed your own formal proof by cases, or vElim. Now you just need lots more practice!

Remember when to use proof by cases: whenever you have a disjunction you need to reason from, proof by cases is the plan.