your proof as Proof Conjunction 2.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Default and generous uses of the § rules

As we said, Fitch is generous in its interpretation of the inference rules of F.

For example, Fitch considers the following to be an acceptable use of § Elim:

17. Tet(a) § Tet(b) § Tet(c) § Tet(d)

.

.

.

26. Tet(d) § Tet(b) § Elim: 17

Section 6.1

146 / Formal Proofs and Boolean Logic

What we have done here is pick two of the conjuncts from step 17 and assert

the conjunction of these in step 26. Technically, F would require us to de-

rive the two conjuncts separately and, like Humpty Dumpty, put them back

together again. Fitch does this for us.

Since Fitch lets you take any collection of conjuncts in the cited sentence

and assert their conjunction in any order, Fitch™s interpretation of § Elim

allows you to prove that conjunction is “commutative.” In other words, you

can use it to take a conjunction and reorder its conjuncts however you please:

13. Tet(a) § Tet(b)

.

.

.

21. Tet(b) § Tet(a) § Elim: 13

You try it

................................................................

1. Open the ¬le Conjunction 3. Notice that there are two goals. The ¬rst goal

asks you to prove Tet(c) § Tet(a) from the premise. Strictly speaking, this

would take two uses of § Elim followed by one use of § Intro. However,

Fitch lets you do this with a single use of § Elim. Try this and then check

the step.

2. Verify that the second goal sentence also follows by a single application of

Fitch™s rule of § Elim. When you have proven these sentences, check your

goals and save the proof as Proof Conjunction 3.

3. Next try out other sentences to see whether they follow from the given

sentence by § Elim. For example, does Tet(c) § Small(a) follow? Should

it?

4. When you are satis¬ed you understand conjunction elimination, close the

¬le, but don™t save the changes you made in step 3.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

The § Intro rule implemented in Fitch is also less restrictive than our dis-

cussion of the formal rule might suggest. First of all, Fitch does not care about

the order in which you cite the supporting sentences. Second, if you cite a sen-

tence, that sentence can appear more than once as a conjunct in the concluding

sentence. For example, you can use this rule to conclude Cube(a) § Cube(a)

from the sentence Cube(a), if you want to for some reason.

Chapter 6

Conjunction rules / 147

Both of the conjunction rules have default uses. If at a new step you cite

a conjunction and specify the rule as § Elim, then when you check the step default uses of

conjunction rules

(or choose Check Proof), Fitch will ¬ll in the blank step with the leftmost

conjunct in the cited sentence. If you cite several sentences and apply § Intro,

Fitch will ¬ll in the conjunction of those steps, ordering conjuncts in the same

order they were cited.

You try it

................................................................

1. Open the ¬le Conjunction 4.

2. Move the focus to the ¬rst blank step, the one immediately following the

premises. Notice that this step has a rule speci¬ed, as well as a support

sentence cited. Check the step to see what default Fitch generates.

3. Then, focus on each successive step, try to predict what the default will

be, and check the step. (The last two steps give di¬erent results because

we entered the support steps in di¬erent orders.)

4. When you have checked all the steps, save your proof as Proof Conjunc-

tion 4.

5. Feel free to experiment with the rule defaults some more, to see when they

are useful.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

One ¬nal point: In applying conjunction introduction, you will sometimes

have to be careful about parentheses, due to our conventions about dropping parentheses and

conjunction rules

outermost parentheses. If one of the conjuncts is itself a conjunction, then

of course there is no need to add any parentheses before forming the larger

conjunction, unless you want to. For example, the following are both correct

applications of the rule. (The ¬rst is what Fitch™s default mechanism would

give you.)

Correct: 1. A § B

2. C

3. (A § B) § C § Intro: 1, 2

Correct: 1. A § B

2. C

3. A § B § C § Intro: 1, 2

Section 6.1

148 / Formal Proofs and Boolean Logic

However, if one of the conjuncts is a disjunction (or some other complex

sentence), to prevent ambiguity you may need to reintroduce the parentheses

that you omitted before. Thus the ¬rst of the following is a correct proof, but

the second contains a faulty application of conjunction introduction, since it

concludes with an ambiguous sentence.

Correct: 1. A ∨ B

2. C

3. (A ∨ B) § C § Intro: 1, 2

Wrong: 1. A ∨ B

2. C

3. A ∨ B § C § Intro: 1, 2

