# Mathematical logic problem: syntax and semantics relation

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.

• Not clear... Assume that $Γ , ϕ[y/x] ⊨ ψ$; by completeness we have : $Γ , ϕ[y/x] ⊢ ψ$ and thus (by hypothesis) : $Γ,∃xϕ ⊢ ψ$. Thus, by soundness : $Γ,∃xϕ ⊨ ψ$. But it seems quite pointless... What is the context of the problem ? – Mauro ALLEGRANZA May 14 '18 at 7:27
• Mauro, this was the first solution that I thought of. However, it does seem pointless, so I got a little insecure with this answer. This is everything that the problem says, it's a homework list covering chapters 3 and 4 from Ebbinghaus' book. Anyway, that must be the answer, thank you for your attention. – Lucas Lavoyer May 14 '18 at 9:12
• Maybe 5.1 (b) page 68 ? In this case, you have to show the correcteness of the rule. If so, mimick the proof of 4.1 page 66. – Mauro ALLEGRANZA May 14 '18 at 9:47

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 ψ$.

• Thank you, Mauro! Great explanation. – Lucas Lavoyer May 14 '18 at 12:41