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.

  • $\begingroup$ 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 ? $\endgroup$ – Mauro ALLEGRANZA May 14 '18 at 7:27
  • $\begingroup$ 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. $\endgroup$ – Lucas Lavoyer May 14 '18 at 9:12
  • $\begingroup$ 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. $\endgroup$ – 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 ψ$.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.