@EliahKagan hahaha you are very nice and awesome and making the world a better place

@EliahKagan ooh, yes

@Zanna Some other notations in math work that way syntactically--picking a variable and binding free occurrences of it in some subformula of arbitrary complexity. For example, in $$\sum_{k=1}^n a_k = a_1 + a_2 + \ldots + a_n$$ the subformula $a_k$ has a free variable, $k$, which $\sum_{k=1}^n$ binds to. Likewise for limits, $$\lim_{x \to a} f(x)$$ in which the subformula $f(x)$ has a free variable, $x$, which $\lim_{x \to a}$ binds to.

(I should say, "which... binds," rather than "which... binds to.")

hmm

I should revisit some things I probably knew about at some time :S

Which things?

things like limits

Limits themselves, or the way they are used to define stuff like derivatives and infinite sums?

I don't know, I only got a very tiny toe-dip into those things

Can you tell me more about that tiny toe-dip?

(I understand if you cannot, since I imagine you're fairly busy.)

I got to do a few small bits of it, just some very simple problems using, what is it called, differentiation and integration, when I was studying physics

one friend I had on the course helped me with that

It was a bit tricky

but it was very impressive to me also. I was like "what a fantastic invention!"

So you are of the view that these things are invented, rather than discovered? :)

I haven't given that as much thought as it deserves, but, yes I think I am of that view. But this calculus seemed entirely like an ingenious technology (it has even got pretty handles!) (rather than a thing that just seems to be lying there in front of you like the fourness of four things or the twoness of half of them, even though probably these things are just so embedded in the technology of language that they are taken for granted)

@Zanna Pretty handles?

$\int$ <-- this

I agree with your sentiment. When I first learned the limit definition of the derivative, I was overjoyed.

@EliahKagan I should not have called $a_k$ and $f(x)$ subformulas, since they're not formulas, they're terms. This is different from the notations shown there. That is, even $ɿx\, Fx$ and $\{x \mid Fx\}$, which are terms, contain the formula $Fx$. However, syntactically what's going in the summation and limit examples is still pretty similar.

So, in $\forall x\, Fx$, $\exists x\, Fx$, and $\exists! x\, Fx$, one starts with a formula of arbitrary complexity, which I've just been showing as $Fx$. By placing a quantifier with $x$ in front of it, one binds any free occurrences of $x$ in the original formula $Fx$, forming another formula in which $x$ is not free.

Likewise, in $ɿx\, Fx$ and $\{x \mid Fx\}$, one starts with a formula of arbitrary complexity, which I've just been showing as $Fx$. By placing $ɿx$ in front of it, or putting it in place of "$\ldots$" in $\{x \mid \ldots\}$, respectively, one binds any free occurrences of $x$ in the original formula $Fx$, forming a term in which $x$ is not free, even though it is free in the subformula $Fx$.

In the $\sum$ and $\lim$ examples I recently showed, $\sum_{k = 1}^n a_k$ and $\lim_{x \to a} f(x)$, one starts with a term of arbitrary complexity, which I've just been showing as $a_k$ and $f(x)$. By placing $\sum_{k = 1}^n$ or $\lim_{x \to a}$, respectively, in front of it, one binds any free occurrences of $k$ or $x$, respectively, forming another term in which $k$ or $x$, respectively, is not free.