Is the 'variable' in 'let $y=f(x)$' free, bound, or neither?

Consider the string 'Let $y = f(x)$." Suppose that it occurs in some elementary context, such as when graphing the function $f$ using $x$/$y$ coordinates. How is this to be understood in predicate logic? We can't have either $x$ or $y$ be free variables, for consider the following:

Let $f:\mathbb{R}\rightarrow \mathbb{R}, \forall x,\ f(x)=2x$

Let $g:\mathbb{R}→\mathbb{R}, \forall x,\ g(x)=x+x$

Let $y = f(x)$

Let $z = g(x)$

$\therefore y = z$

Here the last line is clearly true, but would lack a truth value if either variable were a free variable.

However, if both variables are bound, we're stuck with permutations of quantifiers that mean the wrong things:

$\forall x,\forall y,y=f(x)$ [says the universe has cardinality 1]

$\forall x,\exists y,y=f(x)$ [says f's domain is the universe]

$\exists y,\forall x,y=f(x)$ [says f is a constant function]

$\exists x,\forall y,y=f(x)$ [says the universe has cardinality 1 and f is nonempty]

$\forall y,\exists x,y=f(x)$ [says f is onto the universe]

$\exists x,\exists y,y=f(x)$ [says f is not the empty function]

-
Saying that $y=z$ lacks a truth value is meaningless, the truth value for a formula is defined only in a given model/interpretation (and an interpretation will fix the value of each free variable to a fixed object in the model, and the formula will be true in that model if the values assigned to the two free variables are the same). I think what you intended to say is that the formula is not valid. –  Kaveh Mar 4 '11 at 4:49

It's just a definition of $y$. The statement $y=f(x)$ defines $y$ to be $f(x)$. It doesn't correspond to any particular statement of predicate logic, since you're not claiming anything. Whenever you use $y$ in a statement $P(y)$, you really mean $$\forall y, y=f(x) \implies P(y).$$ You can then use your knowledge that $f$ is a function: $$\exists! y, y = f(x).$$ Using this, you can prove that the extension of the language by adding $y$ is conservative. That means that everything that you prove using this definition of $y$ and does not involve $y$ is actually true even without using $y$. The uniqueness of $y$ guarantees that $f(x) = y$; note that when you say $f(x)$, this is also shorthand for something.

Now to your example. What you're really trying to prove is $$\forall x, \forall y, \forall z, f(x) = y \land g(x) = z \implies y = z.$$ The proof reduces to $x+x=2x$ through the definition of "$f(x)=y$".

-
Isn't this the extension (by definition) rule? –  Kaveh Mar 4 '11 at 4:45
Should be. That only serves to demonstrate the distance between everyday math and axiomatic logic. No wonder "proof assitants" are unusable. –  Yuval Filmus Mar 4 '11 at 16:52

When I was teaching predicate calculus in the introductory course last semester (Well, I was a TA but still...) we took the following approach:

Define terms and formulae.

A term is practically a name for some element of the interpretation (the structure), either a free variable, or a constant in the language and if $F$ is a function and $t_1,\ldots ,t_k$ are terms then $F(t_1,\ldots ,t_k)$ is also a term.

On the other hand, formulae have the familiar structure. You start with atomic formulae which are relations (either equality or within the language) and terms and you say that if you have two formulae then the conjugation, disjunction, negation and implication give you a new formula, as well quantification of $\exists$ and $\forall$.

So the formula $\varphi(x,y)\colon = y=f(x)$ is a formula which receives a TRUE value whenever $y$ is assigned to be $f^M(x)$, it is an atomic formula - namely the equality of two terms.

Now considering the $f$ and $g$ that you have presented above. You will need to have $2$ as a constant in your language, as well the functions of multiplication and addition. Then you want to require your structure to satisfy the axioms that $x+x = 2x$, namely the usual ring axioms (well, you want $\mathbb{R}$ to behave normally) and then you can deduce that.

The lines "let $y = f(x)$" and "let $z=g(x)$" then "$z=y$" can be formulated as follow: $$\forall x\forall y\forall z((y=f(x) \wedge z=g(x))\rightarrow z=y)$$ Or more explicitly: $$\forall x\forall y\forall z((y=2\cdot x\wedge z=x+x)\rightarrow z=y)$$

Another way to look at that is that by definibility. Your language has the addition and multiplication, and $0$, and $1$ as constants.

With that you can define a formula $\varphi(x,y)$ which is only satisfied when $y=f(x)$. In this sense, we have enriched the language with new function symbols - $f$ and $g$.

Now when you say "let $y=f(x)$ and $z=g(x)$" you enrich the language with three other constants, named $x,y,z$, and you add an axiom to you theory "$y=f(x)$" and "$z=g(x)$". Now you claim that from your theory you can deduce that the new constants $y$ and $z$ are interpreted as the same element in the structure.

-

I think that in analysis variables have a personality of their own which is not covered by the notions of "free" or "bound" from predicate calculus. We speak about independent or dependent variables and say, e.g., that the variables $x$, $y$ resp. $r$, $\phi$ are "related" by the equations $x=r \cos\phi$, $y=r\sin\phi$. A given variable $x$ even may give birth to an associated variable $dx$, and on and on. Concerning the formula $y=f(x)$ I would give it the following interpretation: $x$ is a variable taking values in the domain of the function $f$, and $y$ is a variable taking values in the range of $f$, and we assume that at any given time the values of these two variables are related by the equation $y=f(x)$.

It would be interesting to see this everyday use of variables being translated into official logolese . . .

-

The common method to talk about a function in predicate logic is to say, for the desired $y = f(x)$, $$\forall x \exists y \ f(x, y).$$

This treats $f$ as a binary relation, with the quantifiers making the relation act more like a function, namely for every $x$ there is at least one $y$ that satisfies whatever conditions are in the (at this point) predicate $f$ (one could add guards that would restrict this further to say 'at most one $y$' or 'exactly one $y$', or to restrict the domain or codomain).

So in that sense, in this traditional logical rewriting, both variables are bound (since they are mentioned in the quantifiers).

-

I think this is the extension (by definition) rule.

The extension rule is essentially introducing new names (= variables) for terms/formulas. Formally, we take a new variable, and add an axiom to our axioms that states the new variable satisfies the required property. In your case, $y$ is a new variable and it is value is $f(x)$, i.e. the axiom is $y=f(x)$ (it is more complicated that this since $y$ is an object variable not a function variable and therefore you have to treat $x$ as constant as long as you are using $y$). The situation is simpler for propositional logic since we don't have to deal with functional variables.

In short, you can think of the variables as free, but remember that now you have an extra axiom that states the relation between those free variables, and that you can not quantify on $x$ as usual since now it is not an arbitrary object anymore but a specific object satisfying the definition axiom.

-

I think that this question is best answered not by using predicate calculus, but by specifying what we mean by the variables x and y.

If we think of x and y as being variables that represent real numbers, then saying that y is a function of x makes little sense. We don't typically say that 6 is a function of 2, for example. Certainly it doesn't make sense to ask for the derivative of y with respect to x if y and x are numbers.

I worried about this for years, and finally found the following way to explain it to myself. In the above, x represents not an arbitrary real number, but an arbitrary function to the real numbers, whose domain depends upon the application, but let's presume the domain is also the real numbers. In advanced calculus, the domain might be a manifold. So when we define y = f(x), we're defining a new function y with the same domain as x, which the composition of the functions f and x.

Now when we write y=f(x) and z=f(x), therefore y=z, we're saying that y and z designate the same function.

-

Neither.

(1) Let $y = f(x)$.

When you relate the English sentence (1) to a first-order language $\mathcal{L}$, "$f$" will be a unary function symbol of $\mathcal{L}$. This part is clear, yes? This means, according to how interpretations work, that an $\mathcal{L}$-interpretation will map $f$ to a unary function on the interpretation's domain, i.e., to a set of ordered pairs with each term in the pair consisting of just a member of the domain.

Sentence (1) is not treating the variables as free or bound in the way that you're thinking. The English words "$x$" and "$y$" in (1) denote particular symbols of $\mathcal{L}$, just like "$f$" does, i.e., they are being used as English names.$^1$ Sentence (1) doesn't translate to a formula in $\mathcal{L}$ because it is a statement (or rather, imperative) about $\mathcal{L}$ and its interpretations. It is telling the reader to interpret the $\mathcal{L}$-symbols $x$ and $y$ in a certain way, and this interpretation will apply to every $\mathcal{L}$-formula in which the symbols appear, where they may occur free or bound or both. Sentence (1) is putting a restriction on the $\mathcal{L}$-interpretations of $y$ and $f(x)$. It says how the variable assignments must match: if $I$ is an $\mathcal{L}$-interpretation, then $I(y) = I(f(x))$. So if $I(x) = 7$ and $I(f) = \{(7, 14), \ldots\}$ for some $I$, then (1) says that $I(y) = 14$. It says to only consider $I$ where this restriction holds.

Note also that "=" in (1) does not denote the equality symbol of $\mathcal{L}$, if it has one. To make this clearer, you can replace "=" with a symbol intended to denote an order relation or such without requiring $\mathcal{L}$ to have such a symbol. The "=" in (1) (and the previous paragraph) denotes equality in the metalanguage (English with special mathematical jargon).

This is what I take (1) to mean, at least. The other answers don't seem quite right to me or clear enough on this point. The statement is most directly a direction to the reader rather than a description of any mathematical structure.

Cheers, Rachel

$^1$The fact that "$x$" and "$y$" are being used as names is perhaps obscured by the fact that you can then say things like

(2) Then whenever $x$ is negative, $y$ will also be negative.

This makes it seem like the meaning of $x$ is variable, and it is -- but in $\mathcal{L}$, not in English. More accurately, the meaning of $x$ is variable, but the meaning of "$x$" is fixed (for the present discourse). This is analogous to saying that Frege is a logician, but "Frege" is a word with 5 letters; the case with "$x$" is slightly trickier because there are two levels of meaning, that of English and of $\mathcal{L}$. The English word "$x$" is still being used to name the same symbol of $\mathcal{L}$. It only seems to act like a variable in English because the thing that it names is a variable (in $\mathcal{L}$). Sentence (2) is really talking about $\mathcal{L}$-interpretations without mentioning them explicitly. It means "Whenever $I(x)$ is negative...".

-

First, recall that a function is a set of ordered pairs, and the statement $y = f(x)$ is shorthand for $(x,y)\in f$. This is a perfectly good formula, where we make the usual assumption that the variables $x$, $y$ and $f$ represent sets as opposed to proper classes. The main observation is that if we take a formula $\varphi$ with free variables, then we shouldn't expect that sentences resulting from binding the free variables should necessarily be true.

For example, if $\phi$ is $x=y$, then $\forall x, \forall y, \varphi(x,y)$ is false, whereas $\forall x, \exists y, \varphi(x,y)$ is true. The ones you obtain above that "say the wrong things" are false. Moreover, if $\forall x$ is replaced with $\forall x\in A$ for some set $A$, then the proper class problems go away. (Same for $\forall y$.)

-