. 28
( 107 .)


5. Prove the second goal sentence similarly. Once both goals check out, save
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

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):

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
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


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
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


. 28
( 107 .)