Los teoremas extensionales se utilizan sobre todo de forma intensionada

Question

Algunos teoremas se enuncian y demuestran extensionalmente, pero en la práctica casi siempre se utilizan intensionally . Voy a poner un ejemplo para que quede claro: la integración por partes: $$ \int_a^b f(x)g'(x)ds = \left[f(x)g(x)\right]_a^b - \int_a^b f'(x)g(x) dx$$ para dos funciones continuamente diferenciables $f$ y $g$ . En la práctica, esto rara vez se aplica a funciones sino a expresiones que denotan funciones. Y lo que es mucho más importante, casi siempre se aplica mediante la "concordancia de patrones" en un producto plazo . Pero tenga en cuenta que la integración suele describirse formalmente como una operación sobre funciones (es decir, objetos extensionales), pero luego en el primer curso de cálculo se enseña a los alumnos a dominar una serie de reglas de reescritura (es decir, operaciones sobre objetos intensionales).

Los lógicos [Leibniz, Frege, Russell, Wittgenstein, Quine, Carnap, por citar algunos] se han preocupado mucho por ello. Los lingüistas [me viene a la mente Montague] y los físicos [A. Bressan] también se han preocupado por ello.

Tengo dos preguntas:

1. ¿Qué otros ejemplos ha encontrado de esta mezcla de extensión e intención?
2. ¿Por qué no se enseña/aprecia más esta dicotomía?

En el caso del álgebra (más concretamente, de las teorías ecuacionales), la respuesta al punto 2 es muy sencilla: porque esta dicotomía no importa en absoluto, ya que tenemos adjunciones bien avenidas entre las teorías extensionales e intensionales [de hecho, a menudo tenemos isomorfismos]. Por ejemplo, no hay ninguna diferencia esencial entre los polinomios (sobre campos de característica 0) tratados sintáctica o semánticamente. Pero hay una enorme diferencia entre los términos del análisis y los teoremas semánticos correspondientes.

Answer 1

Me parece que el equivalente matemático de la distinción intensional frente a extensional en filosofía sería la distinción entre objetos "formales" frente a "funcionales": series de potencias formales frente a series de potencias convergentes, integración formal por partes (sin tener en cuenta la comprobación de la validez de la operación en un sentido de análisis real) frente a integración rigurosa por partes, polinomios formales frente a funciones que resultan estar representadas por un polinomio, etc. Si es así, yo diría que la distinción formal frente a funcional suele tratarse en clases más avanzadas, aunque normalmente no en el primer curso de licenciatura.

Por ejemplo, en álgebra, el concepto de variable indeterminada (y su distinción de la noción teórica de conjunto de una variable en un dominio fijo) tiende a ser suficiente para mantener los dos conceptos distintos en la mayoría de las situaciones que implican funciones teóricas de conjunto y las expresiones formales que dan lugar a esas funciones. En particular, los polinomios pueden ser formales viviendo en algún anillo polinómico $R[x]$ generado por un $x$ en lugar de tener que ser funciones teóricas sobre algún dominio. La geometría algebraica también tiene especial cuidado a la hora de distinguir un ideal de polinomios del lugar teórico de conjuntos que ese ideal recorta en un campo dado, o más generalmente al distinguir un esquema de una variedad.

Del mismo modo, el análisis real, con todos sus contraejemplos de advertencia sobre cómo diversas operaciones formales (por ejemplo, el intercambio de límites o sumas) pueden llevar al desastre si no se verifican las hipótesis funcionales apropiadas, también tiende a ser bastante bueno a la hora de distinguir un cálculo formal de uno funcional; a menudo, el primero se utiliza sólo como motivación heurística inicial, y el segundo se utiliza para la demostración rigurosa. Aunque ciertamente se han cometido errores al tratar un cálculo formal como si fuera funcionalmente válido...

