Practice Problems: Proofs for TFL

The following are some practice problems on natural deduction proofs for TFL; i.e., they cover Part IV of forall x: Calgary.

When writing sentences of TFL, remember you can use the following ways to enter connectives that are easier to do with a keyboard:

not ¬ -, ~
and ∧ /\, &
or ∨ \/
if then → ->, >
if and only if ↔︎ <->, <>
contradiction ⊥ !?, _|_

The rules for ∧

To justify a sentence of the form 𝒫 ∧ 𝒬, you need both 𝒫 and 𝒬, separately, say with line numbers m and n. Then write as justification "∧I m, n" (replacing m, n with the actual line numbers, of course).

You can use 𝒫 ∧ 𝒬 to justify either 𝒫 or 𝒬 (whichever one you need, but only one per line). If 𝒫 ∧ 𝒬 appears on line number n, write "∧E n" next to 𝒫 (or 𝒬, as the case may be) as the justification.

Suppose you wanted to give a proof of the argument A ∧ B∴ B ∧ A. You would start your proof in the proof editor by listing the premises at the top. In this case there is just one premise, A ∧ B, which then is on line number 1. In Carnap, you indicate that a line is a premise by writing :PR to the right. Carnap will render the proof nicely, off to the right. For instance, it will draw a line under the last premise. Now you will have to write the steps leading to the conclusion underneath. Each line will have a sentence in it, and a justification separated by a colon : to the right. For instance, to justify line 2 by ∧E from line 1 you'd enter :/\E 1 next to the sentence A being justified. (Note: there must be no space between : and /\E.)

Fill in the missing justifications in the proof outline below. A line will get a + next to it once you have entered a correct justification. If the justification is incorrect, you'll get a ? or a . Carnap will try to tell you what's wrong: hover the cursor over the ? or to see a hint.

A /\ B :PR A B B /\ A

