It's my first time doing predicate logic and I don't even know where to start. I know that $(\forall x)$ means for all X, whereas $(\exists x)$ means that some x exists, however I'm not sure what to even do for this proof.
I know the metatheorems for specialized and weak generalization, and I think weak leibniz might be useful here?
Metatheorems: $(\forall x)A\vdash A$ and if we have $\Gamma\vdash A$, we will also have $\Gamma\vdash(\forall x)A$.
To begin, I think the first step would be to remove inferences, as they are notoriously difficult to work with for Leibniz rule:
$\vdash \neg (\forall x) (\neg A\lor B) \lor (\neg(\exists x) \neg A\lor (\exists x) B)$
My next step would be to move $\neg(\forall x)(\neg A\lor B)$ to the assumptions side, making it:
$\neg (\forall x) (\neg A\lor B) \vdash (\neg (\exists x) \neg A \lor (\exists x) B)$
I'm not sure if this is looking right so far, as I am applying first order logic as that's what I know, with the limited examples I have for predicate logic. How do I even go about changing things here? I know I can temporarily remove the $(\exists x)$'s using gen, then readd them later, and vice versa.
Here are some of the rules we may use: Axioms Axioms 2 and Rules
