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$. 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
<a href="http://mathoverflow.net/questions/137843/axiomatization-of-first-order-logic-finitely-many-variables">Axiomatization of first order logic (finitely many variables)</a>. 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.