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.

**LAST EDIT**: I have been stuck on this for a few weeks now. However, I am very hopeful the following strategy will work: first, spell out the details of an **LK** Gentzen type system in this particular setting ($V$ possibly finite, $[y/x]$ essential rather than just avoiding capture) which is equivalent to the Hilbert system. Then for all $i:V\to W$ injective, show the implication $i(\Gamma)\vdash i(\Delta)$ provable without cut $\Rightarrow$ $\Gamma\vdash\Delta$ provable without cut. Finally show that cut elimination holds in this setting. Proofs of the cut elimination theorem (e.g. Takeuti) seem to rely on an infinite supply of variables. However, if I am right about the implication $\Rightarrow$, I can always embed a sequent in a larger space to eliminate cut and bring it back to the smaller space. Comments and suggestions are very welcome.