|= (∀xϕ→ψ) ↔ (∃x(ϕ→ψ)), with x not belonging to FV(ψ) (Free Variable).
I have been struggling with this exercise for a while. I have to prove this formula using either the valuations or as shown in this example in Van Dalen's "Logic and Structure" (I do not know the name of this method) with a more verbal(?) approach if you will.
Lemma which is referenced in the book just in case
I know that I have to reach, at some point during the demonstration that ∀x(ϕ→ψ), but I don't understand how to translate it (from one language to the other and back to the formula) correctly in order to do that.
Not sure if this is correct but I got up to that point and I'm not sure how I continue:
Note: I'm using a' to refer to the element from the language and a to refer to the interpretation of a' in that language.
Let FV( (∀xϕ→ψ) ↔ (∃x(ϕ→ψ)) ) = {z1, ..., zk}.
We must prove that for all structure A with an appropriate type:
A |= ∀z1,...zk( (∀xϕ→ψ)(x, z1,...,zk) ↔ (∃x(ϕ→ψ))(x,z1,...zk) )
So we have to show that:
A |= (∀xϕ→ψ)(x, a'1,...,a'k) ↔ (∃x(ϕ→ψ))(x,a'1,...a'k) for arbitrary a'1,..., a'k that belongs to |A|
A |= (∀xϕ→ψ)(x, a'1, ..., a'k) ⇔
A |= for all b that belongs to |A| ϕ(b, a'1, ..., a'k) implies A |= ψ(a'1,...,a'k) ⇔
...
You want to show that $\models (\forall x \ \phi \rightarrow \psi) \leftrightarrow (\exists x \ (\phi \rightarrow \psi))$, with $x \notin \mathrm{FV}(\psi)$.
As you may know, $\models (\forall x \ \phi \rightarrow \psi) \leftrightarrow (\exists x \ (\phi \rightarrow \psi)) \iff \mathfrak{A} \models (\forall x \ \phi \rightarrow \psi) \leftrightarrow (\exists x \ (\phi \rightarrow \psi))$, for every $\mathfrak{A}$ of the appropriate type.
Hence, we may pick an arbitrary $\mathfrak{A}$ so as to demonstrate our property.
Now, by 2.4.5, $\mathfrak{A} \models (\forall x \ \phi \rightarrow \psi) \leftrightarrow (\exists x \ (\phi \rightarrow \psi)) \iff \mathfrak{A} \models \forall x \ \phi \rightarrow \psi \Leftrightarrow \mathfrak{A} \models \exists x \ (\phi \rightarrow \psi)$.
Hence, let us demonstrate the dual implication.
($\implies$) As $x \notin \mathrm{FV}(\psi)$, $\mathfrak{A} \models \forall x \ \phi \rightarrow \psi \iff \mathfrak{A} \models \forall x \ (\phi \rightarrow \psi)$ (I believe this is a previously shown result in the book, but if not it can be easily shown). From here on out you may easily deduce $\mathfrak{A} \models \exists x \ (\phi \rightarrow \psi)$ either via derivation rules of natural deduction or, through 2.4.5, as $\mathfrak{A} \models \forall x \ (\phi \rightarrow \psi) \iff \mathfrak{A} \models \phi(\overline{a}) \rightarrow \psi(\overline{a})$, for every $a \in |\mathfrak{A}| \implies \mathfrak{A} \models \phi(\overline{a}) \rightarrow \psi(\overline{a})$, for some $a \in |\mathfrak{A}| \iff \mathfrak{A} \models \exists x \ (\phi \rightarrow \psi)$.
($\impliedby$) We shall assume to be working with sentences so as to make matters easier, but in the case that $\mathrm{FV}(\psi), \mathrm{FV}(\phi) \setminus \{x\} \neq \emptyset$, just perform a previous quantifier closure and select arbitrary $z_1, \dots, z_k$ from $\mathrm{FV}(\psi) \cup \mathrm{FV}(\phi) \setminus \{x\}$. This implication could be easily obtained via natural deduction, but let us stick to semantics (and hence to 2.4.5).
As $x \notin \mathrm{FV}(\psi)$, there are two cases to consider: (i) $\mathfrak{A} \models \psi$; (ii) $\mathfrak{A} \not \models \psi$.
If (i), the desired result is immediate, as $\mathfrak{A} \models \forall x \ \phi \rightarrow \psi \iff \mathfrak{A} \models \forall x \ \phi \Rightarrow \mathfrak{A} \models \psi$ will be immediately true.
If (ii), we have then that there is some $a \in |\mathfrak{A}|$ such that $\mathfrak{A} \models \phi(\overline{a}) \rightarrow \psi$. As $\mathfrak{A} \not \models \psi$, such can only be if $\mathfrak{A} \not \models \phi(\overline{a})$. Hence, it can be easily shown that $\mathfrak{A} \not \models \forall x \ \phi(x)$ and thus $\mathfrak{A} \models \forall x \ \phi \rightarrow \psi \iff \mathfrak{A} \models \forall x \ \phi \Rightarrow \mathfrak{A} \models \psi$ is vacuously true.
$\square$