How to show conservative extension without resorting to model theory?

Question

Let $A$ be a set of wffs of first order logic, let $\varphi$ be a wff of first order logic, and let $a$ be a variable that is distinct from $a$ and that does not occur in any formula in $A\cup\{\varphi\}$. Suppose $A\vdash\exists x\varphi$ in the sequent calculus. Define $A' := A \cup \big\{\varphi[a/x]\big\}$. How can it be shown, without resorting to model theory, that every wff that is provable from $A'$ and in which $a$ doesn't occur is provable from $A$?

Answer 1

If $A$ is finite, an even stronger result can be shown: that every wff that is provable from $A'$, even if it involves the variable $a$, is provable from $A$.

Let $\psi$ be a wff that is provable from $A'$. Choose any proof $P^1_1; P^1_2; \dots; P^1_m$ of $A\vdash\exists x\varphi$, and choose any proof $P^2_1; \dots; P^2_n$ of $A'\vdash \psi$.

Then $$ P^1_1; \dots; \underbrace{A\vdash\exists x\varphi}_{P^1_m}; P^2_1; P^2_2; \dots; \underbrace{A,\varphi[a/x]\vdash\psi}_{P^2_n}; A,\exists x\varphi\vdash\psi; A\vdash\psi $$ is a proof of $\psi$ from $A$, where the penultimate step is the conclusion of the rule $(\exists L)$ with the premise $P^2_n$, and the last step is the conclusion of the rule $(\text{Cut})$ with premises $P^1_m$ and $(A,\exists x\varphi\vdash\psi)$.

Remarks

1. For the list of inference rules of the sequent calculus, see here.
2. Note that the converse is also true, i.e., assuming $A$ is finite, every wff that is provable from $A$, is provable from $A'$. Indeed, let $\psi$ be a wff that is provable from $A$. Choose some proof $P_1; P_2; \dots; P_n$ of $A\vdash\psi$. Then $P_1; P_2; \dots; P_n; A'\vdash\psi$ is a proof of $\psi$ from $A'$, where the last step is a conclusion of the rule $(WL)$ with premis $P_n$. This shows that, if $A$ is finite, the wffs that are provable from $A$ are the same wffs that are provable from $A'$.
3. Suppose $A$ is not finite. If the meaning of $A\vdash\psi$ is that there exists a finite subset $B$ of $A$ such that $B\vdash\psi$, then we have shown that the wffs that are provable from $A$ are the same wffs that are provable from $A'$.