En relación con esto está el omnipresente "abuso de la notación", en el que se hace referencia a un conjunto de objetos, estructuras y formas a través de su componente más destacado (es decir, por sinécdoque). Así, por ejemplo, es frecuente ver una función polinómica $P: {\bf R} \to {\bf R}$ para representar simultáneamente la función polinómica y el polinomio formal que la representa, o viceversa (por ejemplo, "el polinomio $x^2$ "para referirse a la función $x \mapsto x^2$ ). Otro caso común de esto es cuando se trata de espacios (conjuntos con estructura adicional); a menudo se abusa de la notación utilizando el propio conjunto para denotar el espacio, por ejemplo, un grupo podría denotarse por su conjunto $G$ de elementos, en lugar de por la tupla $(G, e, \cdot, ()^{-1})$ de estructuras de grupo, o una función teórica de conjuntos mediante el simple mapeo $f$ en lugar del triplete $(f,X,Y)$ que incluye el dominio y el codominio de esa asignación. Tales abusos son técnicamente ilegales utilizando las interpretaciones más estrictas de la notación matemática, pero ahorran mucho espacio y, cuando se utilizan correctamente, permiten a los lectores centrarse en el contenido real de un argumento y no en su formalismo. Aun así, es útil e importante señalar explícitamente estos abusos de vez en cuando...

Answer 2

Un ejemplo de (1) procede de la teoría de la demostración de la aritmética y de la forma en que vemos las demostraciones de enunciados universales sobre los números naturales. La prueba de consistencia original de Gentzen adoptó un punto de vista intensional, razonando explícitamente sobre las variables propias y la inducción. Schütte dio más tarde una prueba de consistencia mucho más simple basada en un punto de vista extensional, donde la inducción matemática se eliminó en favor de la llamada " $\omega$ -regla", una regla de inferencia infinita que afirma $\forall x.A(x)$ pruebas dadas de $A(n)$ para todos $n\in \mathbb N$ .

Buchholz ha conectó los dos enfoques mostrando cómo el resultado de Gentzen puede reconstruirse mediante la traducción al cálculo secuencial de Schütte, esencialmente leyendo la extensión infinita de las pruebas finitas, intensionalmente definidas. (Él llama a esto ver las derivaciones finitas como "notaciones para derivaciones infinitas"). Hay ciertamente una asimetría mucho más fuerte aquí, porque una vez que se adopta una visión extensional de las funciones recursivas primitivas sobre los números naturales, no se puede volver a una visión simbólica (finita).

Answer 3

Una pregunta reciente sobre interpretaciones combinatorias es decir, encontrar una interpretación para la identidad

$$\sum_{k=0}^m 2^{-2k} \binom{2k}{k} \binom{2m-k}{m}=4^{-m} \binom{4m+1}{2m}$$

ofrece otra clase completa de cuestiones de este tipo. Esta ecuación es mucho más que una tautología cuando se interpreta intensionalmente como relativa a la combinatoria: una interpretación combinatoria implica dar una clase natural $C_l$ de objetos para el lado izquierdo y $C_r$ para el lado derecho y una biyección entre estas clases. Además, y aquí es donde las cosas se ponen realmente interesantes (con respecto a mi pregunta original), tales clases $C_l$ y $C_r$ se consideraría "natural" si, utilizando las reglas habituales del recuento combinatorio, obtuviéramos de forma natural que el número de objetos de $C_l$ de tamaño $m$ es la expresión del lado izquierdo (análogamente para $C_r$ y la rhs). La cuestión es que estas expresiones de recuento se derivarían estructuralmente de las clases combinatorias. Se trata de una interacción mucho más interesante entre 3 objetos extensionales (una función de recuento y 2 clases combinatorias) y 2 intensionales (fórmulas diferentes pero iguales que representan la función de recuento).

Answer 4

Georges Gonthier y François Garillot están haciendo cosas interesantes con los tipos fantasma y la unificación en Coq para permitir escribir, por ejemplo, directv (V + W) la proposición de que $V \oplus W$ es una suma directa.

Aún no he comprendido del todo cómo funciona, pero permítanme darles una explicación simplificada de lo que creo que está pasando. Lo que ocurre es que directv X es en realidad una notación para directv_def _ (Phantom _ X) .

Phantom es un constructor de tipo inductivo muy trivial

Inductive phantom (A:Type) (a:A) : Type := Phantom : phantom A a

