. 27
( 107 .)


of even and odd number. This is OK, but make these appeals explicit. Also make explicit any use of proof
by contradiction.

Assume that n2 is Assume that n2 is
5.23 5.24 5.25
Assume that n + m
odd. Prove that n is is odd. Prove that divisible by 3. Prove
that n2 is divisible
odd. n — m is even.
by 9.

5.26 A good way to make sure you understand a proof is to try to generalize it. Prove that 3 is
 irrational. [Hint: You will need to ¬gure out some facts about divisibility by 3 that parallel the
facts we used about even and odd, for example, the fact expressed in Exercise 5.25.] Can you
generalize these two results?

Section 5.4
Arguments with inconsistent premises
What follows from an inconsistent set of premises? If you look back at our
de¬nition of logical consequence, you will see that every sentence is a conse-
quence of such a set. After all, if the premises are contradictory, then there
are no circumstances in which they are all true. Thus, there are no circum-
stances in which the premises are true and the conclusion is false. Which is
to say, in any situation in which the premises are all true (there aren™t any
of these!), the conclusion will be true as well. Hence any argument with an
always valid
inconsistent set of premises is trivially valid. In particular, if one can establish
a contradiction ⊥ on the basis of the premises, then one is entitled to assert
any sentence at all.
This often strikes students as a very odd method of reasoning, and for very
good reason. For recall the distinction between a valid argument and a sound
one. A sound argument is a valid argument with true premises. Even though
any argument with an inconsistent set of premises is valid, no such argument
is sound, since there is no way the premises of the argument can all be true.
For this reason, an argument with an inconsistent set of premises is not worth

Chapter 5
Arguments with inconsistent premises / 141

much on its own. After all, the reason we are interested in logical consequence never sound
is because of its relation to truth. If the premises can™t possibly be true, then
even knowing that the argument is valid gives us no clue as to the truth or
falsity of the conclusion. An unsound argument gives no more support for its
conclusion than an invalid one.
In general, methods of proof don™t allow us to show that an argument
is unsound. After all, the truth or falsity of the premises is not a matter of
logic, but of how the world happens to be. But in the case of arguments with
inconsistent premises, our methods of proof do give us a way to show that at
least one of the premises is false (though we might not know which one), and
hence that the argument is unsound. To do this, we prove that the premises
are inconsistent by deriving a contradiction.
Suppose, for example, you are given a proof that the following argument
is valid:

Home(max) ∨ Home(claire)
Home(max) § Happy(carl)

While it is true that this conclusion is a consequence of the premises, your
reaction should not be to believe the conclusion. Indeed, using proof by cases
we can show that the premises are inconsistent, and hence that the argument
is unsound. There is no reason to be convinced of the conclusion of an unsound


A proof of a contradiction ⊥ from premises P1 , . . . , Pn (without addi-
tional assumptions) shows that the premises are inconsistent. An argu-
ment with inconsistent premises is always valid, but more importantly,
always unsound.


5.27 Give two di¬erent proofs that the premises of the above argument are inconsistent. Your ¬rst
 should use proof by cases but not DeMorgan™s law, while your second can use DeMorgan but
not proof by cases.

Section 5.4
Chapter 6

Formal Proofs and Boolean

The deductive system F is what is known as a system of natural deduction.
natural deduction
Such systems are intended to be models of the valid principles of reasoning
used in informal proofs. In this chapter, we will present the inference rules of
F that correspond to the informal principles of Boolean reasoning discussed in
the previous chapter. You will easily recognize the rules as formal counterparts
of some of the principles we™ve already discussed.
Although natural deduction systems like F are meant to model informal
reasoning, they are also designed to be relatively spare or “stripped down”
versions of such reasoning. For example, we told you that in giving an informal
proof, you can always presuppose steps that you and your audience already
know to be logically valid. So if one of the equivalence laws is not at issue
in a proof, you can simply apply it in a single step of your informal proof.
However, in F we will give you a very elegant but restricted collection of
inference rules that you must apply in constructing a formal proof. Many of
the valid inference steps that we have seen (like the DeMorgan Laws) are not
allowed as single steps; they must be justi¬ed in terms of more basic steps.
The advantage to this “lean and mean” approach is that it makes it easier to
prove results about the deductive system, since the fewer the rules, the simpler
the system. For example, one of the things we can prove is that anything you
could demonstrate with a system that contained rules for all of the named
logical equivalences of Chapter 4 can be proved in the leaner system F .
Systems of natural deduction like F use two rules for each connective,
one that allows us to prove statements containing the symbol, and one that
allows us to prove things from statements containing the symbol. The former
are called introduction rules since they let us introduce these symbols into
introduction and
elimination rules proofs. By contrast, the latter are called elimination rules. This is similar to
our treatment of the identity predicate in Chapter 2. If you go on to study
proof theory in more advanced logic courses, you will see that that this elegant
pairing of rules has many advantages over systems that include more inference
steps as basic.
The formal rules of F are all implemented in the program Fitch, allowing
you to construct formal proofs much more easily than if you had to write
them out by hand. Actually, Fitch™s interpretation of the introduction and

