# Proving validity/invalidity of a modal argument

□(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?

• Truth Trees/Semantic Tableux are a popular choice. If that's not your bag, then there are other options. Another option is the style of proof used in metalogic, which proves things via an examination of the valuation function (if you're unfamiliar, think "maths proof"). Basically, you have options, so I'd recommend doing a bit of research and trying out some options to see what fits :) Sep 29, 2021 at 8:39
• You cannot prove invalidity by formal rules, you generally cannot prove in a formal system that some statement is unprovable (and undisprovable) in it. Such claims only make sense in meta theory. For modal logic that is semantics of possible worlds. So what you need is a counterexample, a set of possible worlds with at least one world where both students and non-students exist. Evaluated over such a set your premise is true but conclusion is false, hence the inference is invalid. Sep 29, 2021 at 11:54
• The formula is not valid. Use Possible Worlds Semantics for Modal Logic to manufacture a counter-example. Intuitively □(A v B) holds in w iff (A v B) is true in every possible world. Thus we may imagine a world w' where A holds (but not B) and a world w'' where B holds (but not A). By truth table for disjunction, formula (A v B) holds in both worlds. But this mean that neither □A holds (because in w'' the formula A does not hold), nor □B (for the same reason). Sep 30, 2021 at 13:41