Note that this roundabout way is necessary, since B ∧ A and A ∧ B are different sentences. You first have to break A ∧ B apart and then put it back together. But note that once you have both A and B on separate lines, you can put them back together in any order, so you can get B ∧ A using I (which you want here), and also A ∧ B (which you don't want). You can also cite a line twice, if you want to justify A ∧ A, for instance.

For the next exercise, write the premise on line 1 (i.e., A /\ (B /\ C) :PR) and then try to find a proof of A ∧ C as the last line.


A tip:  ∧ E only breaks apart the exact conjunction into its two components—in this case, you can only get A and B ∧ C from line 1 using E. To get C, you have to apply E again.

The elimination rule for

The elimination rule for is modus ponens: you can justify 𝒬 if you already have both 𝒫 → 𝒬 and 𝒫, on separate previous lines.

In the next exercise you should prove C ∧ D from the premises A ∧ B, A → C, and B → D. You'll need the E rule twice to justify C and then D, but before you can use it, you have to prove the antecedents of the conditionals you cite. We've filled in some sentences and justifications; you do the rest!

A /\ B :PR A -> C:PR B -> D:PR A C :->E ? ? C /\ D :?

Proof construction strategies

We've already told you how the proof goes, but at this stage you may rightly wonder: well, how do you come up with the lines in the first place, other than guessing wildly? Chapter 17 describes some strategies that you should always try to use. For instance, the very first strategy is to "work backward" from a conjunction. It applies in this case. You want to prove C ∧ D. So your last line will have to be C ∧ D. When you start a proof from scratch, you should therefore not only put in the premises at the top, but also the last line at the bottom, like so:

A /\ B :PR A -> C:PR B -> D:PR ? C /\ D

Now to "work backwards" from C ∧ D means that you will put into your partial proof whatever is needed in order for you to correctly apply the I rule on the last line. (It's always the I rule for the main operator of the sentence you want to prove, in this case that's .) So you should write, between the premises and the last line, the corresponding sentences you'd need as justifications for I. In this case, that's C and D. (Go on, do it: replace the ? by two lines containing C and D.)

C and D are now your new "goals". You will also have to justify those, before you can use them to justify the last line. Let's focus on C. It has no main operator, so you cannot work backwards from it. But you can work forwards from the premises. You'll note that C is also the consequent of the conditional A → C on line 2. Working forwards from a conditional means: put in your proof whatever you'd need to justify your goal (here: C) from the sentence you have (here: A → C) by the E rule for the main operator of the sentence you're working forward from (here: ). Since to use E to justify C from A → C also requires you to have proved A, that's what you enter. (Go on, write A on a new line above C.)

You'll now note that you can justify A by E from premise 1. Then you can justify C by E. Now you go through the same process with D: working forward from the premise on line 3 you enter B above D. You can justify B by E from line 1, D by E from B and premise 3. Finally, now you can justify the last line C ∧ D by I.

Here's another longer exercise, without hints:

IV.40 pts

The introduction rule for →

The I rule requires a new idea, namely that of a subproof. To justify a conditional 𝒫 → 𝒬 you need a separate proof in which 𝒫 is an assumption made in addition to the premises of the entire proof. In Carnap, a subproof is made by indenting the lines that make up the subproof, and by justifying its first line (the assumption of the subproof) by :AS. Let's prove that A → B, B → C ⊢ A → C. Your last line has to be A → C, and it must not be indented at all. To prove it, you work backward: To use I to justify A → C, you need (above the last line) a subproof with assumption A and last line C. So you start your proof like this:

A -> B :PR B -> C :PR A :AS ? C A -> C :->I

Be careful when you write subproofs: the lines in a subproof all have to be indented the exact same amount. Carnap's pretty rendering is often misleading here. This proof box has some extra lines in the proof box itself to make that clear: try adding or removing a space before the C to see what happens.

Also, now that subproofs are involved, it's important to remember that the very last line of your proof should never be indented, i.e., never be inside a subproof.

Now let's combine all the rules we have so far to show that A → (B → C) ⊢ (A ∧ B) → (A ∧ C). Start by writing the premise and conclusion as the first and last line, then construct a subproof in between that you can use to justify the conclusion using I. For this to work, its assumption must be the antecedent of (A ∧ B) → (A ∧ C) and its last line the consequent. Remember, the assumption should have :AS as its justification on the right.


The rules for

The I rule is very simple: you can justify 𝒫 ∨ 𝒬 if you have 𝒫 (and also if you have 𝒬). So it's like the reverse of the E rule.


The E rule is more complicated. It requires two subproofs. To justify some sentence using a disjunction 𝒫 ∨ 𝒬 you need in addition two subproofs, one that derives from the assumption 𝒫, and one that derives from the assumption 𝒬. (To tell Carnap where one subproof ends and the next one starts, type -- on a line by itself. The -- should be indented the same amout as the sentences in the surrounding (sub)proof.)

IV.80 pts
A \/ B :PR A :AS ? -- B :AS ? B \/ A

Note that the sentence can be anything. It may even be one of the disjuncts, e.g, 𝒬. But, and this is important, the last sentence in both subproofs must be the same, and also identical to the sentence you are justifying using E.


The reiteration rule R is a very simple rule that sometimes comes in handy. It allows you to simply repeat a previous line. For instance, we need it if we want to prove that A → A is a tautology. This involves proving A → A, but our proof has no premises at all.

Working strategically is especially important when you prove tautologies like this one. You start by writing down A → A as the last line of your proof. (Since there are no premises it will start off also being the first line of your proof!) Then construct your proof above the sentence you're proving. Work backward from your goal sentence (here: A → A) by writing down what the I rule for the main connective (here: I) requires as a justification. In our case, we will need a subproof with assumption A and last line A. Now use the R rule!


Carnap will put a to the left of if you're expected to give a proof with no premises at all.

Here's another example: If B is true, then A → B is true. After all, the conditional A → B is true iff either A is false or B is true. So the argument B∴ A → B is valid.


You'll often need to do subproofs inside a bigger subproof. Here's an example that illustrates this:

IV.110 pts

Let's look at an example where we use A ∨ B and E to justify B (i.e., B plays both the role of 𝒬 and ). You will still need two subproofs in this case, although one is very simple (and just involves the assumption B and a single use of the R rule.)


Let's now prove A from A ∨ A. Here A plays both the role of 𝒫, 𝒬 and at the same time. You can do two subproofs in this case, both the same, and involving just the assumption A and a single use of the R rule. Or you can just make one subproof, but cite it twice in the E rule.


Now (re)read chapter 17, and let's apply the strategies to give a proof of something harder:


Rules for ¬

To deal with ¬, we introduce a new symbol into our language: . It works just like a sentence letter, except that we think of it as a sentence letter that is always false. It's read as "contradiction". Naturally, we let it be justified in a proof if we have somehow arrived at an outright contradiction: a pair of sentences 𝒫 and ¬𝒫. That's the ¬E rule: we can use ¬𝒫 to justify if we also have 𝒫.

The ¬I rule allows us to justify ¬𝒫 if we can show that assuming 𝒫 leads to a contradiction, in other words, if we can construct a subproof with assumption 𝒫 and last line .

Finally, we have a weird rule, called "explosion" X. We can use to justify anything.

The rules ¬E and X finally allow us to justify disjunctive syllogism.

IV.150 pts

Here's another example where the X rule is needed: a conditional A → B is true iff either A is false or B is true. Since A is false iff ¬A is true, that means the argument ¬A∴ A → B is valid. Let's prove it!


To see how the ¬I rule works, let's prove A → ¬¬A:


Here's another relatively easy one: the law of contraposition. This one will require triple-nested subproofs!


Now something a bit more challenging: one direction of one of De Morgan's laws.

IV.190 pts

Now let's try the other direction, but this time as a tautology:

IV.200 pts

Indirect proof

The final rule of natural deduction is indirect proof, IP. It works like ¬I, except the roles of 𝒫 and ¬𝒫 are reversed. In other words, a subproof with assumption ¬𝒫 that leads to allows you to justify 𝒫. You should use IP if all the other rules and strategies don't lead to a solution.

First, an easy exercise: the converse of contraposition. It's like IV.17, but you'll need IP instead of ¬I.

IV.210 pts

A harder example is A ∨ ¬A:

IV.220 pts

A proof box for you to play in!

Want to use Carnap to construct and check an arbitrary proof? You can do that in this "playground" proof editor. Use it for any of the exercises from Part IV in the book, for instance. (It will accept derived rules, too.)


Your proof is correct if all lines have a + next to them. Since Carnap does not know what you're trying to prove, it will tell you in the top line what you have proved.