Next: Conclusion-annotated proofs
Up: Proof semantics
Previous: Conditional proofs
  Contents
Proofs by contradiction
A common indirect technique for proving a statement
is to reason by contradiction: we assume that
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
. To evaluate such a proof
in an assumption base
, we add the hypothesis
to
and proceed to evaluate the body
in
. If that produces the contradiction false,
then we return
as the conclusion:
Note that false can be derived if the
assumption base contains two formulas of the form
and
: we can then apply the rule
absurd to these two formulas and derive false
(recall the semantics of absurd from Section 1.10.2).
As a simple example, here is a proof of A ==> A:
assume A
suppose-absurd ~A
absurd A, ~A
Next: Conclusion-annotated proofs
Up: Proof semantics
Previous: Conditional proofs
  Contents
2004-08-06