Next: Quantifier reasoning
Up: Proof semantics
Previous: Proofs by contradiction
  Contents
Conclusion-annotated proofs
Sometimes a proof can be made more readable if
we explicitly state at the outset what the intended
conclusion is. This is a common idiom in mathematical
reasoning, whereby authors will often say
``We now derive
as follows:
''
In NDL we can declare the purported conclusion
of the proof with the BY keyword. Specifically,
a deduction of the form
BY
``promises''
that
will derive
. An error occurs if we
evaluate
and obtain some other conclusion
instead. The formal semantics of such deductions
are simple:
For instance, an alternative--and perhaps slightly more
readable--way to express the previous example is the following:
assume A
suppose-absurd ~A
false BY absurd A, ~ A
2004-08-04