next up previous contents
Next: Conclusion-annotated proofs Up: Proof semantics Previous: Conditional proofs   Contents


Proofs by contradiction

A common indirect technique for proving a statement $F$ is to reason by contradiction: we assume that $F$ does not hold and proceed to show that this is an absurd hypothesis, in that it allows us to derive a contradiction. NDL models such reasoning with proofs of the form suppose-absurd $F$ $D$. To evaluate such a proof in an assumption base $\beta$, we add the hypothesis $F$ to $\beta$ and proceed to evaluate the body $D$ in $\mbox{$\beta$}\cup \{F\}$. If that produces the contradiction false, then we return $\mbox{\tt\symbol{126}}\,F$ as the conclusion:
$\;\;$ $\mbox{$\beta$}\cup \{F\} \mbox{$\:\vdash\:$}D \mbox{$\:\longrightarrow\;$}\mbox{\tt false}$$\;$  
  $\;\:$
$\;\;$ $\mbox{$\beta$}\mbox{$\:\vdash\:$}\mbox{\tt suppose-absurd } \, F \;\, D \mbox{$\:\longrightarrow\;$}\mbox{\tt\symbol{126}}\,F$$\;$  
Note that false can be derived if the assumption base contains two formulas of the form $F$ and $\mbox{\tt\symbol{126}}\,F$: we can then apply the rule absurd to these two formulas and derive false (recall the semantics of absurd from Section 1.8.2). As a simple example, here is a proof of A ==>   A:
assume A
  suppose-absurd ~A
    absurd A, ~ A

next up previous contents
Next: Conclusion-annotated proofs Up: Proof semantics Previous: Conditional proofs   Contents
2004-08-04