1 of 2

14.1 Know the Basics

The first step to learning how to do difficult proofs is knowing the basics. You should be able to take out a blank piece of paper and write down all the formal proof rules (Intro, Elim, Reit) rules from memory.

This is an essential skills check-in for you!

Do that now. This is an essential skills check-in for you!

By writing down the rules, we mean the little sketch or schema we used to teach you what each rule is, like this:

1. P&Q 
2. P


You should write out all the rules several times a day until it is so easy for you it seems ridiculous to keep bothering.

If you can’t write out the Intro and Elim rules on a blank piece of paper from memory, this is a critical early intervention for you!

If you can’t do that, then this is a critical early intervention: you need to invest more time in formal proofs now, before the class gets harder!

The key to this training is to space out your attempts: if the rules are just in short-term memory, then it is easy to write them out. You need to try writing them out several hours later, and again the next morning.

While you are memorizing the rules, it is helpful to also solve easy proofs with them. The science of learning has conclusively shown that learning something in context is far easier than learning it out of the blue.

The context for formal proof rules is actually doing formal proofs with them: that is what they are for. So let’s practice.

Next we’ll walk you through a set of lessons that cover the idiosyncrasies of each rule.

Lesson 1

Lesson 1: Obey the parentheses

The first lesson is that you must obey parentheses when they are there. Rules only apply to the main connective of a sentence, so if you want to do &Elim on this sentence:

1. P&(Q&R)

You cannot write:

2. R  


Parentheses are like traffic signals: they dictate the flow of inferences in the proof.

&Elim allows you to bring down the conjuncts of the main conjunction, so you could write P or you could write Q&R with &Elim.

You already know that we are allowed to have a long string of conjunctions or disjunctions:


In that case, all of the &s are considered to have the same scoping; they are all main connectives. So if there are no parentheses, then you can bring down any conjunct.

But you can’t pick and choose. For example, you’re not allowed to infer P&S from P&Q&R&S with &Elim.

Instead, you have to bring down P on one line, and S on another, and then put them together with &Intro.

Lesson 2

Lesson 2: Only two negations at a time

The second lesson is that ~Elim does not work exactly like the DN (double negation) principle. When we did chain of equivalences with DN, we allowed you to do multiple applications of it at once.

But with ~Elim, you can only eliminate two negations at a time.

Lesson 3

Lesson 3: Just two rules allow you to jump proof lines

The third lesson is that moving from a subproof to the parent proof is a special event. Only two rules allow us do that: vElim and ~Intro.

Starting subproofs is easy: you can just start a new subproof and cite it with Assume. But you can only get out of a subproof by using one of those two rules.

You might be wondering why you couldn’t use the #Elim rule. After all, #Elim allows you to write whatever you want, so why not write the conclusion?

Technically speaking, there is a correct use of #Elim that allows you to write ~(P&Q). But the problem is that it would still be within the subproof:

The trouble is that doing #Elim here is no help. Even though that line is not invalid, it doesn’t make progress toward our goal, because we’re still stuck in the subproof.

When you’re stuck in a subproof, ask yourself: why did I start this subproof? That tells you how to end it.

When you’re in a situation like this, stuck in a subproof and can’t get out, ask yourself: why did I start this subproof in the first place?

The reason why you started it tells you how to end it. If you started it because you’re doing a reductio, then you get out of it by proving # and using ~Intro. If you started it because you have a disjunction, and the assumption is one of your disjuncts, then you get out of it by proving the same sentence in every case and using vElim.

What if you started it for a different reason, not for one of those? Then there’s a problem!

Remember: ~Intro and vElim are the only two rules that let you move proof lines and get out of a subproof.

Lesson 4

Lesson 4: Never start a subproof without a plan

The fourth lesson is just a continuation of the third.

We said above that starting subproofs is easy: you can temporarily assume anything you want during a proof. But don’t abuse the power!

When you temporarily assume something, it starts another subproof line, and you have to get out of it in order to finish the proof.

It’s no good to start assuming things, and then blindly hope that later on it will pay off and you can get out of the subproofs. Instead, you should only start a subproof when you have a plan. Either you already know a disjunction, and your plan is proof by cases, or you think the assumption can get you a contradiction, and your plan is reductio.

Lesson 5

Lesson 5: vElim: do cases left to right

The fifth lesson creates uniformity so that we approach proofs in the same way. vElim requires that you prove the same sentence in every case.

If you are doing any repeated operations, go from left to right.

We require that you do the case on the left-hand side of the disjunction first.

Similarly, if you are bringing down conjuncts from a conjunction, bring them down from left to right.

That doesn’t mean you must always bring down every conjunct of a conjunction. Sometimes you only need one of them, and you can just do that one.

But for any operation you are performing repeatedly, perform it from left to right.

Lesson 6

Lesson 6: More disjuncts means more cases

Lesson 6 spells out a point that was already implicit in proof by cases: you need to do a subproof for every case.

We have focused on basic disjunctions with two disjuncts, like PvQ, which only have two cases to consider.

But if you have three disjuncts all on the main scope, like PvQvR, then you need three cases. Make sure to follow Lesson 6 and do them left to right!

Lesson 7

Lesson 7: One-line subproofs don’t need a dash.

Here’s our final lesson for now: one-line subproofs are allowed.

For proof by cases, you have to end every subproof with the same sentence. But what if your assumption is the sentence you are proving in each case?

You could use Reit, but that isn’t even necessary. If a subproof only has one line, then technically it both begins and ends with that sentence.

When you cite one-line subproofs, no dash “-” is necessary, just cite the number of the subproof.

Great work! You’ve completed the bootcamp basics, and you’re ready for the harder stuff!