. 30
( 107 .)


when the premises of your argument are themselves inconsistent. In fact, this
is how we give a formal proof that a set of premises is inconsistent. A formal
formal proofs of
inconsistency proof of inconsistency is a proof that derives ⊥ at the main level of the proof.
Let™s try out the rules of ⊥ Intro and ¬ Intro to see how they work.

You try it
1. To illustrate these rules, we will show you how to prove ¬¬A from A.
This is the other direction of double negation. Use Fitch to open the ¬le
Negation 1.
2. We will step you through the construction of the following simple proof.

1. A

2. ¬A
3. ⊥ ⊥ Intro: 1, 2
4. ¬¬A ¬ Intro: 2“3
3. To construct this proof, add a step immediately after the premise. Turn it
into a subproof by choosing New Subproof from the Proof menu. Enter
the assumption ¬A.
4. Add a new step to the subproof and enter ⊥, changing the rule to ⊥ Intro.
Cite the appropriate steps and check the step.

Chapter 6
Negation rules / 157

5. Now end the subproof and enter the ¬nal sentence, ¬¬A, after the sub-
proof. Specify the rule as ¬ Intro, cite the preceding subproof and check
the step. Your whole proof should now check out.

6. Notice that in the third line of your proof you cited a step outside the
subproof, namely the premise. This is legitimate, but raises an important
issue. Just what steps can be cited at a given point in a proof? As a ¬rst
guess, you might think that you can cite any earlier step. But this turns
out to be wrong. We will explain why, and what the correct answer is, in
the next section.

7. Save your proof as Proof Negation 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
The contradiction symbol ⊥ acts just like any other sentence in a proof. In
particular, if you are reasoning by cases and derive ⊥ in each of your subproofs,
then you can use ∨ Elim to derive ⊥ in your main proof. For example, here
is a proof that the premises A ∨ B, ¬A, and ¬B are inconsistent.
1. A ∨ B
2. ¬A
3. ¬B

4. A
5. ⊥ ⊥ Intro: 4, 2
6. B
7. ⊥ ⊥ Intro: 6, 3
8. ⊥ ∨ Elim: 1, 4“5, 6“7

The important thing to notice here is step 8, where we have applied ∨
Elim to extract the contradiction symbol from our two subproofs. This is
clearly justi¬ed, since we have shown that whichever of A or B holds, we
immediately arrive at a contradiction. Since the premises tell us that one or
the other holds, the premises are inconsistent.

Other ways of introducing ⊥

The rule of ⊥ Intro recognizes only the most blatant contradictions, those
where you have established a sentence P and its negation ¬P. What if in the
course of a proof you come across an inconsistency of some other form? For

Section 6.3
158 / Formal Proofs and Boolean Logic

example, suppose you manage to derive a single tt-contradictory sentence
like ¬(A ∨ ¬A), or the two sentences ¬A ∨ ¬B and A § B, which together form
a tt-contradictory set?
It turns out that if you can prove any tt-contradictory sentence or sen-
tences, the rules we™ve already given you will allow you to prove ⊥. It may
take a fair amount of e¬ort and ingenuity, but it is possible. We™ll eventually
prove this, but for now you™ll have to take our word for it.
One way to check whether some sentences are tt-contradictory is to try to
derive ⊥ from them using a single application of Taut Con. In other words,
introducing ⊥
with Taut Con enter ⊥, cite the sentences, and choose Taut Con from the Rule? menu. If
Taut Con tells you that ⊥ follows from the cited sentences, then you can be
sure that it is possible to prove this using just the introduction and elimination
rules for §, ∨, ¬, and ⊥.
Of course, there are other forms of contradiction besides tt-contradictions.
For example, suppose you manage to prove the three sentences Cube(b), b = c,
and ¬Cube(c). These sentences are not tt-contradictory, but you can see
that a single application of = Elim will give you the tt-contradictory pair
Cube(c) and ¬Cube(c). If you suspect that you have derived some sentences
whose inconsistency results from the Boolean connectives plus the identity
predicate, you can check this using the FO Con mechanism, since FO Con
introducing ⊥
with FO Con understands the meaning of =. If FO Con says that ⊥ follows from the cited
sentences (and if those sentences do not contain quanti¬ers), then you should
be able to prove ⊥ using just the introduction and elimination rules for =, §,
∨, ¬, and ⊥.
The only time you may arrive at a contradiction but not be able to prove
⊥ using the rules of F is if the inconsistency depends on the meanings of
predicates other than identity. For example, suppose you derived the contra-
diction n < n, or the contradictory pair of sentences Cube(b) and Tet(b). The
rules of F give you no way to get from these sentences to a contradiction of
the form P and ¬P, at least without some further premises.
What this means is that in Fitch, the Ana Con mechanism will let you
introducing ⊥
with Ana Con establish contradictions that can™t be derived in F . Of course, the Ana Con
mechanism only understands predicates in the blocks language (and even
there, it excludes Adjoins and Between). But it will allow you to derive ⊥
from, for example, the two sentences Cube(b) and Tet(b). You can either do
this directly, by entering ⊥ and citing the two sentences, or indirectly, by
using Ana Con to prove, say, ¬Cube(b) from Tet(b).

