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

⊥

.

.

.

P

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

subproof.

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

Exercises

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