In the last chapter we began to construct derivations.

So far we've studied and applied the introduction and elimination rules for the three binary connectives, conjunction, disjunction, and the conditional. These rules correspond to patterns of argumentation.

Let’Äôs briefly recall the rules for disjunction.

it is quite obvious that we can infer φ v ψ if we are given a proof of either φ or ψ; these patterns of reasoning give us the introduction rules.

The corresponding elimination rule reflects the standard "argument by cases". We are given a proof of φ v ψ.

If the assumption of φ allows us to prove ρ...

and the assumption of ψ allows us to prove ρ...

then we can infer ρ (without either of these assumptions).

Now it's time to take a look at the rules of inference for our unary connective, negation. Negation plays obviously a crucial role in the classical indirect arguments we examined in the Introduction.

We assume that the square root of 2 is rational, derive a contradiction and can infer logically the irrationality of the square root of 2.

In this chapter, we look not only at the basic introduction and elimination rules for negation, but some useful derived rules as well.

We'll also examine the notion of an indirect proof, and explain why the negation introduction and elimination rules are considered to be indirect.

Finally, we'll present a strategy for finding contradictions to be used in applying the indirect rules.