Standard textbooks in mathematical logic will assume an infinite supply of variables. Their axiomatization of first order logic will typically contain an axiom of the form $\forall x\phi_{1}\to\phi_{1}[y/x]$ with varying qualifications on what the term $y$ is allowed to be, along the lines of '$y$ is free for $x$ in $\phi_{1}$'. When the set of variables $V$ is finite, the standard textbook approach creates a problem: the formula $\forall x\forall y(x\in y)\to\forall x(y\in x)$ with $x\neq y$ is not an axiom. In general, this is hardly a problem as the set of variable $V$ will have a spare variable $z\not\in\{x,y\}$ allowing us to show that $\forall x\forall y(x\in y)\to\forall x(y\in x)$ is in fact a theorem. However, when $V=\{x,y\}$ there doesn't seem to be any way to prove the formula and we are left with a valid formula which cannot be proven. So whenever $V$ is a finite set, we can easily believe that excluding the axiom $\forall x\phi_{1}\to\phi_{1}[y/x]$ simply because $y$ is not free for $x$ in $\phi_{1}$ (without any substitute), will create a situation where a perfectly reasonable formula such as $\forall x\forall y(x\in y)\to\forall x(y\in x)$ which should have been an axiom, will fail to be included while not being a theorem, thereby leading to an incomplete axiomatization. Somehow we need a way to specify all axioms $\forall x\phi_{1}\to\phi_{1}[y/x]$ without leaving anyone out. Because $V$ is a finite set, we cannot hope to define a substitution of variable mapping $[y/x]:{\bf P}(V)\to{\bf P}(V)$ simply by using fresh variables which haven't yet been used. We fundamentally need to re-use variables, while avoiding capture. This I believe is the key issue which needs to be resolved so as to offer a sensible axiomatization of FOL with finitely many variables (but I could be wrong about this). So my question is:
Question 1: Can anyone suggest an axiomatization of FOL with $V$ finite which is known to be sound, complete and in which the deduction theorem holds without qualification on closed formulas?
Question 2: Is there a known reference which deals with this question? (answered by Andres and Francois)
One may assume no constant or function symbol, and a unique binary predicate $\in$ for the purpose of this post.
My personal approach to defining an essential substitution $[y/x]:{\bf P}(V)\to{\bf P}(V)$ is to create a mapping ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathbb{N})$ which effectively replaces every bound variable of its argument by an element of a copy of $\mathbb{N}$ which is disjoint from $V$, while avoiding capture. So for example ${\cal M}(\forall x(x\in y))=\forall\,0(0\in y)$ and ${\cal M}(\forall y\forall x(x\in y))=\forall\,1\forall\,0(0\in 1)$ (the '$y$' has been replaced by $1$ instead of $0$ to avoid capture):
Minimal Transform of formula:
${\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 for}\ {\cal M}(\phi_{1})\ \}$.
Given a map $\sigma:V\to W$, its natural extension $\bar{\sigma}:V\oplus\mathbb{N}\to W\oplus\mathbb{N}$ (defined by $\bar{\sigma}(x)=\sigma(x)$ and $\bar{\sigma}(n)=n$) can act on the formula ${\cal M}(\phi)$ while avoiding capture. So $\bar{\sigma}\circ{\cal M}(\phi)$ is a meaningful formula which is our intended meaning for '$\sigma(\phi)$'. The problem is $\bar{\sigma}\circ{\cal M}(\phi)$ is a formula in ${\bf P}(W\oplus\mathbb{N})$ and not ${\bf P}(W)$. The trick is to show that provided $W$ is an infinite set or has cardinality no less than that of $V$, it is always possible to find a $\psi\in{\bf P}(W)$ such that $\bar{\sigma}\circ{\cal M}(\phi)={\cal M}(\psi)$. This formula $\psi$ is unique modulo $\alpha$-equivalence and is our candidate for $\sigma(\phi)$. I am not claiming to prove anything here, just sketching the ideas of what can be done to define a notion of:
Essential substitution $\sigma:{\bf P}(V)\to{\bf P}(W)$ associated with $\sigma:V\to W$, which is a map satisfying the key equality $\bar{\sigma}\circ{\cal M}={\cal M}\circ\sigma$ and behaves for all intent and purposes as a variable substitution mapping, while avoiding capture at all times. This map is essentially unique and can be re-defined modulo $\alpha$-equivalence while preserving its intended properties.
In the case when $W=V$ and $\sigma=[y/x]$ the existence of an essential substitution $[y/x]:{\bf P}(V)\to{\bf P}(V)$ is guaranteed and we seemingly have the object we need to finally write down specialization axioms:
Specialization scheme:
$\forall x\phi_{1}\to\phi_{1}[y/x]$
where $[y/x]:{\bf P}(V)\to{\bf P}(V)$ is an essential substitution of $y$ in place of $x$.
Going back to the case when $V=\{x,y\}$, $x\neq y$ and $\phi_{1}=\forall y(x\in y)$, taking $\sigma=[y/x]$ we see that $\bar{\sigma}\circ{\cal M}(\phi_{1})=\forall\,0(y\in 0)$ and consequently the only possible value for $\sigma(\phi_{1})$ is $\forall x(y\in x)$ and we can rejoice at the fact that $\forall x\forall y(x\in y)\to\forall x(y\in x)$ has now become an axiom. So:
Question 3: Is anyone familiar with any alternative approach to this question of constructing essential substitution mapping $\sigma:{\bf P}(V)\to{\bf P}(W)$ associated with $\sigma:V\to W$ making a complete axiomatization possible?
This being said, despite having what I think are the right axioms, I still do not know if it can lead to a complete system (but this is already the object of another post Embedding of consistent subset in first order logic (finitely many variables)
EDIT: some of the comments suggest that there is little point in considering finite variable fragments of FOL. After all, a closed formula (which is what we care most about) has only bound variables which are dummy names and do not matter modulo $\alpha$-equivalence. So whether we restrict these dummy names to be part of a finite set, or allow them to be chosen fresh at will, should not make any difference and is purely cosmetic. I completely agree with this of course and I am not suggesting there is anything interesting to be gained by seeing distinctions between dummy names. I perfectly accept that the interesting entities are congruence classes modulo $\alpha$-equivalence. but the fact remains: every formula of FOL needs a minimal number of variables to be expressed modulo $\alpha$-equivalence. The free algebra ${\bf P}(3)$ is the set of set theory statements which can be expressed with $3$ variables or less. There is a fundamental difference between ${\bf P}(0)$, ${\bf P}(1)$, ${\bf P}(2)$, ${\bf P}(3)$ and ${\bf P}(\mathbb{N})$. These are subsets of all statements of set theory which may be interesting in their own rights. In fact, there seems to be results about the classical decision problem being decidable in ${\bf P}(2)$ but not in ${\bf P}(3)$ (I may be saying something silly here, as I haven't yet checked the research, so please forgive me if my claim is inaccurate). Imagine we could code the Riemann Hypothesis in ${\bf P}(157)$ and the decision problem was decidable in ${\bf P}(n)$ for all $n\leq 160$. No one would question the pertinence of ${\bf P}(157)$. Unfortunately, this won't happen it seems...
Monk (1971) : Provability with finitely many variables seems to indicate that no finite scheme of axioms can achieve an axiomatization of FOL which is sound and complete. However, we have to be careful about the signatures involved. Monk assumes a language with equality, and a sequence of predicates with identical arity $n\geq 3$. He also crucially assumes that the number of variables is exactly equal to this common arity $n$. Thus, the question outlined in this post falls outside the scope of Monk's paper (since we have no equality, a single binary predicate and an arbitrary number of variables). So there is still hope that completeness can be achieved with the above specialization scheme (see Embedding of consistent subset in first order logic (finitely many variables) for a full description of a possible deductive system involving that scheme). As recommended by Andres and Francois, I will still carefully review the paper and its associated literature.
