# Axiomatization of first order logic (finitely many variables)

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.

-
I'm curious as to why you're interested in FOL with finitely many variables. You only need two symbols to generate a potentially infinite supply of variables, e.g. $x$, $x'$, $x''$, etc., so why introduce an artificial restriction? –  Marc Hoyois Jul 26 '13 at 17:04
There is an extensive literature on the subject, that goes back to Henkin. I suggest you google "Monk logic finitely many variables". You will reach his "provability" paper as first or second hit, and it provides appropriate references. –  Andres Caicedo Jul 26 '13 at 17:07
Marc's suggestion is not to introduce "prime" as a function symbol but rather to use the strings of symbols $x$, $x'$, $x''$, etc. as variables. –  Andreas Blass Jul 26 '13 at 17:21
@Noel: Thanks for the explanation. To be more explicit, my earlier comment was saying that your algebra $\mathbf{P}(\mathbb{N})$ is a subset of the free algebra on the signature $\{\bot, \to, ', x\}$ with $x$ 0-ary and $'$ 1-ary, so in some sense (though not the one you're interested in) it's already "finite-dimensional". –  Marc Hoyois Jul 26 '13 at 19:35
I think it is rather arbitrary to limit the number variables, while you do not limit the formula. You can invent an FOL without variables at all, but then you have a kind of environment, from which you select your variable. But this is just window dressing. –  Lucas K. Jul 27 '13 at 19:49

## 1 Answer

I have spent decades away from much of this material, so the following is not an answer so much as a sequence of suggestions spinning off the idea that the poster is looking for a finite axiomatization of first order logic using just a single binary predicate suggestive of set theory.

In dealing with recursive functions over the natural numbers, there is a technique of converting between functions taking multiple arguments and functions taking one argument: decode the single argument as a tuple and then feed the tuple to the function, run the computation, and return the result. Perhaps finitely many variables could be encoded as definitional predicates which unpack a set-theoretic encoding from a single variable. I don't know if one can try this kind of Skolemization with only predicate symbols but it may be worth considering.

A partial inspiration for this is the Fitch calculus, which is written about in Hans Hermes' book on computability. The calculus is quite complex, but uses something like an alphabet of only two letters and parentheses. Hopefully this pushes the poster in a good direction.

-
@Masked Thank you for this. I will see if Fitch calculus helps me. Regarding the encoding of t-uples they may be something relevant there. The challenge is to show that consistency is preserved in an embedding $i:{\bf P}(2)\to{\bf P}(n)$ with $2\leq n$. There is always a syntactic route, but possibly also a semantic route. So trying to define a 'sound projection' $q:{\bf P}(n)\to{\bf P}(2)$ (so $\vdash\phi\Rightarrow\vdash q(\phi)$ and $q\circ i(\psi)=\psi$). So this involves 'coding' elements of ${\bf P}(n)$ as elements of ${\bf P}(2)$ –  Noel Vaillant Jul 29 '13 at 5:59