Language, Proof, and
Now we return to doing proofs. Last time we did proofs, we had only the =Intro,
=Elim, and Reit rules. Now, however, we have added three logical connectives to
our arsenal, and we can introduce rules governing what we can do with each of
Notes on Chapters 5 and 6
Proof by Cases; Proof by
Chapter 5 concerns informal "methods of proof." Chapter 6 concerns formal
proofs. The informal methods apply to logical reasoning in general; the rules
in chapter 6 are an attempt to formalize the informal methods and include them
in our formal system. Although our homework will emphasize doing formal proofs,
in a sense the informal methods are more important. There may be many different
ways to formalize these informal methods; what is important about the formal
rules is not so much the specific formalization as the general insights that
The main informal methods discussed in Chapter 5 are:
- proof by cases, and
- proof by contradiction (sometimes called reductio ad absurdum).
In proof by cases, we determine what possibilities there are, and then
attempt to show that our conclusion follows no matter which of these
In proof by contradiction, we assume the opposite of what we want to prove,
and show that this assumption leads to a contradiction. Then we conclude that
our original assumption was false, i.e. that its negation is true.
The formal system includes not only rules corresponding to these informal
methods, but also rules that capture steps that are so obvious that we don't
usually notice them in informal reasoning, but that still need to be captured
in the formal system. We will have Intro and Elim rules for every connective we
Today we are discussing only the conjunction and disjunction rules; next
time we will consider the negation rules.
So, we need to discuss:
- ∧Intro (conjunction introduction)
- ∧Elim (conjunction elimination)
- ∨Intro (disjunction introduction)
- ∨Elim (disjunction elimination)
Three of these are very obvious and straightforward. The fourth, disjunction
elimination, is more interesting, and corresponds to the method of proof by
Rules for ¬ and
Now we will add Intro and Elim rules for ¬. In the process we introduce a
new symbol, ⊥, with its own Intro and Elim rules.
- Let's take the easy rule first. This is ¬Elim, which allows us to write
down P if we already have ¬¬P.
- ¬Intro is trickier. It corresponds to the method of proof that Chapter 5
calls "Indirect Proof" or "Proof by Contradiction." (The same method is
also often called "reductio ad absurdum.")
The general idea: if a sentence leads to a contradiction, it must not be
true (so its negation must be true). So at the beginning of a ¬Intro
application, we have a sentence that we have not derived and whose negation
we also have not derived. We want to establish that the negation of the
sentence is true. So we start by assuming, for the sake of argument, the
opposite of what we want to prove -- that is, if we want to prove ¬P, we
start by assuming P. If we can derive a contradiction inside the subproof,
then back in the main proof, we can infer that ¬P. The idea is that if P
leads to a contradiction, then the negation of P must be true.
What do we mean by "a contradiction"? Well, we will use the symbol
represent a contradiction. So we need a
⊥Intro rule to allow us to write
⊥ on a line of our proof.
⊥Intro works like this: if on
earlier lines of our proof (or subproof) we have established any sentences
one of which has the form P and the other of which has the form ¬P, then
we can write down
⊥. Notice that P can itself be a compound sentence, so,
for example, the sentences (Tet(a)
∧ Large(b)) and ¬(Tet(a)
∧ Large(b)) would work.
We also have a
⊥Elim rule. This is strictly speaking unnecessary; we
could always get the same results without it, but it speeds things up a bit
in some circumstances. This rule allows us to write down anything we please
once we've gotten
⊥. (This seems strange, but the general idea is that if
the sentences you are working with are messed up enough to allow you to
derive ⊥, then anything goes.)
By the way, the fact that
will let you write down absolutely any sentence whatsoever is sometimes
called the "principle of explosion," since a proof of a contradiction
"explodes" into a proof of absolutely anything. There is a good discussion
of this principle here.
Proofs with no Premises
Tautologies are provable with no premises at all. Since they must be true no
matter what, i.e. since their truth does not depend on anything else, it is
possible to construct proofs for them which start from scratch, so to speak.
Of course, most of the rules in our system can only be used if we already
have one or more sentences to apply them to. The only exception we have had up
until now is the rule of identity introduction, whose use is pretty limited.
Now we have added another rule that requires no earlier steps: negation
introduction. (Later we will add another, conditional introduction.) So at this
point, if we are attempting to prove something with no premises, we can be
pretty certain we will need to use negation introduction. (The only exception
would be a proof in which we were just trying to prove something like a=a. But
since that's so easy, it's not likely to be assigned as an exercise!)
(One sort-of exception is proofs where we use Taut Con to establish the Law
of Excluded Middle, and then use disjunction introduction. But it is not really
an exception, because if we actually go through the steps of proving Excluded
Middle, we will need to use negation introduction.)
Hints on Constructing Proofs:
- Never start a subproof unless you know what rule you intend to use it
for, and what the last line of the subproof will be.
- Try to see why the overall proof, and each step along the way, makes
sense. (I.e. don't treat the rules as just a meaningless game; keep in mind
why they are reasonable.)
- Work both forward and backward (what rules can you use on the sentences
you've already got? What rules might get your final conclusion from some
- If you don't see anything else to do, try ¬Intro.
Last update: February 13, 2013.
Curtis Brown | Symbolic Logic | Philosophy
Department | Trinity University