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 \bgroup\color{red}$F_1 \Rightarrow F_2$\egroup, they add the hypothesis \bgroup\color{red}$F_1$\egroup to the set of their current working assumptions \bgroup\color{red}$\beta$\egroup, and proceed to derive the desired conclusion \bgroup\color{red}$F_2$\egroup. When the derivation of \bgroup\color{red}$F_2$\egroup is complete, \bgroup\color{red}$F_1$\egroup 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 \bgroup\color{red}$F_1$\egroup.'' Rather, the scope of the hypothesis \bgroup\color{red}$F_1$\egroup is lexically apparent 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 \bgroup\color{red}$F$\egroup \bgroup\color{red}$D$\egroup. To evaluate such a proof in an assumption base \bgroup\color{red}$\beta$\egroup, we add the hypothesis \bgroup\color{red}$F$\egroup to \bgroup\color{red}$\beta$\egroup and proceed to evaluate the body \bgroup\color{red}$D$\egroup in the augmented assumption base \bgroup\color{red}$\mbox{$\beta$}\cup \{F\}$\egroup. Once we obtain a conclusion \bgroup\color{red}$G$\egroup, we return the implication \bgroup\color{red}$F \; \mbox{\tt ==>}\; G$\egroup as the final result:
\bgroup\color{red}$\;\;$\egroup \bgroup\color{red}$\mbox{$\beta$}\cup \{F\} \mbox{$\:\vdash\:$}D \mbox{$\:\longrightarrow\;$}G$\egroup \bgroup\color{red}$\;$\egroup
\bgroup\color{red}$\;\:$\egroup
\bgroup\color{red}$\;\;$\egroup \bgroup\color{red}$\mbox{$\beta$}\mbox{$\:\vdash\:$}\mbox{\tt assume } \, F \;\, D \mbox{$\:\longrightarrow\;$}F \;\mbox{\tt ==>}\;G$\egroup \bgroup\color{red}$\;$\egroup
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-06