Jtdylktuy

I am a little unclear about why the whole concept of free and bound variables.

Shouldn't we be trying to bound every variable that appears in any statement of a formal proof?

Otherwise what stops us from doing something like $k = text{donut}$ or $k=text{1/0}$ or $k=(text{picture of a flower})$ if $k$ is not bound to some universe of discourse such as the set of natural numbers, or a specific set or range, etc?

Under what circumstances would we ever use a free variable?

To me it's like defining a useless concept such as "Well when we use the addition operator + we usually put two numbers on either side, but if we don't, we consider it a 'free operator' because it's not adding anything." Like if it's a useless concept, why have it?

Why isn't it a requirement to just bind every variable whenever it's used or introduced? Do proof generally do this in practice where all variables are bound to some universe of discourse (which I assume means "some defined set from which the variable belongs").

One reason we allow statements with free variables is that the same statement can be used for lots of different purposes. Take, for example, the statement $x+y=0$.

We might bind the two free variables with two existential quantifiers and ask whether the resulting statement is true. Or we might bind it with with two universal quantifiers, or with one universal and one existential quantifier.

Or we might bind both variables by sticking the equation into set builder notation and defining its solution set over various different things, such as:

• the real numbers ${(x,y) in mathbb R^2 mid x+y=0}$


• the complex numbers ${(x,y) in mathbb C^2 mid x+y=0}$


• the $5$-adic numbers ${(x,y) in mathbb Q_5^2 mid x+y=0}$
  


• the cyclic group of order $7$ ${(x,y) in C_7 mid x+y=0}$.

In essence, the equation $x+y=0$ becomes, itself, an interesting object of mathematical study. We can consider questions like "How does the solution set of $x+y=0$ vary as we vary the field (or abelian group, or whatever)?" We would not be able to formulate and study such questions if we were forced to bind the variables every time we talked about the equation $x+y=0$.

You have a confusion about what binding a variable means. In first-order logic, a variable isn't "bound to some universe of discourse". In a semantic approach to (single-sorted) first-order logic, all terms including variables (whether free or bound) refer to elements in some given domain. Unless $text{donut}$ is part of your semantic domain (aka a universe [of discourse]), it does not make sense to have it be the interpretation of a variable.

I suspect your confusion comes from the set-theoretic notation, $forall ninmathbb N.P(n)$. This is usually informally interpreted as restricting $n$ to elements of $mathbb N$, but that's not what's happening. I assume this is what you're imagining when you think of $n$ being "bound to" the "universe of discourse" $mathbb N$. What's actually happening is $forall ninmathbb N.P(n)$ is shorthand for $forall n.ninmathbb Nto P(n)$. In other words, $n$ ranges over the whole domain (i.e. the actual universe of discourse) which is all sets as this is in the context of a set theory. It is merely the case that $ninmathbb N$ will be false if $n$ is not a natural number. And again, per the first paragraph, $text{donut}$ will not be a possibility for $n$ unless $text{donut}$ refers to some specific set.

It might be worth elaborating on what the semantics of formulas with free variables is. A semantics for a single-sorted first-order logic consists of a set, $D$, called the domain and an interpretation for formulas. In my strongly held opinion, the best way to organize this is to index formulas by the (usually finite) set of free variables that may occur in them. Write $mathsf{Form}(V)$ for the set of formulas with free variables in $V$. An interpretation is then a family of functions (satisfying some laws) indexed by sets of free variables, $mathsf{interpret}_V:mathsf{Form}(V)to mathcal P(D^V)$ where $D^V$ is the set of functions from $V$ to $D$ and $mathcal P$ is the powerset operation. That is, $mathsf{interpret}_V$ applied to a formula produces a subset of $D^V$ corresponding to those functios $Vto D$ that satisfy the formula. Since we can rename variables, we only really care about how big $V$ is. That is, we could write something like $mathsf{interpret}_n : mathsf{Form}(n) to mathcal P(D^n)$, and now $mathsf{interpret}_n$ applied to some formula produces an $n$-ary relation¹. With this perspective, the $i$th free variable corresponds to the $i$th projection $pi_i : D^nto D$. For example, the semantics of the formula $x = y$ would be ${pin Dtimes Dmid pi_1(p) = pi_2(p)}$. I've been talking about "free variables" but there aren't separate free versus bound variables as far as the semantics is concerned. A quantifier gets interpreted as an operation $mathcal P(D^{n+1})tomathcal P(D^n)$. So a variable is represented by a projection but still a projection into the given domain set $D$.

You could alternatively take a syntactic approach to this. I won't go into detail about it, but ultimately it is even more stringent. At the level of syntax, it doesn't make sense to talk about the "value" of a free variable. Further, the only things you can refer to are things that your formal language includes. Your syntax for terms is very unlikely to include a picture of a flower as a well-formed term. Even if it did, it would not have any significance. It would just be an elaborate way of naming a constant. The notion of free and bound variables lives at the level of syntax (which is why it was unimportant to the semantics in the previous paragraph), but the "universe of discourse" is a semantic concept.

¹ I actually don't recommend doing this and rather sticking to the $D^V$ view because the names of free variables have some significance, particularly when we're combining multiple formulas. I'm just assuming things will seem more familiar if I talk about relations and the names don't matter for our purposes here.