I know that this sequent is true for classical logic. But is it true in minimal or intuitionistic logic?
What would be a Kripke model that doesn't satisfy the property?
I would appreciate some (as many as possible) Kripke model examples where classically true formulas are false.
I already have one where $\forall x\neg\phi\lor\neg\neg\phi$ is not true:
Here we have $\alpha\nvDash \neg P(a)\lor\neg\neg P(a)$