I need to prove the validity of the formula:
$Q= \forall x \forall y \forall v \ F(x,y,f(x,y),v, g(x,y,v)) \rightarrow \forall x \forall y \exists z \forall v \exists u \ F(x,y,z,v,u)$
I thought the best way to do this is by proving that $\neg Q$ is unsatisfiable and I tried the Tableaux Method but I did not know what I should do with the $f$ and $g$ so I couldn't reach a closed tableau
I would appreciate some pointers or suggestions on how to prove the validity of $Q$ or maybe what I'm doing wrong in the tableau
If I remember my tableaus, you get $\forall x,y,zF(\ldots)$ (the antecedent) and $\neg\forall x,y\exists z\ldots$ (the negation the of consequent).
You should have a rule that allows you to conclude $$¬∃z∀v∃uF(a,b,z,v,u)$$ for some $a,b$. To reduce $¬∃z$ we need something to apply it to. The terms we have lying around are those involving $a,b,f,g$. To line up with the antecedent (which we are trying to contradict) instantiate $f(a,b)$ for $z$. This should get you going.