Initialization in the tableaux method for first order logic

Question

This I believe is a question that can be answered in a one-line comment, but finals are just around the corner and I want to be sure about everything.

So suppose I want to check the validity of $$\exists x(P(x)\wedge Q(x))\models \exists xP(x)\wedge \exists xQ(x)$$ What I've been doing is to negate the implication of the two, that is $$\neg \left( \exists x(P(x)\wedge Q(x)) \rightarrow \exists xP(x)\wedge \exists xQ(x)\right)$$ and then try to arrive to a contradiction using the rules of the tableaux method. But I've questioned myself whether this is true, that is

$\psi \models \varphi \Leftrightarrow \psi \rightarrow \varphi$?

Thank you in advance.

Answer 1

Technically, it's:

$\psi \models \varphi \Leftrightarrow \vDash \psi \rightarrow \varphi$

But given your proof by Contradiction method, what you really use is:

$\psi \models \varphi \Leftrightarrow \neg (\psi \rightarrow \varphi) \vDash \bot$

But yes, the method you use works just fine!