next up previous contents
Next: Proofs by contradiction Up: Proof semantics Previous: Composite proofs   Contents


Conditional proofs

When mathematicians want to establish a conditional statement $F_1 \Rightarrow \; F_2$, they add the hypothesis $F_1$ to the set of their current working assumptions $\beta$, and proceed to derive the desired conclusion $F_2$. When the derivation of $F_2$ is complete, $F_1$ ceases to be an active assumption--it is ``discharged''. Note that the discharge is not explicitly made; mathematicians do not say ``and now we discharge $F_1$.'' Rather, the scope of the hypothesis $F_1$ is lexically evident by the division of the proof text into units such as paragraphs. Conditional reasoning as described above is captured in NDL by proofs of the form assume $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 the augmented assumption base $\mbox{$\beta$}\cup \{F\}$. Once we obtain a conclusion $G$, we return the implication $F \; \mbox{\tt ==>}\; G$ as the final result:
$\;\;$ $\mbox{$\beta$}\cup \{F\} \mbox{$\:\vdash\:$}D \mbox{$\:\longrightarrow\;$}G$$\;$  
  $\;\:$
$\;\;$ $\mbox{$\beta$}\mbox{$\:\vdash\:$}\mbox{\tt assume } \, F \;\, D \mbox{$\:\longrightarrow\;$}F \;\mbox{\tt ==>}\;G$$\;$  
As a simple example, here is a proof of A ==> A:
assume A
  claim A

next up previous contents
Next: Proofs by contradiction Up: Proof semantics Previous: Composite proofs   Contents
2004-08-04