En lógica, nos referimos a entidades como $\forall$ et $\exists$ como cuantificadores porque vinculan variables. Sin embargo, la vinculación de variables no sólo se produce en los cuantificadores. Por ejemplo, el símbolo $i$ denota una variable ligada en la siguiente expresión.
$$\sum_{i=0}^n i$$
¿Cómo llamamos a las entidades (como $\sum$ ) que vinculan variables? Me gustaría saber el nombre oficial de tales entidades, para poder leer cómo se formalizan en los sistemas lógicos.
Véase también la sección Cuantificación en la obra de Edsger W. Dijkstra EWD1300 : Gries-Schneider basaron su presentación en las notaciones de Dijkstra/Feijen/Scholten.
He visto que se les llama "aglutinantes" en el contexto de las herramientas de prueba automatizadas.
Para la familia HOL, hay Luz HOL donde la sección 6.1 Cuantificadores en "Tutorial de HOL Light (para la versión 2.20)" dice
Las constantes como '!' que se analizan e imprimen en esta forma abreviada cuando aplicadas a las abstracciones se denominan carpetas porque parece que vinculan variables. (Pero estrictamente hablando no lo hacen: es la abstracción subyacente la que lo hace).
También los documentos relacionados con HOL4 utilizan con frecuencia el término "carpeta".
Mizar no tiene carpetas, pero hay un artículo "Una propuesta de sintaxis para las carpetas en Mizar" por Freek Wiedijk.
En esencia, un binder es una función de orden superior: es una función que mapea una función de $\;X\;$ a $\;Y\;$ a un valor de tipo $\;Z\;$ donde muy a menudo $\;Y\;$ et $\;Z\;$ son los mismos. Así, por ejemplo $\;\forall \;:\; (U \to \text{boolean}) \to \text{boolean}\;$ et $\;\sum : (U \to \mathbb C) \to \mathbb C\;$ .
(Personalmente, no me gusta utilizar el término 'cuantificador' para operadores como $\;\prod\;$ et $\;\int\;$ . Pero me gusta mucho la teoría general de Gries-Schneider sobre los aglutinantes/cuantificadores).
Véase Dirk van Dalen, Lógica y estructura (5ª ed - 2013), página 58 :
En matemáticas hay una serie de operaciones de vinculación de variables como la suma, la integración, la abstracción. Consideremos, por ejemplo, la integración, en $ \int \mathrm{\sin}x dx$ la variable juega un papel inusual para una variable. [...] Decimos que la variable $x$ es encuadernado por el símbolo de integración.
El símbolo
$$\sum_{i=0}^n a_i$$
fue introducido por Fourier en 1820. La anotación sigma se denomina "suma". La cantidad $a_i$ después de la "gran" $\Sigma$ se llama el sumando.
La variable índice $i$ está ligado a la anotación sigma.
Esta característica es común con el signo integral, ya que ambos son una "generalización" de la operación de suma.
Si se piensa en el cuantificador universal como una "conjunción infinita" (es decir $\forall x (x \ge 0)$ como : $(0 \ge 0) \land (1 \ge 0) \land (2 \ge 0) \land ...$ ) y la existencial como disyunción infinita, se puede ver inmediatamente la conexión con la suma ( $\Sigma$ ) y el producto "generalizado" ( $\Pi$ ).
Esta analogía es mucho más clara si se piensa que en el Álgebra de la tradición lógica : Boole, Peirce y Schroeder, la conjunción fue simbolizada como " $.$ " y la disyunción como "+".
Peirce introdujo en 1870 los símbolos del cuantificador - véase La lógica de Peirce - y utilizó para ellos exactamente los símbolos $\Pi$ et $\Sigma$ , donde :
" $\Pi$ significa multiplicación lógica y $\Sigma$ significa adición lógica".
En conclusión, la suma es una operador de enlace de variables como un cuantificador.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
