Proposition 56: Iterated conjunction introduction (inference rule)

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

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

Base cases: Suppose that the statements \alpha , \beta and \gamma hold. Using conjunction introduction, the conjunction (\alpha \wedge \beta) holds. By the same rule, \big( (\alpha \wedge \beta) \wedge \gamma \big) then holds. But (\alpha \wedge \beta \wedge \gamma) is short for precisely this statement.

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