I'm stuck on proving the following: $$ \forall x(\phi \lor \psi) \vdash \forall x\phi \lor \psi $$ Here, $x$ is not free in $\psi$ but can be free in $\phi$. My proof starts like the following:
- $\forall x(\phi \lor \psi)$ (premise)
- $\phi[x_0/x] \lor \psi$
- $\psi$ (assumption)
- $\forall x\phi \lor \psi$ (or-introduction)
- $\phi[x_0/x]$ (assumption)
And then I'm stuck. In the proof it is like the or-context is in conflict with the $x_0$-context.
Brams28's answer looks correct. But I don't understand why there can't be a simpler proof. The analoguous sequent in propositional logic is just $(p_1 \lor q) \land (p_2 \lor q) \vdash (p_1 \land p_2) \lor q$ which is easily solvable without contradictions.