Section 6.2

Disjunction rules

We know: the conjunction rules were boring. Not so the disjunction rules,

particularly disjunction elimination.

Disjunction introduction

The rule of disjunction introduction allows you to go from a sentence Pi to

any disjunction that has Pi among its disjuncts, say P1 ∨ . . . ∨ Pi ∨ . . . ∨ Pn .

In schematic form:

Disjunction Introduction (∨ Intro):

Pi

.

.

.

P1 ∨ . . . ∨ Pi ∨ . . . ∨ Pn

Once again, we stress that Pi may be the ¬rst or last disjunct of the conclusion.

Further, as with conjunction introduction, some thought ought to be given to

whether parentheses must be added to Pi to prevent ambiguity.

As we explained in Chapter 5, disjunction introduction is a less peculiar

rule than it may at ¬rst appear. But before we look at a sensible example of

how it is used, we need to have at our disposal the second disjunction rule.

Chapter 6

Disjunction rules / 149

Disjunction elimination

We now come to the ¬rst rule that corresponds to what we called a method

of proof in the last chapter. This is the rule of disjunction elimination, the

formal counterpart of proof by cases. Recall that proof by cases allows you

to conclude a sentence S from a disjunction P1 ∨ . . . ∨ Pn if you can prove

S from each of P1 through Pn individually. The form of this rule requires us

to discuss an important new structural feature of the Fitch-style system of

deduction. This is the notion of a subproof.

A subproof, as the name suggests, is a proof that occurs within the context subproofs

of a larger proof. As with any proof, a subproof generally begins with an as-

sumption, separated from the rest of the subproof by the Fitch bar. But the

assumption of a subproof, unlike a premise of the main proof, is only temporar- temporary

assumptions

ily assumed. Throughout the course of the subproof itself, the assumption acts

just like an additional premise. But after the subproof, the assumption is no

longer in force.

Before we give the schematic form of disjunction elimination, let™s look at

a particular proof that uses the rule. This will serve as a concrete illustration

of how subproofs appear in F.

1. (A § B) ∨ (C § D)

2. A § B

3. B § Elim: 2

4. B ∨ D ∨ Intro: 3

5. C § D

6. D § Elim: 5

7. B ∨ D ∨ Intro: 6

8. B ∨ D ∨ Elim: 1, 2“4, 5“7

With appropriate replacements for A, B, C, and D, this is a formalization

of the proof given on page 133. It contains two subproofs. One of these runs

from line 2 to 4, and shows that B ∨ D follows if we (temporarily) assume

A § B. The other runs from line 5 to 7, and shows that the same conclu-

sion follows from the assumption C § D. These two proofs, together with the

premise (A § B) ∨ (C § D), are just what we need to apply the method of proof

by cases”or as we will now call it, the rule of disjunction elimination.

Look closely at this proof and compare it to the informal proof given

on page 133 to see if you can understand what is going on. Notice that the

Section 6.2

150 / Formal Proofs and Boolean Logic

assumption steps of our two subproofs do not have to be justi¬ed by a rule any

more than the premise of the larger “parent” proof requires a justi¬cation.

This is because we are not claiming that these assumptions follow from what

comes before, but are simply assuming them to show what follows from their

supposition. Notice also that we have used the rule ∨ Intro twice in this proof,

since that is the only way we can derive the desired sentence in each subproof.

Although it seems like we are throwing away information when we infer B ∨ D

from the stronger claim B, when you consider the overall proof, it is clear that

B ∨ D is the strongest claim that follows from the original premise.

We can now state the schematic version of disjunction elimination.

Disjunction Elimination (∨ Elim):

P1 ∨ . . . ∨ Pn

.

.

.

P1

.

.

.

S

“

Pn

.

.

.

S

.

.

.

S

What this says is that if you have established a disjunction P1 ∨. . . ∨Pn , and

you have also shown that S follows from each of the disjuncts P1 through Pn ,

then you can conclude S. Again, it does not matter what order the subproofs

appear in, or even that they come after the disjunction. When applying the

rule, you will cite the step containing the disjunction, plus each of the required

subproofs.

Let™s look at another example of this rule, to emphasize how justi¬cations

involving subproofs are given. Here is a proof showing that A follows from the

sentence (B § A) ∨ (A § C).

Chapter 6

Disjunction rules / 151