¿Es "todo razonamiento categórico formalmente contradictorio"?

Question

En el Número de diciembre de 2009 de la Boletín de la Sociedad Matemática Europea hay una entrevista muy interesante con Pierre Cartier. En la página 33, a la pregunta

¿Cuál era el estatus ontológico de las categorías para Grothendieck?

responde

Hoy en día, uno de los puntos más interesantes de las matemáticas es que, aunque todos los razonamientos categóricos son formalmente contradictorios, los utilizamos y nunca nos equivocamos.

¿Podría alguien explicar qué significa esto realmente? (Por favor, siéntase libre de reetiquetar.)

Answer 1

Nota: No soy historiador. Sólo estoy adivinando lo que motivó los comentarios.

Mi suposición es la siguiente: si haces teoría de conjuntos de forma ingenua, a la antigua usanza de "cualquier cosa es un conjunto", te encuentras con la paradoja de Russell; el conjunto formado por todos los conjuntos que no son elementos de sí mismos te da problemas. Así que decides que la teoría de conjuntos necesita formalizarse (estoy hablando de hace 100 años, por supuesto) y escribes algunos axiomas, y los que "ganan" son ZFC, donde sólo las colecciones "pequeñas" de cosas son conjuntos, y las cosas "grandes" como "todos los grupos" no son conjuntos. Por supuesto, no hay nada contradictorio en considerar todos los grupos, o cuantificar sobre los grupos (es decir, decir que "todo grupo tiene un elemento de identidad"), pero no se puede cuantificar sobre el set de todos los grupos.

Y ahora, como son los años 50 o 60 y quieres hacer álgebra homológica y tomar funtores derivados y hacer secuencias espectrales y esas cosas de alguna manera abstracta, ahora sientes un poco la presión, porque quieres definir "funciones" desde la categoría de todos los módulos G (G un grupo) a la categoría de grupos abelianos llamada "cohomología de grupos", pero "H^n(G,-)" no es una función, porque su dominio y su rango no son conjuntos. Así que lo llamas "functor", lo cual está bien, y sigues adelante.

Y a medida que pasa el tiempo, y empiezas a componer funtores derivados, sabes en tu corazón que todo está bien.

Y entonces llega Grothendieck, y probablemente otras personas también, y plantean la cuestión de que realmente hay que tener un poco más de cuidado, porque no queremos otro Frege (que escribió un enorme tratado sobre la teoría de conjuntos, pero permitió conjuntos grandes y sus axiomas eran contradictorios debido a la paradoja de Russell). Así que Grothendieck intentó domar a estas bestias y "volver a lo básico", pero en cierto sentido "fracasó" o, más exactamente, se dio cuenta de que había problemas fundamentales si realmente quería tratar las categorías como conjuntos. "A la mierda", pensó Grothendieck, "este no es realmente el punto principal". Así que dijo "vamos a suponer que existe un universo, es decir, (básicamente) un conjunto en el que se cumplen todos los axiomas de la teoría de conjuntos" (era un poco más complicado que eso, pero aún así). Esta suposición (a) solucionaba todos sus problemas pero era (b) indemostrable a partir de los axiomas de ZFC (debido a Goedel).

Así que hay que adivinar. Cartier tal vez se esté pasando con lo de "contradictorio": la afirmación "la paradoja de Russell es una paradoja" es cierta, pero la afirmación "cualquier manipulación matemática con colecciones de objetos que no forman un conjunto es formalmente contradictoria" es mucho más fuerte y seguramente falsa.

Answer 2

Este es el resumen de Pierre Cartier de la reunión de Oberwolfach Teoría de las categorías y campos afines: Historia y perspectivas (febrero de 2009).

Vivir en un mundo contradictorio: ¿categorías o conjuntos?

En la actualidad, la ambición de ofrecer unos fundamentos globales para las matemáticas, libres de ambigüedades y contradicciones, que abarquen todo el espectro de las actividades matemáticas, se ha visto cuestionada por los conocidos fallos inducidos por el uso y el abuso de las "grandes" categorías. A menos que estemos dispuestos a abandonar una gran parte de las tendencias fructíferas de la investigación matemática, tenemos que enfrentarnos de frente a la realidad (o pesadilla) de unas matemáticas contradictorias. Sugiero una posible salida utilizando una teoría de tipos para formalizar las pruebas de la teoría de categorías.

El fantasma de la contradicción