Conjunction rules / 143

elimination rules is a bit more generous in spirit than F. It doesn™t allow you
to do anything that F wouldn™t permit, but there are cases where Fitch will
let you do in one step what might take several in F. Also, many of Fitch™s
rules have “default applications” that can save you a lot of time. If you want rule defaults
the default use of some rule, all you have to do is specify the rule and cite
the step or steps you are applying it to; Fitch will then ¬ll in the appropriate
conclusion for you. At the end of each section below we™ll explain the default
uses of the rules introduced in that section.

Section 6.1
Conjunction rules
The simplest principles to formalize are those that involve the conjunction
symbol §. These are the rules of conjunction elimination and conjunction

Conjunction elimination

The rule of conjunction elimination allows you to assert any conjunct Pi of a
conjunctive sentence P1 § . . . § Pi § . . . § Pn that you have already derived
in the proof. (Pi can, by the way, be any conjunct, including the ¬rst or the
last.) You justify the new step by citing the step containing the conjunction.
We abbreviate this rule with the following schema:

Conjunction Elimination (§ Elim):

P1 § . . . § Pi § . . . § Pn

You try it
1. Open the ¬le Conjunction 1. There are three sentences that you are asked
to prove. They are shown in the goal strip at the bottom of the proof
window as usual.

2. The ¬rst sentence you are to prove is Tet(a). To do this, ¬rst add a new
step to the proof and write the sentence Tet(a).

Section 6.1
144 / Formal Proofs and Boolean Logic

3. Next, go to the popup Rule? menu and under the Elimination Rules,
choose §.

4. If you try to check this step, you will see that it fails, because you have
have not yet cited any sentences in support of the step. In this example,
you need to cite the single premise in support. Do this and then check the

5. You should be able to prove each of the other sentences similarly, by means
of a single application of § Elim. When you have proven these sentences,
check your goals and save the proof as Proof Conjunction 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Conjunction introduction

The corresponding introduction rule, conjunction introduction, allows you to
assert a conjunction P1 § . . . § Pn provided you have already established each
of its constituent conjuncts P1 through Pn . We will symbolize this rule in the
following way:

Conjunction Introduction (§ Intro):


P1 § . . . § Pn

In this rule, we have used the notation:



to indicate that each of P1 through Pn must appear in the proof before you
can assert their conjunction. The order in which they appear does not matter,
and they do not have to appear one right after another. They just need to
appear somewhere earlier in the proof.
Here is a simple example of our two conjunction rules at work together. It
is a proof of C § B from A § B § C.

Chapter 6
Conjunction rules / 145

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

Let™s try our hand using both conjunction rules in Fitch.

You try it
1. Open the ¬le Conjunction 2. We will help you prove the two sentences
requested in the goals. You will need to use both of the conjunction rules
in each case.

2. The ¬rst goal is Medium(d) § ¬Large(c). Add a new step and enter this
sentence. (Remember that you can copy the sentence from the goal pane
and paste it into the new step. It™s faster than typing it in.)

3. Above the step you just created, add two more steps, typing one of the
conjuncts in each. If you can prove these, then the conclusion will follow
by § Intro. Show this by choosing this rule at the conjunction step and
citing the two conjuncts in support.

4. Now all you need to do is prove each of the conjuncts. This is easily done
using the rule § Elim at each of these steps. Do this, cite the appropriate
support sentences, and check the proof. The ¬rst goal should check out.


. 27
( 107 .)