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

next up previous contents
Next: Quantifier reasoning Up: Proof semantics Previous: Proofs by contradiction   Contents
2004-08-06