La función Phantom es un constructor polimórfico de tipo forall (A:Type)(a:A), phantom A a . El objetivo de Phantom es elevar los valores al nivel de tipo para que la inferencia de tipo pueda operar sobre estos valores.

directv_def ni siquiera utiliza el (Phantom _ X) (porque no contiene datos). El único propósito de este argumento es conducir el motor de inferencia de tipo para rellenar el primer argumento. directv_def tiene tipo forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop . addv_expr es un tipo de registro.

Record addv_expr := build_addv_expr {
 V1 : VectorSpace; 
 V2 : VectorSpace;
 Vadd : VectorSpace }

La definición de directv_def es

directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW)

El ingrediente final es que fun V1 V2 => (build_addv_expr V1 V2 (V1 + V2)) se declara como Estructura Canónica.

¿Qué lee Coq cuando escribes directv (V + W) ? Bueno, analiza esto como notación para

directv_def _ (Phantom _ (V + W))

El primer parámetro de Phantom es el tipo de (V + W) así que podemos rellenarlo rápidamente para obtener

directv_def _ (Phantom VectorSpace (V + W))

Phantom VectorSpace (V + W) tiene tipo phantom VectorSpace (V + W) pero directv_def espera algo del tipo phantom _ (Vadd _) por lo que intenta unificar (V + W) con (Vadd _) . Porque Vadd es una proyección de registro, Coq intenta buscar en su lista de estructuras canónicas para ver si hay alguna declarada cuyo Vadd es de la forma (V + W) . Dice: "¡Ajá! ¡lo hay! puedo usar build_addv_expr V W (V + W) "(nótese aquí el comportamiento intensional de la inferencia canónica). Así pues, Coq unifica con éxito (V + W) con (Vadd (build_addv_expr V W (V + W)) y esto fuerza el primer parámetro de directv_def:

directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W))

Y eso es todo para la inferencia de tipos. Más tarde esta expresión podría ser utilizado, por lo que comenzará a normalizar:

dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W))) 

y luego a

dim V + dim W = dim (V + W)

Si intenta escribir otra cosa como directv 0 entonces la inferencia de la estructura canónica fallará y obtendrá un (probablemente obtuso) error de tipo.

---

Este ha sido un ejemplo simplificado. En la realidad, directv es mucho más complicado y permite escribir directv (\sum_(0 <= i < n) V i) es decir $\bigoplus_{i=0}^n V_i$ es una suma directa y acepta cosas como directv 0 para referirse a una suma directa trivial.

Matita permite escribir directamente sugerencias de unificación sin tener que construir necesariamente estructuras canónicas. Sospecho que hacer este tipo de inferencia intencional sería más fácil en un sistema de este tipo.

Answer 5

¿Existe una definición formal de la distinción intensión/extensión, o incluso de "intensión" y "extensión" como términos separados?

En los ejemplos comentados aquí, la diferencia es simplemente que hay un tipo más rico de objeto A, que conlleva su propio conjunto de operaciones y relaciones permitidas, que se asigna (quizá de forma parcialmente definida) a un tipo más tosco de objeto B. Lo más tosco B podría ser, como en los ejemplos publicados, un "olvido de la estructura" o una "descategorización" o "evaluación numérica" de A. Algunas de las operaciones permitidas en A no funcionarán perfectamente o sin ambigüedades en B per se debido a la pérdida de estructura. Por ejemplo, sustituir $(x-1)/(x-1)$ por $1$ es correcto para las funciones racionales (intensionales, formales) pero requiere una entrada adicional (un dominio) para definirse sin ambigüedades para las funciones racionales (extensionales, numéricas). La estructura adicional que posiblemente falte puede verse como un restablecimiento de la información perdida al pasar de A a B, o datos de rigidificación necesarios para desambiguar las operaciones sobre B.

Desde este punto de vista, la intensión parece ser sólo una especificación del contexto A, y una interpretación extensional de dicho contexto es una especificación de un mapa de A a algún otro contexto B, normalmente menos estructurado. ¿Hay algo más en esta distinción tal y como aparece en la literatura filosófica o informática?