Modal Logic question about provability/ countermodels.
This statement is provable. You can turn it into an equivalent implication: ¬□(□A → B) → □(□B → A)
Then make the hypothesis that the first term is true and show that the second follows.
The first term is equivalent to
◇¬(□A → B)
◇(□A ∧ ¬B)
From which follows that
□A ∧ ◇¬B
Then in any possible world, we have
From which we can trivially show that in this possible world,
□B → A
This is true in any possible world, so we've shown that the second term of the implication follows from the first.