En su artículo pionero sobre "Transformaciones naturales", Eilenberg y Mac Lane destacaron la importancia de un nuevo tipo de construcciones, ahora conocidas como funtores. Hasta ahora las construcciones conocidas en geometría asociaban dos clases elemento a elemento, por ejemplo un círculo en un plano y su centro. Los ejemplos procedentes de la topología eran de un tipo diferente, asociando globalmente a un espacio otro espacio (como el espacio de bucles) o invariantes algebraicos (como la homotopía o los grupos de homología). También se planteó la cuestión de la naturalidad de algunas transformaciones, como la identificación de un espacio vectorial de dimensión finita con su dual (no natural) o su bidual (natural). La insistencia en las transformaciones conduce a un estilo de demostración "sin puntos". De nuevo, en su descripción axiomática de los grupos de homología de un grupo (o de un álgebra de Lie), tal como la dio en el Seminario de Cartan de 1950, Eilenberg considera una "construcción" que a un grupo G asocia los grupos de homología Hi(G;Z), por ejemplo. Pero no es explícito sobre cómo expresar tal construcción en el paradigma aceptado de la teoría de conjuntos. En el libro de Cartan-Eilenberg también hay una descripción "sin puntos" de la suma directa de dos módulos. Así que, en la mente de los padres fundadores de la teoría de categorías, esta teoría era una especie de superestructura sobre la matemática existente, más bien al nivel de la metamatemática.

En su documento Tohoku, que marcó una época, Grothendieck invirtió esta tendencia. Inspirado por el trabajo de Cartan y sus colaboradores sobre las gavillas y su cohomología, Grothendieck introdujo la cabeza en los métodos infinitos en la teoría de categorías. Su propósito era utilizar los límites directos para definir los tallos de las gavillas de forma categórica, ya que se conocían ya muchos ejemplos de gavillas en una categoría, como gavillas de grupos, de anillos, etc. También uno de los mayores descubrimientos de Grothendieck en este trabajo es la existencia de objetos inyectivos en una categoría razonable (que satisface el axioma AB 5*). Volviendo a este nivel abstracto, uno puede utilizar libremente las gavillas inyectivas, simplificando así en gran medida la teoría general de las gavillas.

Con ello, Grothendieck combinaba dos líneas de pensamiento: los métodos más bien metamatemáticos (por tanto, finitos) de Eilenberg y Mac Lane, con los métodos infinitos de la topología y el álgebra de Bourbaki, centrados en los límites infinitos (directos o inversos) y los problemas universales. Este matrimonio fue extraordinariamente fructífero para las matemáticas, pero hubo que pagar un precio. El razonamiento categórico era "pruebas sin puntos", pero los nuevos métodos exigían considerar las totalidades reales (no potenciales) de todos los espacios, o todas las transformaciones continuas entre espacios. Inmediatamente resurgieron los viejos fantasmas de las paradojas de la teoría de conjuntos, como la antinomia Burali-Forti del conjunto de todos los conjuntos, o la antinomia de Richard relativa a los objetos definibles. Un desarrollo natural condujo a nociones fundamentales, como límite de un funtor, funtor representable y lema de Yoneda, par adjunto de funtores. Pero la enfermedad lógica permaneció, conduciendo, por ejemplo, a una prueba cuestionable de la existencia general de un funtor adjunto.

Si la teoría de categorías puede formularse fácilmente en un marco de lógica de primer orden (y esto llevó a Lawvere a formular la teoría de conjuntos con este espíritu), y si la teoría de conjuntos recibió una axiomatización adecuada como el sistema Zermelo-Frenkel, la combinación de ambos resultó explosiva. Se intentaron algunos remedios, como el uso de universos por parte de Grothendieck y Gabriel-Demazure. Pero esto es muy artificial, como todos los métodos que utilizan un dominio universal, y nos lleva a los difíciles (e irrelevantes) problemas de los grandes cardinales en la teoría de conjuntos.

Por el momento, la situación no es muy diferente a la que prevalecía en el siglo XVIII en el cálculo infinitesimal. Todo el mundo sabía que la existencia de cantidades infinitesimales era cuestionable y que su uso conducía fácilmente a contradicciones. Hoy en día, conocemos los puntos peligrosos, en los que no hay que nadar, y tratamos de mantenernos alejados mientras continuamos nuestra exploración.

Un posible exorcismo de fantasmas

