What do we call entities (like $\sum$) that bind variables?

In logic, we refer to entities like $\forall$ and $\exists$ as quantifiers, because they bind variables. However, variable-binding doesn't just occur at quantifiers. For example, the symbol $i$ denotes a bound variable in the following expression.

$$\sum_{i=0}^n i$$

What do we call entities (like $\sum$) that bind variables? I'd like to know the official name of such entities, so I can read up on how they're formalized in logical systems.

Solution 1:

In "A Logical Approach to Discrete Math" by David Gries & Fred Schneider authors call them all quantifiers (actual quantifiers, summation, multiplication and others). There is a whole section in which they develop general theory for those structures.

Solution 2:

I've seen them called 'binders' in the context of automated proof tools.

For the HOL family, there is HOL Light, where section 6.1 Quantifiers in "HOL Light Tutorial (for version 2.20)" says

Constants such as ‘!’ that are parsed and printed in this abbreviated form when applied to abstractions are called binders, because they appear to bind variables. (But strictly speaking they don’t: it’s the underlying abstraction that does that.)

Also documents related to HOL4 frequently uses the term 'binder'.

Mizar does not have binders, but there is an article "A proposed syntax for binders in Mizar" by Freek Wiedijk.

In essence, a binder is a higher-order function: it is a function that maps a function from $\;X\;$ to $\;Y\;$ to a value of type $\;Z\;$, where very often $\;Y\;$ and $\;Z\;$ are the same. So for instance $\;\forall \;:\; (U \to \text{boolean}) \to \text{boolean}\;$ and $\;\sum : (U \to \mathbb C) \to \mathbb C\;$.

(Personally, I don't like to use the term 'quantifier' for operators like $\;\prod\;$ and $\;\int\;$. But I really like Gries-Schneider's general theory of binders/quantifiers.)

Solution 3:

See Dirk van Dalen, Logic and Structure (5th ed - 2013), page 58 :

In mathematics there are a number of variable-binding operations, such as summation, integration, abstraction. Consider, for example, integration, in $ \int \mathrm{\sin}x dx$ the variable plays an unusual role for a variable. [...] We say that the variable $x$ is bound by the integration symbol.

The symbol

$$\sum_{i=0}^n a_i$$

was introduced by Fourier in 1820. The sigma-notation is called "summation". The quantity $a_i$ after the "big" $\Sigma$ is called the summand.

The index variable $i$ is bound to the sigma-notation.

This feature is in common with the integral sign, both being "generalization" of the sum operation.

If you think at the universal quantifier as an "infinite conjunction" (i.e. $\forall x (x \ge 0)$ as : $(0 \ge 0) \land (1 \ge 0) \land (2 \ge 0) \land ...$) and the existential one as as infinite disjunction, you can see immediately the connection with summation ($\Sigma$) and "generalized" product ($\Pi$).

This analogy is much more clear if you think that in the Algebra of logic tradition : Boole, Peirce and Schroeder, conjunction was symbolized as "$.$" and disjunction as "+".

Peirce in 1870 introduced the quantifier symbols - see Peirce's Logic - and he used for them exactly the simbols $\Pi$ and $\Sigma$, where :

"$\Pi$ signifies logical multiplication and $\Sigma$ signifies logical addition".

In conclusion, the summation is a variable-binding operator, like a quantifier.