Conditional Proof

Next Related Topic on Ring

Rule ACP starts an indented sequence of steps. The indentation will terminate with a CP step which produces a line with a conditional main operator. ACP allows you to assume ANY proposition which is helpful.

The assumption will ALWAYS wind up as the antecedent of the CP-line and the last indented line before the CP-step will always become the consequent.

Often this conditional is the conclusion of the argument, so the ACP is used to assume its antecedent.

But no proof can end on an indented line. So, once you start ACP, the consequent rather than the conclusion is sought. Find it, do CP, and then finish deriving the conclusion.

For example:

  1. (A ∨ B) ⊃ C / A ⊃ C
  | 2. A   ACP
  | 3. A∨B   2, add
  | 4. C   1,3 MP
  5. A ⊃ C     2-4 CP

Rule CP makes a line of the form p⊃q where p is the previous undischarged ACP and q is the previous justified line. (If by mistake you start with AIP instead of with ACP, then the computer will change it for you when it executes the CP.)

This is a very helpful rule in many proofs. The conditional which it is used to prove does not have to be the conclusion of the argument! Just pick any conditional which will speed the proof of the conclusion, use ACP to assume its ANTECEDENT, derive its CONSEQUENT, and then use CP.