We consider the language ${\cal L}=\{\in\}$ with an arbitrary set of variables $V$. 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 following 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\mathbb{N}\to W\oplus\mathbb{N}$ is the extension defined by $\bar{\sigma}(n)=n$ for all $n\in\mathbb{N}$ and ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathbb{N})$ is the operation replacing all bound variables of a formula by elements of the copy of $\mathbb{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\mathbb{N}:[k/x]\mbox{ avoids capture in }{\cal M}(\phi_{1})\}$
A substitution theorem is a result of the form:
Theorem (Substitution Theorem): $\Gamma\vdash\phi\ \Rightarrow\ \sigma(\Gamma)\vdash\sigma(\phi)$
for all $\sigma:{\bf P}(V)\to{\bf P}(W)$ satisfying [hypothesis here]
I can show the substitution theorem is true for essential substitutions $\sigma:{\bf P}(V)\to{\bf P}(W)$. I also believe it is true for naive variable substitutions $\sigma:{\bf P}(V)\to{\bf P}(W)$ which avoid capture on $\phi$ and every element of $\Gamma$, provided $|W|$ is an infinite cardinal or $|V|\leq|W|$ (this is because essential substitutions can be shown to exist when these conditions on cardinals are met). This leads to my question:
Question: Is the substitution theorem true for naive variable substitutions which avoid capture in the case when $W$ is a finite set smaller than $V$.
I have the feeling (or hope) it should be true, but there may be a simple argument showing my hopes are vain. The difficulty is that a sequent $\Gamma\vdash\phi$ does not say anything about the axioms potentially being used in the underlying proof. So even though $\sigma$ could avoid capture on $\phi$ and the elements of $\Gamma$, there is no guarantee it will avoid capture on the axioms. So I cannot hope to translate a proof from the larger space into the smaller space. This is the limitation I think of the Hilbert-style deduction system where we have no control on the complexity of proofs (but of course the experts already know that, I am simply learning the hard way). I am hoping a careful study of Gentzen $\bf LK$-system will allow me to have a better control on proofs once we show that cut elimination can hold in this setting. Comments or suggestions are very welcome.