Me gustaría sugerir una posible salida a este impasse. Me parece que el pecado inicial es la opinión predominante sobre la ontología subyacente de las matemáticas. Desde un punto de vista técnico, la propuesta de Hilbert de codificar todo objeto matemático como un conjunto ha sido extremadamente exitosa. Después de la exitosa aritmetización del análisis, representando (de varias maneras: cortes de Dedekind,...) un número real como una colección (o conjunto) de enteros, o pares de enteros, ..., todo tipo de construcciones matemáticas cedieron al paradigma de la teoría de conjuntos. Pero en la forma de pensamiento aceptada, un conjunto sólo se define después de haber creado y puesto bajo control todos sus elementos. Así, hablar del conjunto de los gatos (enteros) significa que se podría llamar al conjunto de todos los gatos (enteros). Así, cuando hablamos de la categoría de los grupos, deben estar presentes todos los grupos imaginables. Este es el punto de vista de los infinitos reales en sentido extensional. La indecidibilidad de la hipótesis del continuo representa para mí una mancha ineludible de este punto de vista "realista" sobre el infinito.

El nuevo enfoque debe basarse en un esquema de comprensión. Es decir, un conjunto se describe por la propiedad característica de sus elementos: el conjunto de gatos se define por la propiedad de ser un gato, descrita con la mayor precisión posible, sin ninguna afirmación sobre la totalidad de los gatos existentes. Esta es una práctica habitual en los lenguajes tipados de la informática. Normalmente, un programa comienza con instrucciones como

x : real

n : número entero

t : booleano

... ... ...

declarando variables de varios tipos (o clases). Un lenguaje de este tipo incorpora reglas para crear nuevos tipos a partir de los antiguos, por ejemplo el tipo

entero → real

es el tipo de secuencias de números reales. Normalmente, también se dispone de un principio de abstracción, en forma de operación λ

λx.t

para describir una función que asocia a x el valor t (descrito por una fórmula que contiene a x). Por tanto, el marco es un λ-calculus tipificado .

Recientemente se han producido avances en la informática teórica, en forma de diversos asistentes de pruebas (HOL Light, Mizar, Coq, Isabelle,...). Son capaces de crear pruebas completamente formalizadas de las matemáticas "reales", como el teorema de los números primos, y comprobar y garantizar su corrección.

Planteo el reto de traducir las pruebas habituales de la teoría de categorías dentro de un sistema así. Lo que debería requerirse es la existencia de tipos como cat (= categorías), func (= funtores),... Así que una frase estándar como "Sea C una categoría" debería ser codificada por una declaración como:

C : gato .

No es necesario pensar en la totalidad de las categorías posibles. Por supuesto, un tipo como conjunto encarnaría la categoría de conjuntos.

Por supuesto, la estrategia implícita es la de Russell cuando inventó la teoría de tipos para curar las enfermedades de la teoría de conjuntos, como el conjunto de todos los conjuntos. . . También me gustaría mencionar que la lógica interna de un topos se parece mucho, así que quizás podríamos formalizar grandes segmentos de la teoría de categorías dentro de un topos universal definido sintácticamente .

Answer 3

Con respecto a lo que dijo Darij, si se ve a Haskell como un sistema formal, es bastante fácil derivar contradicciones; corresponden a bucles infinitos:

loop :: forall a. a
loop = loop

Sin embargo, visto así, la cita se convierte en algo así como:

Hoy en día, una de las cosas más interesantes de la programación informática es que, aunque la mayoría de los lenguajes permiten escribir bucles infinitos, la mayoría de los programas que la gente escribe no son bucles infinitos.

Pero esto no es sorprendente en absoluto, porque la mayoría de la gente construye programas con alguna actividad productiva en mente, en lugar de limitarse a dar vueltas en un bucle vicioso. Y del mismo modo, la mayoría de los matemáticos presumiblemente eligen teoremas y pruebas que les parecen igualmente productivos, en lugar de una paradoja enmascarada, incluso si el sistema formal permitiera esto último. El hecho de que el sistema formal permita la paradoja no significa que no haya formas no paradójicas de demostrar cosas en el sistema, o que la mayoría de las pruebas que la gente escriba no sean estas últimas.

