next up previous contents
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 $F$ as follows: $\cdots$'' In NDL we can declare the purported conclusion of the proof with the BY keyword. Specifically, a deduction of the form $F$ BY $D$ ``promises'' that $D$ will derive $F$. An error occurs if we evaluate $D$ and obtain some other conclusion instead. The formal semantics of such deductions are simple:
$\;\;$ $\mbox{$\beta$}\mbox{$\:\vdash\:$}D \mbox{$\:\longrightarrow\;$}F$$\;$  
  $\;\:$
$\;\;$ $\mbox{$\beta$}\mbox{$\:\vdash\:$}\, F \;\, \mbox{\tt BY} \;\,D \mbox{$\:\longrightarrow\;$}F$$\;$  
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