Chapter 6
Negation rules / 159

You try it
1. Open Negation 2 using Fitch. In this ¬le you will ¬nd an incomplete proof.
As premises, we have listed a number of sentences, several groups of which
are contradictory.
2. Focus on each step that contains the ⊥ symbol. You will see that various
sentences are cited in support of the step. Only one of these steps is an
application of the ⊥ Intro rule. Which one? Specify the rule for that step
as ⊥ Intro and check it.
3. Among the remaining steps, you will ¬nd one where the cited sentences
form a tt-contradictory set of sentences. Which one? Change the justi¬-
cation at that step to Taut Con and check the step. Since it checks out,
we assure you that you can derive ⊥ from these same premises using just
the Boolean rules.
4. Of the remaining steps, the supports of two are contradictory in view of the
meaning of the identity symbol =. Which steps? Change the justi¬cation
at those step to FO Con and check the steps. To derive ⊥ from these
premises, you would need the identity rules (in one case = Elim, in the
other = Intro).
5. Verify that the remaining steps cannot be justi¬ed by any of the rules ⊥
Intro, Taut Con or FO Con. Change the justi¬cation at those steps to
Ana Con and check the steps.
6. Save your proof as Proof Negation 2. (Needless to say, this is a formal proof
of inconsistency with a vengeance!)
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

⊥ Elimination

As we remarked earlier, if in a proof, or more importantly in some subproof,
you are able to establish a contradiction, then you are entitled to assert any
fol sentence P whatsoever. In our formal system, this is modeled by the rule
of ⊥ Elimination (⊥ Elim).
⊥ Elimination (⊥ Elim):


Section 6.3
160 / Formal Proofs and Boolean Logic

The following You try it section illustrates both of the ⊥ rules. Be sure
to go through it, as it presents a proof tactic you will have several occasions
to use.

You try it

1. It often happens in giving proofs using ∨ Elim that one really wants
to eliminate one or more of the disjuncts, because they contradict other
assumptions. The form of the ∨ Elim rule does not permit this, though.
The proof we will construct here shows how to get around this di¬culty.

2. Using Fitch, open the ¬le Negation 3. We will use ∨ Elim and the two ⊥
rules to prove P from the premises P ∨ Q and ¬Q.

3. Start two subproofs, the ¬rst with assumption P, the second with assump-
tion Q. Our goal is to establish P in both subproofs.

4. In the ¬rst subproof, we can simply use reiteration to repeat the assump-
tion P.

5. In the second subproof, how will we establish P? In an informal proof,
we would simply eliminate this case, because the assumption contradicts
one of the premises. In a formal proof, though, we must establish our goal
sentence P in both subproofs, and this is where ⊥ Elim is useful. First use
⊥ Intro to show that this case is contradictory. You will cite the assumed
sentence Q and the second premise ¬Q. Once you have ⊥ as the second
step of this subproof, use ⊥ Elim to establish P in this subproof.

6. Since you now have P in both subproofs, you can ¬nish the proof using ∨
Elim. Complete the proof.

7. Save your proof as Proof Negation 3.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
It turns out that we do not really need the rule of ⊥ Elim. You can prove
any sentence from a contradiction without it; it just takes longer. Suppose, for
example, that you have established a contradiction at step 17 of some proof.
Here is how you can introduce P at step 21 without using ⊥ Elim.

Chapter 6
Negation rules / 161

17. ⊥
18. ¬P
19. ⊥ Reit: 17
20. ¬¬P ¬ Intro: 18“19
21. P ¬ Elim: 20

Still, we include ⊥ Elim to make our proofs shorter and more natural.

Default and generous uses of the ¬ rules

The rule of ¬ Elim allows you to take o¬ two negation signs from the front of
a sentence. Repeated uses of this rule would allow you to remove four, six, or
indeed any even number of negation signs. For this reason, the implementation
of ¬ Elim in Fitch allows you to remove any even number of negation signs
in one step.
Both of the negation rules have default applications. In a default application default uses of
negation rules
of ¬ Elim, Fitch will remove as many negation signs as possible from the front
of the cited sentences (the number must be even, of course) and insert the
resulting sentence at the ¬ Elim step. In a default application of ¬ Intro,
the inserted sentence will be the negation of the assumption step of the cited

You try it
1. Open the ¬le Negation 4. First look at the goal to see what sentence we
are trying to prove. Then focus on each step in succession and check the
step. Before moving to the next step, make sure you understand why the
step checks out and, more important, why we are doing what we are doing
at that step. At the empty steps, try to predict which sentence Fitch will
provide as a default before you check the step.
2. When you are done, make sure you understand the completed proof. Save
your ¬le as Proof Negation 4.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations


6.7 If you skipped any of the You try it sections, go back and do them now. Submit the ¬les
‚ Proof Negation 1, Proof Negation 2, Proof Negation 3, and Proof Negation 4.

Section 6.3
162 / Formal Proofs and Boolean Logic

6.8 (Substitution) In informal proofs, we allow you to substitute logically equivalent sentences


. 30
( 107 .)