Proposition 92: Iterated disjunction elimination (inference rule)

Given that the iterated disjunction (\alpha \vee \beta \vee \cdots \vee \omega) holds, and that each of the statements \alpha , \beta , …, \omega entail \xi , we may infer that \xi holds: \cfrac{\alpha \vdash \xi \quad \beta \vdash \xi \quad \cdots \quad \omega \vdash \xi \quad \vdash (\alpha \vee \beta \vee \cdots \vee \omega)}{\vdash \xi}.

Proof: We argue using structural induction over the definition of iterated disjunctions.

Base cases: Suppose we have statements \alpha , \beta and \gamma such that (\alpha \vee \beta \vee \gamma) holds, and that each of \alpha , \beta and \gamma entail \xi . Assume the disjunction \alpha \vee \beta . Since \alpha and \beta each entail \xi , we get by disjunction elimination that \xi holds. Thus, we have showed that \alpha \vee \beta entails \xi .

By definition, (\alpha \vee \beta \vee \gamma) is short for (\alpha \vee \beta) \vee \gamma . Using this, that \gamma entails \xi , and the above, we conclude by disjunction elimination that \xi holds.

Inductive step: We take as the induction hypothesis that the desired result is justified for the premise \vdash (\alpha \vee \beta \vee \cdots \vee \psi) together with the entailments \alpha \vdash \xi, \hspace{3mm} \beta \vdash \xi, \hspace{3mm} \cdots \hspace{3mm} \psi \vdash \xi, and want to show it is then also justified given \vdash (\alpha \wedge \beta \wedge \cdots \wedge \psi \wedge \omega) in combination with the entailments \alpha \vdash \xi, \hspace{3mm} \beta \vdash \xi, \hspace{3mm} \cdots \hspace{3mm} \psi \vdash \xi, \hspace{3mm} \omega \vdash \xi. Assume (\alpha \vee \beta \vee \cdots \vee \psi) . By the induction hypothesis, using all but the last of the above list of entailments, we get that \xi holds. Thus, we have showed that (\alpha \vee \beta \vee \cdots \vee \psi) entails \xi . Since \gamma entails \xi , we conclude by means of disjunction elimination that \xi holds. \square