□(A v B) → (□A v □B) ...(1)
This symbolic argument is intuitively invalid. In (1), if we replace B with ~A, then we see that though the antecedent is necessary, the consequent is a contradiction since A and ~A both would be necessary. Saying (1) is valid is equivalent to saying that "it is necessary that either I am a student or I am not a student" implies that "either it is necessary that I'm a student or it's necessary that I'm not a student", which is invalid.
However, apart from deducing its invalidity intuitively, is there any way we can prove it formally? In propositional or quantification logic we use a set of rules such as &-introduction, &-elimination, ~-introduction, etc. What type of inference rules should we use in this case to show that it is invalid?
A similar case is, for example, (□A v □B) → □(A v B) ...(2) or ◇(A v B) ↔ (◇A v ◇B) ...(3) are intuitively valid. But is there any way to prove these formally?
