Theorem 74: Disjunction elimination (inference rule)

Given that \phi entails \xi , and that \psi entails \xi , and that the disjunction (\phi \vee \psi) holds, we may infer that \xi holds: \cfrac{\phi \vdash \xi \quad \psi \vdash \xi \quad \vdash (\phi \vee \psi)}{\vdash \xi}.

Proof: Assume the negation \neg \xi . Using weakening twice, we get (under the assumption \neg \xi ) that \phi entails \neg \xi and \psi entails \neg \xi . We have as premises that \phi entails \xi and \psi entails \xi , so we get by negation introduction (still with the assumption \neg \xi ) that \neg \phi and \neg \psi hold. This means the conjunction \neg \phi \wedge \neg \psi holds by conjunction introduction; we have showed \neg \xi entails \neg \phi \wedge \neg \psi .

On the other hand, it is a premise that \neg (\neg \phi \wedge \neg \psi) holds, for which \phi \vee \psi is shorthand. By weakening, we infer that \neg \xi entails \neg (\neg \phi \wedge \neg \psi) . Thus, using negation introduction, we can infer that \neg \neg \psi holds. By double negation elimination, we conclude \xi holds. \square