[FOM] Regarding bound variables

[Anthony Coulter]

 > Well, try the following experiment: ask an ordinary mathematician
 > whether or not the following is an identity:
 >     f'(x) = f(x)'

I don't usually see ordinary mathematicians write f(x)' , but I do
often see d[f(x)]/dx . And the latter expression is workable. We can
allow limits, derivatives, and integrals to bind their own variables.
Consider the notation:
    "Lim(c) x: f(x)"    for $\lim_{x\to c} f(x)$
    "D(c) x: f(x)"      for ${d\over dx}f(x)|_{x=c} = f'(c)$
    "D(x) x: f(x)"      for ${d\over dx}f(x) = f'(x)$
    "Int(a,b) x: f(x)"  for $\int_a^b f(x)\!dx$

The first two terms above can be defined as:
   (Lim(c) x: f(x)) = Iota y: all epsilon > 0: exi delta: all x:
                      0 < abs(x - c) < delta -> abs(f(x) - L) < epsilon
   (D(c) x: f(x)) = Lim(0) h: (f(c+h) - f(c)) / h
   (D(x) x: f(x)) = D(x) y: f(y)  # Rename dummy variables

where "Iota" is a definite description operator. I leave the integral
as an exercise to the reader; the problem is that it makes use of an
indexed sum like "Sum(1, n) i: f(i)", which has a recursive definition.
The question of how to denote recursive definitions is beyond the scope
of this post.

You'll notice that "Lim(c) x:" and "D(c) x:" apply not to the function
symbol "f" but to the entire term "f(x)". But there's nothing ambiguous
about these terms and their definitions.

Anthony