Note: Some questions in this section ask about likely last lines of an indirect proof.  Indirect proofs end in contradictions.  If there is a one contradiction in a proof, then a contradiction can be found with any formula and its negation.  For, imagine any contradiction, α~α.  By the method we saw in the discussion of explosion in section 3.5, we can simplify the α, add any wff β, simplify the ~α, and then, by DS, conclude β.  By performing this same process with ~β in place of β, we can, starting with any contradiction, derive any other contradiction. 

 

A likely last line of an indirect proof is a contradiction which can be found in the indented sequence without using the method just described for either half of the contradiction.  To find a likely last line, determine which simple formulas and their negations can be derived, without using the method of explosion.