Theorem 58: Disjunction introduction (inference rule)

(a) Given that \phi holds, we may infer that the disjunction (\phi \vee \psi) holds: \cfrac{\vdash \phi}{\vdash (\phi \vee \psi)}. (b) Given that \psi holds, we may infer that the disjunction (\phi \vee \psi) holds: \cfrac{\vdash \psi}{\vdash (\phi \vee\psi)}.

Proof: (a): Using weakening, we may infer that the conjunction of negations \neg \phi \wedge \neg \psi entails \phi . Assume \neg \phi \wedge \neg \psi . By conjunction elimination, we infer \neg \phi holds. Thus we have showed \neg \phi \wedge \neg \psi entails \neg \phi . We infer by negation introduction that \neg (\neg \phi \wedge \neg \psi) holds, for which \phi \vee \psi is short.

(b): Using a very similar argument to the above, showing first that \neg \phi \wedge \neg \psi entails both of \psi and \neg \psi and then using negation introduction, we obtain the desired conclusion. \square