# Prove that a disjunction (in first-order logic) does not depend on the order or grouping of its disjuncts

For at least four disjuncts. For example, it should follow immediately that any two disjunctions of seven formulas are equivalent. There are 132 cases to check without this general result.

Prove using axioms, rules of inference, theorems of first-order logic. You may assume that disjunction is commutative and associative.

• The proof must be general, i.e. for $n$ disjuncts whatever and must be by induction, and thus in the meta-theory. Of course, it must rely on the basis cases, i.e. $A \lor B \equiv B \lor A$ and $(A \lor B) \lor C \equiv A \lor (B \lor C)$. – Mauro ALLEGRANZA Apr 23 '18 at 7:24
• The last ones can be axioms of the calculus or tehy are easily derivable from propositional calculus; of courese, the details depend on thechosen axiomatization. – Mauro ALLEGRANZA Apr 23 '18 at 7:25