I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. I assume that $\Gamma\subseteq{\bf P}(V)$ is a consistent subset, namely that the sequent $\Gamma\vdash\bot$ is false in relation to some Hilbert-style deductive system. I am trying to establish that $i(\Gamma)$ is itself consistent. When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.

EDIT: Following Andreas' answer, I realize no-one can really answer this question unless I spell out the details of a specific deductive system. This is all the more important as when dealing with a finite set $V$, it is very easy to spell out specialization axioms of the form $\forall x\phi_{1}\to\phi_{1}[y/x]$ with some caveats on variable capture which will effectively exclude many reasonable (valid) formulas which will not even be theorems (I discuss this point more fully in the post Axiomatization of first order logic (finitely many variables). When that happens, Gödel's completeness theorem will fail and we shall have cases of consistent subsets $\Gamma\subseteq{\bf P}(V)$ for $V$ finite which are no longer consistent when embedded into a larger ${\bf P}(W)$. For example, when $V=\{x,y\}$ with $x\neq y$, it is very easy to spell out an axiomatization on ${\bf P}(V)$ whereby the formula $\forall x\forall y(x\in y)\to\forall x(y\in x)$ is not regarded as a legitimate instance of a specialization scheme, and is therefore excluded as an axiom without there being any way to make it a theorem. So $\Gamma=\{ [\forall x\forall y(x\in y)\to\forall x(y\in x)]\to\bot\}$ will be consistent in ${\bf P}(V)$ but not in ${\bf P}(W)$ where $W=\{x,y,z\}$ with $x,y,z$ distinct. So here we go:

Axioms:

(i) $\phi_{1}\to(\phi_{2}\to\phi_{1})$

(ii) $\phi_{1}\to(\phi_{2}\to\phi_{3})\to[(\phi_{1}\to\phi_{2})\to(\phi_{1}\to\phi_{3})]$

(iii) $[(\phi_{1}\to\bot)\to\bot]\to\phi_{1}$

(iv) $\forall x(\phi_{1}\to\phi_{2})\to(\phi_{1}\to\forall x\phi_{2})\ ,\ x\not\in\mathtt{Fr}(\phi_{1})$

(v) $\forall x\phi_{1}\to\phi_{1}[y/x]\ \ ,\ \ \mbox{$[y/x]:{\bf P}(V)\to{\bf P}(V)$ essential substitution of $y$ in place of $x$}$

Rules of inference :

(i) Modus ponens

(ii) Generalization w.r. to $x\in V$ which do not appear free in any hypothesis

I am not insisting on this particular system, especially as I am not defining essential substitutions of variables (a sketch of such definition may however be found in my other post already referred to). I am very happy for someone to propose something reasonable (hopefully leading to the same set of true sequents $\Gamma\vdash\phi$) where consistent subsets $\Gamma\subseteq{\bf P}(V)$ remain consistent once embedded into a larger ${\bf P}(W)$. This is what we need I think to achieve a complete axiomatization on ${\bf P}(V)$. For those questioning the pertinence of finite variable fragments of FOL (a legitimate concern by all means), I refer them to my 'EDIT' section of the post mentioned above.