Antes de que acabe 2017, con su quinto centenario de la rebelión de Lutero, origen de la Reforma protestante, quisiera aprovechar esta estupenda oportunidad para hablar un poco del cisma en las matemáticas. Para el lego, esto es algo que suena difícil de creer: ¿cismas? ¿división entre los matemáticos? Y encima, ¿división irreconciliable? Pero ¡si en matemáticas es donde uno tiene seguridad de encontrar siempre el mismo resultado! ¡Casi el único terreno donde los hombres pueden esperar llegar siempre a acuerdos!
La Biblia del Oso, texto protestante realizado en Sevilla en el XVI.
Y bien, pues resulta que no es tan simple. Igual que las iglesias cristianas se dividieron hace cinco siglos, el mundo de los matemáticos sufrió una división hace aproximadamente un siglo. Bueno: ‘igual’ claro que no, ya que es bien distinto el tema de los cismas en matemáticas, terreno de una objetividad envidiable, y en religión… Pero a lo que íbamos: en 1917 el holandés L. Egbertus J. Brouwer andaba publicando el primero de sus artículos sobre “teoría de conjuntos intuicionista”, y con esto consumaba una división fundamental. El trabajo de Brouwer llevaría a la matemática intuicionista plenamente desarrollada, y causaría la célebre “crisis de fundamentos” que se desarrolló en los años 1920. Brouwer contra Hilbert, la matemática de la certeza intuitiva contra la matemática de las estructuras libremente postuladas; el crítico de los transfinitos cantorianos frente al defensor del “paraíso de Cantor”; el extravagante que exigía métodos lógicos y de demostración especiales cuando trabajamos con el infinito, frente al más ‘clásico’ defensor del tertium no datur y la reducción al absurdo.
¿No es siempre claro y obvio el resultado en matemáticas? Bueno: sin duda 2 y 2 son 4, sí. Pero ¿cuanto es 2–√2√? Ni siquiera sabemos si es un número irracional o racional.
La Iglesia “católica” es la del Papa Hilbert, la Iglesia “reformada” en este caso fracasó en su ambición ecuménica. Aunque Brouwer y Weyl, dos matemáticos totalmente sobresalientes en su generación, tenían claro que el intuicionismo era ‘el camino’, o incluso —como dijo Weyl— que era ‘la revolución’, lo cierto es que la partida la ganaron los seguidores de Hilbert. Pero no porque la ganaran en el terreno intelectual, ya que Hilbert y los seguidores de su programa no lograron el Santo Grial que buscaban: demostrar la consistencia de la aritmética, del análisis (teoría de los números reales) y de la teoría de conjuntos. La batalla se ganó en el terreno de las instituciones, ya que la mayoría de los matemáticos siguieron la metodología propuesta por Hilbert, y no las duras reformas que defendía Brouwer.
Ahora bien, no es de Brouwer de quien quiero hablar hoy, ni tampoco de Weyl y su enfoque alternativo sobre el continuo. Lo que me parece más interesante es señalar que el tema del cisma no es algo del pasado, no es una cosa anecdótica que haya quedado cerrada y olvidada después de 1931 o 1939. (En 1931 Gödel demuestra sus dos famosos teoremas: el de incompletitud de la aritmética de Peano, y el de indemostrabilidad de su consistencia con medios finitarios; en 1939 Gödel —de nuevo— demuestra la consistencia del axioma de elección relativamente a la teoría de conjuntos sin dicho axioma; en el mismo año, los Bourbaki comienzan a publicar sus exitosos Elementos de matemática, hilbertianos y conjuntistas…) En estos últimos años, el tema se ha revitalizado de la mano del medalla Fields Vladimir Voevodsky (muerto este septiembre de forma prematura).
Voevodsky se hizo célebre por sus contribuciones sobre todo a la cohomología motívica, que le valieron en 2002 el máximo galardón de la Fields, pero también llamó mucho la atención unos años más tarde al dar una conferencia en la que sugería que puede haber una contradicción en la misma aritmética, ¡nada menos! Desarrollando y corrigiendo esta idea, pero sobre todo buscando garantizar la fiabilidad de los resultados matemáticos futuros, Voevodsky acabó uniendo sus fuerzas a las de otros lógicos y matemáticos para desarrollar el sistema HoTT: la llamada teoría de tipos homotópica.
Voevodsky (dcha.) y Martin-Löf (2º dcha.) en Oberwolfach
HoTT es un fundamento para las matemáticas alternativo a la teoría de conjuntos; se aparta del camino de Hilbert para acercarse más bien a los herederos de Brouwer. Pero además de basarse en un sistema de teoría de tipos intuicionista, desarrollado desde los años 1970 por el lógico sueco Per Martin-Löf, tiene el innegable atractivo de que acerca el lenguaje matemático básico a los demostradores de teoremas automáticos. La idea es que, en el futuro, los matemáticos formularán sus resultados en el lenguaje de HoTT y, al hacerlo, podrán recurrir a los theorem provers para producir una versión formalizada y certificada del resultado. Con los nuevos medios informáticos, algo que parecía imposible podría lograrse: la formalización completa de las matemáticas actuales, y con ello la obtención de garantías de que el gran edificio matemático, pese a crecer cada vez más, no alberga ninguna contradicción.
La teoría de tipos HoTT combina de manera sorprendente ideas tomadas de diferentes ramas. Por un lado, la teoría de tipos de Martin-Löf, pese a haberse desarrollado por motivos puros de fundamentos, había encontrado un lugar de privilegio en el mundo de la computación teórica; sistemas computacionales como los proof assistants Isabelle y Coq se basan en la teoría de tipos intensional, con su noción de tipos dependientes. Por su parte, Voevodsky encontró un modo de conectar la teoría de Martin-Löf con ideas de la geometría homotópica, lo cual le condujo a un nuevo axioma de “univalencia” y a la idea de tipos inductivos superiores. Básicamente puede decirse que en este enfoque una sintaxis lógico-matemática de teoría de tipos se une con nociones semántico-modelistas derivadas del universo de la homotopía; y completa el proyecto la conexión de dichos enfoques con los asistentes automáticos a la demostración, o proof assistants.
La frase “fundamentos univalentes” fue empleada por Vladimir Voevodsky en referencia a su visión de un sistema de fundamentos en el que los objetos básicos son tipos de homotopía, formulado mediante una teoría de tipos con el añadido del axioma de univalencia, y formalizado con ayuda automática. Está por ver si este nuevo proyecto, que recibió un gran impulso en 2012 al dedicar el Institute for Advanced Study de Princeton un “Special Year on Univalent Foundations of Mathematics”, dará lugar a nuevos resultados lo bastante potentes como para que la comunidad matemática cambie de rumbo. Se puede imaginar un día cuando los tiempos en que los novatos aprendían el lenguaje conjuntista queden en mero pasado; pero como digo, eso es aun conjetura. Lo cierto es que, al menos en el mundo de la lógica, el tema de HoTT es un tema muy caliente.
Y una cosa está clara: el cisma que se abrió en 1917 todavía tiene vida e inspira nuevos desarrollos.
(Un par de aclaraciones indispensables: los fundamentos univalentes no constituyen un enfoque intuicionista, sino que es un sistema híbrido que toma algunas ideas derivadas del intuicionismo y las combina con nociones matemáticas del entorno de homotopía y categorías. Más aún: es un programa de trabajo que se basa en ciertas conjeturas, especialmente lo relacionado con el axioma de univalencia, que están en pleno estudio y desarrollo.)
Para saber más: el libro de HoTT en https://homotopytypetheory.org/book/
y la conferencia de Voevodsky, https://www.youtube.com/watch?v=O45LaFsaqMA
