Is the 'variable' in 'let $y=f(x)$' free, bound, or neither?
Solution 1:
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$".
Solution 2:
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 . . .
Solution 3:
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)$$
Addendum:
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.
Solution 4:
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.
Solution 5:
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...".