How do I prove $\vDash \ (\forall x \varphi \rightarrow \psi)\leftrightarrow \exists x (\varphi \rightarrow \psi)$ with $x$ not free in $\psi$?

Question

I need to prove the following statement:

$$\vDash \ (\forall x \varphi \rightarrow \psi)\leftrightarrow \exists x (\varphi \rightarrow \psi)$$ if $x$ is not a free variable of $\psi$.

I would normally write what I have tried, but this is the first time I encountered this problem and I'm absolutely clueless about where and how to begin, and I believe it would help me to see an actually example of how a proof of a statement like that should be done in order to progress further in the subject. Thank you in advance!

EDIT: Is it an approach like this valid? ($\sim$ denotes logical equivalence) \begin{align*} (\forall x \varphi \rightarrow \psi)\leftrightarrow \exists x (\varphi \rightarrow \psi) & \sim \neg (\forall x \varphi) \vee \psi) \leftrightarrow \exists x(\varphi \rightarrow \psi)\\ & \sim (\exists x \neg \varphi) \vee \psi \leftrightarrow \exists x (\neg \varphi \vee \psi)\\ & \sim \exists x (\neg \varphi \vee \psi) \leftrightarrow \exists x (\neg \varphi \vee \psi)\\ &\sim \top \end{align*}

Answer 1

You approach is good, but the crucial step is showing that

$$(\exists x \neg \varphi) \vee \psi \sim \exists x (\neg \varphi \vee \psi)$$

Now, as it turns out, the existential distributes over disjunction, so you have in general that:

$$\exists x (\varphi \lor \psi) \sim \exists x \ \varphi \lor \exists x \ \psi$$

Moreover, if $\psi$ does not contain $x$ as a free variable, we have as a general Null Quantification principle:

$$\exists x \ \psi \sim \psi$$

So if you have these two principles as given to you:

$$(\exists x \neg \varphi) \vee \psi \sim \text{(Null Quantification)}$$

$$\exists x \ \neg \varphi \lor \exists x \ \psi \sim \text{(Distribution existential over disjunction)}$$

$$\exists x \ (\neg \varphi \lor \psi)$$

Another possibility is that you are given a bunch of Prenex Laws, which one can use to bring quantifiers from inside a statement to the outside. The relevant Prenex Law in this case would be:

$$\exists x \ \varphi \lor \psi \sim \exists x( \varphi \lor \psi)$$

Which is almost exactly what you want:

$$\exists x \ \neg \varphi \lor \psi \sim \exists x( \neg \varphi \lor \psi) \text{(Prenex Law)}$$

Now, if you don't have any of these equivalences available to you, then you need to prove these principles some other way, but how? Well, can use formal semantics to show these, but here is a more intuitive way to understand these equivalences: An existential can be seen as kind of disjunction, that is, if $a,b,c,...$ denote the objects in your domain, then you can think of an existential like this:

$$\exists x \: \varphi(x) \approx \varphi(a) \lor \varphi(b) \lor \varphi(c) \lor ...$$

I use $\approx$ since this is technically not a logical equivalence, and again you can use formal semantics to make this hard, but what you would be doing there does follow the basic idea below, so let's just leave it more informal.

OK, so with this 'equivalence', we can show (or at least informally understand) an equivalence like $$\exists x \: (\varphi(x) \lor \psi(x)) \Leftrightarrow \exists x \ \varphi(x) \lor \exists x \ \psi(x)$$ as follows:

$$\exists x (\varphi(x) \lor \psi(x)) \approx$$

$$(\varphi(a) \lor \psi(a)) \lor (\varphi(b) \lor \psi(b)) \lor (\varphi(c) \lor \psi(c)) \lor ... \sim \text{(by Association and Commutation we can reorder)}$$

$$(\varphi(a) \lor \varphi(b) \lor \varphi(c) ...) \lor (\psi(a) \lor \psi(b) \lor \psi(c) ...) \approx$$

$$\exists x \varphi(x) \lor \exists x \psi(x)$$

We can also show the Prenex Law, i.e. with $\psi$ not containing $x$ as a free variable:

$$\exists x (\varphi(x) \lor \psi) \approx$$

$$(\varphi(a) \lor \psi) \lor (\varphi(b) \lor \psi) \lor (\varphi(c) \lor \psi) \lor ... \sim \text{(by Association and Commutation we can reorder)}$$

$$(\varphi(a) \lor \varphi(b) \lor \varphi(c) ...) \lor (\psi \lor \psi \lor \psi ...) \sim \text{(Idempotence)}$$

$$(\varphi(a) \lor \varphi(b) \lor \varphi(c) ...) \lor \psi \approx$$

$$\exists x \varphi(x) \lor \psi$$