Proving soundness of sequent calculus rules

Question

Prove the soundness of the following rules of the sequent calculus $LK$ for classical logic: $$\dfrac{\Gamma, A(y) \vdash \Delta}{\Gamma,\exists x A(x) \vdash \Delta}{\exists\mathsf I}$$ $$\dfrac{\Gamma \vdash A(t), \Delta}{\Gamma \vdash \exists x A(x), \Delta}{\exists\mathsf r}$$

(where in $(\exists l) \space y$ is an eigenvariable, i.e. $y \notin \Gamma \cup \Delta$).

Are these rules also invertible?

I know how to proof soundness of $(\forall r)$, where I can say something like this:

Assume $\Gamma \models P_1[y/x], \Delta$. Let $(\mathcal{A}, \xi^{\mathcal{A}})$ such that $(\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma, (\mathcal{A}, \xi^{\mathcal{A}}) \not\models \Delta$ and $(\mathcal{A}, \xi^{\mathcal{A}}) \models P_1[^y /_x]$. Since $y \notin \Gamma, (\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma$ if and only if $\forall b \in D_{\mathcal{A}} \space (\mathcal{A}, \xi^{\mathcal{A}}[^b/_y]) \models \Gamma$. Hence, $\forall b \in D_{\mathcal{A}} \space (\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma$ implies $(\mathcal{A}, \xi^{\mathcal{A}}[^b/_y]) \models P_1[^y/_x]$. Hence, $(\mathcal{A}, \xi^{\mathcal{A}}) \models \forall x P_1$, from which $\Gamma \models \forall x P_1, \Delta$ follows.

But, I'm having trouble in converting this proof to $(\exists l)$ and $(\exists r)$. Please note that $(\mathcal{A}, \xi^{\mathcal{A}})$ is an interpretation for a first order language $\mathcal{L}$, where $\mathcal{A}$ is a structure and $\xi^{\mathcal{A}}$ an environment of $\mathcal{A}$. And $D_{\mathcal{A}}$ is the domain.

EDIT:

For $(\exists l)$:

Assume $\Gamma, P_1[y/x] \models \Delta$. Let $(\mathcal{A}, \xi^{\mathcal{A}})$ such that $(\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma, (\mathcal{A}, \xi^{\mathcal{A}}) \not \models \Delta$ and $(\mathcal{A}, \xi^{\mathcal{A}}) \not \models P_1[^y /_x]$. Since $y \notin \Gamma \cup \Delta, (\mathcal{A}, \xi^{\mathcal{A}}) \not \models \Delta$ if and only if $\exists b \in D_{\mathcal{A}} \space (\mathcal{A}, \xi^{\mathcal{A}}[^b/_y]) \not \models \Delta$. Hence, $\exists b \in D_{\mathcal{A}} \space (\mathcal{A}, \xi^{\mathcal{A}}) \not \models \Delta$ implies $(\mathcal{A}, \xi^{\mathcal{A}}[^b/_y]) \not \models P_1[^y/_x]$. Hence, $(\mathcal{A}, \xi^{\mathcal{A}}) \models \exists x P_1$, from which $\Gamma \models P_1[y/x], \Delta$ follows.

For $(\exists r)$:

Assume $\Gamma \models P_1[t/x], \Delta$. Let $(\mathcal{A}, \xi^{\mathcal{A}})$ such that $(\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma, (\mathcal{A}, \xi^{\mathcal{A}}) \not \models \Delta$ and $(\mathcal{A}, \xi^{\mathcal{A}}) \models P_1[^t /_x]$. Since $(\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma$ if and only if $\exists b \in D_{\mathcal{A}} \space (\mathcal{A}, \xi^{\mathcal{A}}[^b/_x]) \models \Gamma$. Hence, $\exists b \in D_{\mathcal{A}} \space (\mathcal{A}, \xi^{\mathcal{A}}) \models \Gamma$ implies $(\mathcal{A}, \xi^{\mathcal{A}}[^b/_x]) \models P_1[^t/_x]$. Hence, $(\mathcal{A}, \xi^{\mathcal{A}}) \models \exists x P_1$, from which $\Gamma \models \exists x P_1, \Delta$ follows.

Answer 1

Hint

Consider :

$$\dfrac{\Gamma, A(y) \vdash \Delta}{\Gamma,\exists x A(x) \vdash \Delta}{\exists\mathsf l}$$

with the proviso on the eigenvariable $y$ that : $y \notin \Gamma \cup \Delta$.

In order to prove that the rule is sound, we have to prove that if the upper sequent is valid, so is the lower one, where we say that :

a sequent $\Gamma \vdash \Delta$ is valid if it is satisfied in every interpretation, and it is satisfied in the interpretation $\mathfrak F$ iff either some formula in $\Gamma$ is not satisfied by $\mathfrak F$, or some formula in $\Delta$ is satisfied by $\mathfrak F$.

Thus, "discarding" the contexts $\Gamma$ and $\Delta$, we have to show that :

if $A(y)$ is not satisfied, then also $\exists x A(x)$ is.

Due to the fact that $y \notin \Gamma \cup \Delta$, we have no "limitations" on the choice of the interpretation for $y$; thus, if we cannot find a "suitable" object $b$ in the domain $D$ of the interpretation such that $A[b/y]$ holds in $\mathfrak F$ (i.e. $\mathfrak F \nvDash A[b/y]$), then it is impossible to satisfy $\exists x A(x)$ in $\mathfrak F$ (i.e. also $\mathfrak F \nvDash \exists x A(x)$).

---

Basically, the same argument works for $\exists\mathsf r$, assuming the satisfiability of $A(t)$ in $\mathfrak F$.