Indirect Proof

Rule AIP starts an indented sequence of steps which is to lead to a contradiction and then to an IP step. The indentation ends when the IP step is taken.

But no proof can end on an indented line. So, once you start AIP, ANY contradiction is sought (rather than the conclusion). When it is found, do IP and then finish deriving the conclusion.

In the AIP step, you get to assume ANY proposition which is helpful. But, keep in mind that ALL IP STEPS HAVE A ~ MAIN OPERATOR.

If the conclusion ALSO HAS a ~ main operator, assume all of it EXCEPT the ~ MO. Then the conclusion will be the IP step.

BUT, if the conclusion LACKS a ~ MO, the AIP line will have one. Thus the IP line will start ~~ and so the proof will require a concluding use of DN.

Rule IP makes a line which is the denial of the previous undischarged AIP. (If by error you start with ACP instead of with AIP, the computer will change it when doing the IP.) IP requires that the last line which was justified have the form q•~q

This is a very helpful rule which simplifies the strategy for doing many proofs. Just assume the denial of the conclusion by using AIP. Proceed to break up ALL propositions that have •∨⊃≡ operators until only simple propositions and their negations are left. A contradiction will always be found among the leftovers. Then use CONJ to build an instance of q•~q

The IP conclusion ALWAYS has one more ~ than the AIP. So sometimes IP has to be followed by a DN to get rid of the ~~. WARNING: The text examples and answers occasionally combine the IP and the DN into one step. LogicCoach does not allow this. So, it will reject some proofs that the text accepts.

If the Conclusion is already of the form ~C, then