Does Gödel's Completeness Theorem still hold even if the set of variables is finite?

Question

Let $L$ be a first order language with a finite set of variables. Let $T$ be a consistent set of formulas of $L$. Does it follow that there exists a model for $T$?

Answer 1

I don't think that this is possible in a meaningful way.

The point of Godel's completeness theorem is that it ties in the syntactical and semantical notions together nicely. However it is hard to figure out you would even come up with a syntactic notions in this case: Here is an example: Suppose your language has two constant symbols $a_{1},a_{2}$ and $T$ says that $a_{1}\neq{a_{2}}$. Now in a reasonable proof system you would expect that the rules would allow you to conclude that $\exists{x_{1}},{x_{2}}$ $\text{s.t.}x_{1}\neq{x_{2}}$. But if you say that there is only one variable allowed then you can't really say that.

Edit: I think that the real question here is that if the conclusion only refers to $n$ variables, is there a proof of it that only involves $\leq{n}$ variables? If that was the case what you are attempting would make sense. But I think the following can be fleshed out give a counter example.

Suppose you only have two variables to play around with and that the language has a unary predicate $P$. Suppose that $T=\{\exists{!x_{1}}\text{ s.t. }Px_{1}\} \cup$ $\{\forall{x_{1}}Px_{1}\}$. Now any model $M$ of $T$ should model that the universe has exactly one element. But a proof I do not think is possible without reference to a third variable (this I'm not sure how to prove, and probably requires a proof analysis which I'm not sure how to do).

Note: I don't have Manin's book. However he would have placed restrictions on where substitutions can be made and the attempt to prove the result by assuming the existence of two elements will fail because of these rules (See my answer here: A problem with the interpretation of Kleene (Mathematical Logic) restrictions on deduction on FOL). However in order to show no proof is possible would require a sort of proof analysis in the spirit of Godel's incompleteness which I'm not sure how to do.

Answer 2

This is not an answer but a long comment.

I agree with Danul's answer that a limited supply of individual variables can greatly limit the expressive capability of the language.

But it is well known that f-o logic is not able to express "everything"; in particular, it is not able to discriminate between models with different infinite cardinalities.

Thus, we may suppose that, with only 100 variables, the supposed "finite" f-o logic cannot discriminate between models with more than 100 objects.

But we have f-o math theory, like group theory, which needs a very limited numbers of variables : exactly three (see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001), page 93).

For f-o number theory [see S.C.Kleene, Introduction to Metamathematics (1952), page 82, or Peter Smith, An Introduction to Gödel's Theorems (1st ed - 2007), page 77], two variables suffice.

As explained in Asaf's comment, to assert the infinitude of models of $\mathsf {PA}$ we only need two variables $x,y$ and the constant symbol $0$, because it depends on the two axioms :

$∀x∀y(S(x)=S(y)→x=y)$ and $∀x(x≠0→∃y(x=S(y)))$.

Thus, my perplexity is that, leaving apart the questions of cardinality, I cannot "see" what are the "impacts" of the above limitations: about consistency, completeness, etc.

What about induction axiom for number theory (we have only a finite amount of wf formulae in the "finite" f-o logic) ?

The only modern textbook which I know with a discussion about the "ontology" of variables is :

George Tourlakis, Lectures in Logic and Set Theory. Volume 1 : Mathematical Logic (2003), page 10-on.

I suggest a reflection on this passage [page 12] :

If we are Platonists, then we have available in the metatheory all sorts of sets, including infinite sets, in particular the set of all natural numbers. We can use any of these items, speak about them, etc., as we please, when we are describing or building the formal theory within our metatheory.

Now, if we are not Platonists, then our “real” mathematical world is much more restricted. In one extreme, we have no infinite sets. [footnote : A finitist – and don’t forget that Hilbert-style metatheory was finitary, ostensibly for political reasons – will let you have as many integers as you like in one serving, as long as the serving is finite. If you ask for more, you can have more, but never the set of all integers or an infinite subset thereof.]

We can still manage to define our formal language! After all, the “nonending” sequence of object variables $v_0, v_1, v_2,$ . . . can be finitely generated in at least two different ways, as we have already seen. Thus we can explain (to a true formalist or finitist) that “non-ending sequence” was an unfortunate slip of the tongue, and that we really meant to give a procedure of how to generate on demand a new object variable, different from whatever ones we may already have.

A final "silly" comment. I think is that we have at least a "pragmatic" refutation for the "finite" f-o language : why stop at 10, or 100, or a billion of individual variables ? we have no reason to choose a "specific" limit... thus, assume an unlimited supply of them.

Added - April, 27

About the original question :

Let L be a first order language with a finite set of variables. Let $T$ be a consistent set of formulas of L. Does it follow that there exists a model for $T$?

I think YES.

Consider the language for f-o number thoery, and "restrict" it to two individual variables : $v_0, v_1$; obviously, in this way, we may form only a finite number of wf formulae.

Consider now the so-called system $Q$ of Robinson Arithmetic, without induction schema [see Peter Smith, page 55]; its seven axioms needs only two variables.

If we "restrict" $Q$ to the "finite" f-o language with only two variables, we have a sub-theory $Q^-$, wich is sound ($\mathbb N$ is a model of it) and consistent, if $Q$ is (because if we can prove a contradiction in $Q^-$, this proof is ipso facto also a proof in $Q$).

The notion of valid formula does not change : a formula with only two variable is valid if it is true in all models.

The issue of completeness for the e.g.two-variables "finite" f-o logic is more difficult.

Are we able to prove the completeness theorem ? i.e. that all valid formulae with only two variables are provable ?

Answer 3

By a quick reading of Manin's book I think the answer to your question is yes, by completeness theorem.

Indeed Manin's proof doesn't seem to require the set of variables to be infinite.

Nonetheless I also suppose the following claim being true:

Let $L$ and $L'$ be two languages, such that $L \subseteq L'$ and $L'$ is obtained by $L$ just adding an infinite set of variables. For every $L$-formula $\varphi$ and a $L$-theory $T$ then $T \vdash \varphi$ in the language $L$ if and only if $T \vdash \varphi$ in the language $L'$.

One implication is trivial. The idea to prove the other implication should procede in the following way:

• prove that for any proof that uses formulas with variables in $L' \setminus L$ we can replace such formulas with others obtained by substitution of the wrong variables with suitable terms of $L$, thus obtaining a proof of the same formula in the language $L$;
• by definition of provability conclude the claim.

Of course this is not a proof but I hope it can give an idea of why it should work.