Mathematical logic problem: syntax and semantics relation

Question

Suppose that $\Gamma$, $\phi[y/x] \vdash \psi \implies \Gamma, \exists x \phi \vdash \psi $, where y doesn't occur freely on $\Gamma \cup \{\exists x \phi, \psi\}$. Prove that:

$\displaystyle \Gamma$, $\phi[y/x] \models \psi \implies \Gamma, \exists x \phi \models \psi $.

I'm struggling with this exercise and would appreciate some help. I've tried to think of a solution using the Correcteness Theorem, but it doesn't seem to work.

Thank you.

Answer 1

I assume that the problem refers to :

• Heinz-Dieter Ebbinghaus & Jörg Flum & Wolfgang Thomas, Mathematical logic, Springer (2nd ed, 1994), page 68.

We have to prove the correctness of the rule, i.e. we have to prove that :

if $Γ, ϕ[y/x] \vDash ψ$, then $Γ,∃xϕ ⊨ ψ$, provided that $x$ is not free in $\Gamma,ψ$.

Assume that $\mathfrak I \vDash Γ$ and $\mathfrak I \vDash∃xϕ$ for some interpretation $\mathfrak I$.

According to the definition [page 33], $\mathfrak I \vDash∃xϕ$ means : $\mathfrak I [a/x] \vDash ϕ$, for some $a \in A$.

But $x$ is not free in $\Gamma$; thus, from $\mathfrak I \vDash Γ$ we have also $\mathfrak I [a/x] \vDash Γ$ (because $\mathfrak I$ and $\mathfrak I [a/x]$ agree on every variables/constants except for $x$).

Due to : $Γ, ϕ[y/x] \vDash ψ$, we have also : $\mathfrak I [a/x] \vDash ψ$.

But $x$ is not free in $ψ$ and thus :

$\mathfrak I \vDash ψ$.