Proposition 96: Associativity of disjunction (inference rule)

(a) Given that the disjunction (\phi \vee \psi) \vee \xi holds, we may infer \phi \vee (\psi \vee \xi) holds: \cfrac{\vdash \big( (\phi \vee \psi) \vee \xi \big)}{\vdash \big( \phi \vee (\psi \vee \xi) \big)}. (b) Given that \phi \vee (\psi \vee \xi) holds, we may infer that (\phi \vee \psi) \vee \xi holds: \cfrac{\vdash \big( \phi \vee (\psi \vee \xi) \big)}{\vdash \big( (\phi \vee \psi) \vee \xi) \big)}.

Proof: (a): First, assume \phi . By disjunction introduction, part (a), we may infer that \phi \vee (\psi \vee \xi) holds. We have thus showed \phi entails this disjunction.

Next, assume \psi . By part (a) of disjunction introduction, we infer \psi \vee \xi holds. Using part (b) of disjunction introduction, we infer that \phi \vee (\psi \vee \xi) holds. We have now showed that \psi entails the latter disjunction.

For the next step, assume \phi \vee \psi . Using this assumption and the entailments found above as premises for the disjunction elimination rule, we infer that \phi \vee (\psi \vee \xi) holds. Therefore, we conclude that \phi \vee \psi entails \phi \vee (\psi \vee \xi) .

Last, assume \xi . Using disjunction introduction part (a) and then (b), we infer that \phi \vee (\psi \vee \xi) holds. Therefore, \xi entails this disjunction. By disjunction elimination, using our original premise, we infer that \phi \vee (\psi \vee \xi) holds.

(b): We proceed similarly to above. Using disjunction introduction parts (a) and (b), we note that each of \psi and \xi entail (\phi \vee \psi) \vee \xi ; by disjunction elimination we thus get that \psi \vee \xi entails (\phi \vee \psi) \vee \xi . Further, we find that \phi entails this last disjunction, and so by using disjunction elimination and our original premise we conclude (\phi \vee \psi) \vee \xi holds. \square