Proposition 75: Implication chain introduction (inference rule)

Given statements \alpha, \beta, ... \omega such that each but the last statement entails the statement which is listed to its right, we may infer that the implication chain (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \omega) holds: \cfrac{\alpha \vdash \beta \quad \beta \vdash \cdots \quad \cdots \quad \cdots \vdash \omega}{\vdash (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \omega)}.

Proof: We use structural induction over the definition of implication chains.

Base cases: Suppose we have statements \alpha , \beta and \gamma such that \alpha \vdash \beta, \hspace{3mm} \textup{and}\hspace{3mm} \beta \vdash \gamma. Using conditional introduction twice, the implications (\alpha \Rightarrow \beta) and (\beta \Rightarrow \gamma) hold. But then, by conjunction introduction, the conjunction \big( (\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \gamma) \big) holds, for which (\alpha \Rightarrow \beta \Rightarrow \gamma) is shorhand.

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 . By the induction hypothesis, (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi) holds. By conditional introduction, (\psi \Rightarrow \omega) also holds. Using conjunction introduction, we conclude that \Big( (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi) \wedge (\psi \Rightarrow \omega) holds, for which (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi \Rightarrow \omega) is shorthand. \square