next up previous
Next: Case Analysis [GS] Up: No Title Previous: Implication [GS]

Assuming the Antecedent [GS]

It is common in mathematics to prove an implication tex2html_wrap_inline581 by assuming the antecedent p and proving the consequent q. By ``assuming the antecedent'' we momentarily think of it as an axiom and thus equivalent to true. The formal justification of this proof technique relies on the Deduction Theorem from mathematical logic.gif

Here is a simple example (from [GS]): Suppose we want to prove tex2html_wrap_inline595 . In the proof we get to assume the conjuncts of the antecedent. We are required to prove a = b:

Proof:

 Ass ume  tex2html_wrap_inline599 

a

= % Assumption of a.

true

= % Assumption of b.

b

Warning: For the proof of tex2html_wrap_inline581 , the Deduction Theorem requires that all variables in the assumed expression, p, be viewed as constants throughout the proof of q, so that you cannot substitute expressions in for the ``variables'' that appear in the assumptions. The following incorrect proof of tex2html_wrap_inline613 (which is not valid) shows why this is necessary. The proof is incorrect because b in the assumption is replaced.

Proof (Incorrect):

 Ass ume  tex2html_wrap_inline617 

d

= % Assumption of (b = c)[d/b], i.e., d = c

c

Notice that the expression in which we are attempting to do the substitution is b = c.



Norman Papernick
Thu Mar 21 14:07:58 EST 1996