How to check the validity of formula in first-order logic?

62 Views Asked by At

I have the following formula in FO first order predicate logic. It is given that g is a univariate and f a bivariate function symbol and I'm trying to figure out if the formula is valid or not.

$$ {\forall x \forall y ((f(x,y) = f(y,x)\wedge \sim \forall z f(f(x,y),z) = f(x,f(y,z))), \exists x \forall y \ g(y)=x} $$

I assume $ f(x,y) = f(y,x)$ means that the formula requires f to be symmetric. Also $f((f(x,y),z) = f(x,f(y,z)) $ is basically the associativity equation and the last condition $ \exists x \forall y \ g(y)=x$ means that g must be surjective, if I'm correct. That's how far I've gotten so far. I'm not sure what to do from here.

I'm a little confused. It there is anybody who could help, I'd be grateful. Thanks in advance