Ahora, uno podría decir, "la gente escribe bucles infinitos". Y esto es cierto. Pero, la analogía con Haskell se rompe un poco en ese punto, porque Haskell lo hace fácil para escribir bucles infinitos. Es simplemente un hecho en el lenguaje, como el mío de arriba. Con los sistemas formales inconsistentes, normalmente no es tan fácil conseguir una prueba de falso. La gente hizo mucha teoría de conjuntos ingenua sin darse cuenta de que se podía hacer, por ejemplo. La paradoja de Russel es probablemente la más fácil de todas, pero es bastante fácil romperla. Por ejemplo, podrías tener una teoría de conjuntos ingenua con más restricciones de tipificación, de manera que proposiciones como x ∉ x no estén bien formadas. Seguirá siendo inconsistente, pero tendrás que hacer más trabajo para construir una paradoja. Como otro ejemplo, una teoría de tipos con Type : Type (es decir, hay un tipo de todos los tipos) es incoherente, pero demostrando que es falso es mucho trabajo .

Así que, para plantear una razón de por qué la gente nunca se equivoca con sus pruebas categóricas, a pesar de que es una posibilidad dado que la gente suele trabajar en un sistema ingenuo: puede que sea mucho más difícil construir pruebas circulares (en teoría de categorías) para la mayoría de los teoremas en los que la gente está interesada que escribir buenas pruebas. Por un lado, puede ser difícil demostrar la falsedad. En segundo lugar, demostrar la falsedad y luego inferir lo que se quiera es obviamente malo, por lo que la lógica paradójica tendría que ser disfrazada como un argumento legítimo. Y es poco probable que ése sea el tipo de razonamiento que un matemático tiene en mente para demostrar cosas que no están bastante relacionadas con las paradojas.

Answer 4

No soy para nada un lógico, pero ya que estoy usando categorías, decidí en algún momento averiguar qué está pasando. Un lógico probablemente le daría una mejor respuesta, pero mientras tanto, aquí está mi entendimiento.

El axioma del universo de Grothendieck (todo conjunto es un elemento de un universo de Grothendieck) equivale a decir que para cada cardinal existe un cardinal mayor estrictamente inaccesible.

(Recordemos que un cardenal $\lambda$ es débilmente inaccesible, si a. es regular (es decir, un conjunto de cardinalidad $\lambda$ no puede representarse como una unión de conjuntos de cardinalidad $<\lambda$ indexado por un conjunto de cardinalidad $<\lambda$ ) y b. para todos los cardenales $\mu<\lambda$ tenemos $\mu^+<\lambda$ donde $\mu^+$ es el sucesor de $\mu$ . Los cardenales fuertemente inaccesibles se definen de la misma manera, con $\mu^+$ sustituido por $2^\mu$ . Normalmente se añade también la condición de que $\lambda$ debería ser incontable).

Asumiendo que ZFC es consistente podemos demostrar que ZFC + "no hay cardinales débilmente inaccesibles" es consistente. A mi entender, esto se debe a que si tenemos un modelo para ZFC, entonces todos los conjuntos más pequeños que el cardinal inaccesible más pequeño seguirían dándonos un modelo para ZFC en el que no existen cardinales inaccesibles. Véase, por ejemplo, Kanamori, "The Higher Infinite", p. 18.

Hasta ahora la situación es bastante similar a, por ejemplo, la Hipótesis del Continuo (CH): suponiendo que ZFC es consistente, podemos demostrar que ZFC+no CH es consistente.

Lo que hace que el Axioma del Universo sea diferente de la CH es que no podemos deducir la considtencia de ZFC + IC de la consistencia de ZFC (aquí IC significa "hay un cadrinal inaccesible"). Esto se debe a que podemos deducir de ZFC + IC que ZFC es consistente: básicamente, de nuevo todos los conjuntos más pequeños que el cardinal inaccesible más pequeño dan un modelo para ZFC. Así que si podemos deducir de la consistencia de ZFC que ZFC + IC es consistente, entonces podemos demostrar la consistencia de ZFC + IC en ZFC + IC, lo que viola el teorema de incompletitud de G\"odel (véase, por ejemplo, Kanamori, ibid, p. 19).

Nótese que la imposibilidad de deducir la consistencia de ZFC + IC a partir de la consistencia de ZFC es más fuerte que simplemente la imposibilidad de demostrar IC en ZFC.

Así que mi conjetura sería que Cartier se refiere al hecho de que la consistencia de ZFC implica la consistencia de ZFC más la negación del Axioma del Universo, pero no ZFC más el propio Axioma del Universo.