Proposition 62: Generalized disjunction introduction (inference rule)

Given that the statements \alpha, \beta, ..., \omega hold, we may infer that the generalized disjunction (\alpha \vee \beta \vee \cdots \vee \omega) holds: \cfrac{\vdash \alpha \quad \vdash \beta \quad \cdots \quad \vdash \omega}{\vdash (\alpha \vee \beta \vee \cdots \vee \omega)}.

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

Base cases: Suppose that the statements \alpha , \beta and \gamma hold. From any one of these premises we may infer the disjunction (\alpha \vee \beta) holds, using disjunction introduction. By the same rule, \big( (\alpha \vee \beta) \vee \gamma \big) then holds. But (\alpha \vee \beta \vee \gamma) is short for precisely this statement.

Inductive step: We take as the induction hypothesis that the desired result is evident for statements \alpha, \beta, ..., \psi , and want to show from this hypothesis that it is evident for statements \alpha, \beta, ..., \psi, \omega . But if all of these statements hold then our hypothesis gives us that (\alpha \vee \beta \vee \cdots \vee \psi) holds; disjunction introduction then lets us infer that \big( (\alpha \vee \beta \vee \cdots \vee \psi) \vee \omega) \big) holds. But this statement is abbreviated by (\alpha \vee \beta \vee \cdots \vee \psi \vee \omega) . \square