How many variables in formal logic?

Question

Remark: I assume the equality symbol „$=$“ with its standard semantics to always be included in first-order logic.

Suppose we want to formalize some first-order theory. For our first-order language, we need to fix some set of variables and some set of contstants, e.g. one constant in group theory and Peano arithmetic, no constant at all in ZFC. The choice of a set of constants is most often done quite canonical.

Also, the cardinality of the set of constants can have a direct influence on semantics. For if the set of constants has cardinality $\kappa$ and we add for any two distinct constants $c,d$ the axiom $c\neq d$, each model must have at least cardinality $\kappa$.

What consequences does the choice of the set of variables have?

I can think of these two cases:

• One usually takes an at least infinite set of variables to be able to nest arbitrary many quantifiers. Example: Let $P$ be a 1-ary predicate and $F$ be a 2-ary function, then the formula $$ \forall x_1 \forall x_2 \forall x_3 \dots \forall x_n : P(F(x_1,F(x_2,F(x_3, \dots ,F(x_{n-1},x_n)))))$$ does only make sense, if one has at least $n$ distinct variables.
• If one has at least $n$ distinct variables, one can add axioms like $$ \exists^{\ge n} x : P(x) \qquad \text{or} \qquad \exists^{\le n} x : P(x)$$ which imply each model to contain at least $n$ or at most $n$ elements.
• If one wants to enumerate the set of all strings and do some gödelian reasoning, one must only take a countable set of variables.

Do you know any more cases, where the cardinality of the set of variables does matter? Does it, as long as it is infinite, affect the class of models for our formal theory?

Answer 1

EDIT: Note that Eric Wofsey's answer here differs from mine. This is not a contradiction; we're describing two different, totally satisfactory ways of making things precise. This reflects part of why this isn't generally talked about (not saying that's a good thing) - there's not really a "best implementation," and there are many "good enough" implementations with no significant differences (in my opinion) between them.

This is a good question, and one which is often passed over (unfortunately). Generally the answer you'll see is "all that you could want," and formally what that means is that we have a proper class of every relevant type of thing. In particular, there is no "set of all first-order formulas."

A formal presentation is a bit messy, but here is one approach:

To get as many of everything as we want, we'll proceed as follows:

• An $n$-ary relation symbol is any set of the form $\langle \langle 0,n\rangle,x\rangle$ for $x$ a set.

• An $n$-ary function symbol (and we'll treat constant symbols as nullary function symbols) is any set of the form $\langle \langle 1,n\rangle,x\rangle$ for $x$ a set.

• A variable is any set of the form $\langle \langle 2,2\rangle,x\rangle$ for $x$ a set.

Here $\langle\cdot,\cdot\rangle$ is your favorite ordered pairing notion.

We can then build, on this basis, the proper classes of all first-order terms/formulas/sentences. Note that the intrusion of proper classes here isn't really making things any worse, since we already have proper classes kicking in on the semantics side (how many structures are there?).

Theorems about first-order logic are then phrased carefully by talking about sets of symbols - e.g. the compactness theorem is phrased as

For any set $\Sigma$ of relation symbols, function symbols, and variables, and any set $X$ of sentences using only the logical symbols and the symbols from $\Sigma$, if every finite subset of $X$ has a model then $X$ has a model.

This can raise the worry that some natural results about first-order logic are actually ill-posed, in that when we try to formalize them naively we wind up talking about classes in an illegal way. This can be gotten around by just being careful about phrasing them; alternatively, we can work in a broader theory like NBG which trivializes the issue.

---

This is not to say that restricting to smaller collections of symbols is uninteresting (and for example you're right that Godel numbering doesn't work when our language gets too big); however, it's not something we do a priori. The general development of first-order logic does take this proper class approach.

It's also worth noting that all proper classes need not be equivalent (see e.g. here) - and so to avoid any possible issues I've really gone for the biggest possible type (e.g. the class of $2$-ary relation symbols is in definable bijection with the class of all sets).

Answer 2

In standard first-order logic, there is always an infinite set of variables available. As you point out, if there were only finitely many variables, that would severely diminish the expressiveness of the language. I've never seen such a thing studied, and it seems like more of a syntactic curiosity than something that is really of interest as a logic.

Assuming you have infinitely many variables, it doesn't matter how many you have (so, the standard setup is just to say you have countably infinitely many). Any formula only uses finitely many variables, and the semantic value of a sentence (i.e., which models satisfy it) is unchanged if you replace all of its variables with different variables. Similarly, if you want to talk about proofs, any proof will involve only finitely many formulas with finitely many variables, which you can replace freely with other variables without changing the validity of the proof. So, if you have some fixed countably infinite set of variables, you can always just replace all the variables in a given formula by variables from that set.

Note that despite their syntactic similarity, constants and variables are in some sense very different sorts of things and you should not think of them as being on an equal footing. Variables are just part of the basic underlying syntactic machinery of the logic, analogous to connectives and quantifiers. No matter what theory you are studying, you still use the same set of variables (not that you have to, but there's just no reason to change it). Constant symbols, on the other hand, are non-logical symbols which are chosen as part of the specific theory you want to talk about and which receive interpretations in models, along with relation and function symbols (in fact, I would consider them to be a special case of function symbols, namely the $0$-ary function symbols).