Proposition 98: Implication chain elimination (inference rule)

Given that \alpha holds and the implication chain (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \omega) holds, we may infer that \omega holds: \cfrac{\vdash \alpha \quad \vdash (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \omega)}{\vdash \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 holds and (\alpha \Rightarrow \beta \Rightarrow \gamma) holds. This latter statement is shorthand for the conjunction \big( (\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \gamma) \big). Using conjunction elimination, we infer that the implication (\alpha \Rightarrow \beta) holds. By conditional elimination, this means \beta holds. But then, because (\beta \Rightarrow \gamma) also holds using conjunction elimination, we get by conditional elimination again that \gamma holds.

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 . The implication chain (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi \Rightarrow \omega), which holds as one of our premises (the other premise being that \alpha holds), is shorthand for \big( (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi) \wedge (\psi \Rightarrow \omega) \big). Conjunction elimination tells us (\alpha \Rightarrow \beta \Rightarrow \cdots \Rightarrow \psi) and (\psi \Rightarrow \omega) both hold. By the induction hypothesis, we get using the first of these that \psi holds. But by the latter implication, together with conditional elimination, we then can infer that \omega holds. \square