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$. Specifically we define ${\bf P}(V)$ as the free algebra of type $\{\bot,\to\}\cup\{\forall x:x\in V\}$ (with the obvious arity for each symbol) generated by the ordered pairs $(x,y)$, denoted $(x\in y)$, for $x,y\in V$. We consider the Hilbert-style axiomatization on ${\bf P}(V)$:

> **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

An essential substitution $\sigma^{*}:{\bf P}(V)\to{\bf P}(W)$ associated with a map $\sigma:V\to W$ is a map which satisfies the property ${\cal M}\circ\sigma^{*}=\bar{\sigma}\circ{\cal M}$ where $\bar{\sigma}:V\oplus\mathtt{N}\to W\oplus\mathtt{N}$ is the extension defined by $\bar{\sigma}(n)=n$ for all $n\in\mathtt{N}$ and ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathtt{N})$ is the operation replacing all bound variables of a formula by elements of the copy of $\mathtt{N}$ disjoint from $V$, as specified by the following recursion:
     > $(i)\ {\cal M}(x\in y)=(x\in y)$
> $(ii)\ {\cal M}(\bot)=\bot$
> $(iii)\ {\cal M}(\phi_{1}\to\phi_{2})={\cal M}(\phi_{1})\to{\cal M}(\phi_{2})$
>
>$(iv)\ {\cal M}(\forall x\phi_{1})=\forall n{\cal M}(\phi_{1})[n/x]$
>
> where $\ n=\min\{k\in\mathtt{N}:[k/x]\mbox{ avoids capture in }{\cal M}(\phi_{1})\}$

I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. My question is:

> **Question:** is it true that $\Gamma$ consistent $\ \Rightarrow\ $ $i(\Gamma)$ 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' and Noah's answer, I have hopefully made the question clearer.