I have to semantically prove that for any closed formulas $Φ$ and $ψ$ from $ψ\models Φ$ and $\negψ\models Φ$ always follows $\modelsΦ$.
I would try to prove this in the following way, but I am not sure if it is a formally correct proof. That's why I would like to get feedback for it.
Let $I$ be any interpretation so that $ψ\models Φ$ and $\negψ\models Φ$ holds. Assume that $\not\models$ $Φ$.
We now distinguish between two cases.
- If $I\models ψ$ then $I\models Φ$ must hold because of $ψ\models Φ$. However, this is a contradiction to our assumption that $\not\models$ $Φ$.
- If $I\not\models ψ$, i.e. $I\models \negψ$, then $I\models Φ$ must hold because of $\negψ\models Φ$. However, this is a contradiction to our assumption that $\not\models$ $Φ$.
We have now a contradiction for both cases. That means that our assumption is wrong and $\models Φ$ must hold for any interpretation.
This works, but it would be simpler to phrase it as a direct proof: suppose $\mathcal{A}$ is an arbitrary interpretation. Now one of two things happens: either $\mathcal{A}\models\psi$, in which case $\mathcal{A}\models\Phi$ since $\psi\models\Phi$, or $\mathcal{A}\models\neg\psi$, in which case $\mathcal{A}\models\Phi$ since $\neg\psi\models\Phi$. Either way, we have $\mathcal{A}\models\Phi$. In other words, $\Phi$ is true in every interpretation, which is what we wanted to show.
This is the same proof you've written, but with an unnecessary contradiction removed.