La consistencia de New Foundations: una demostración matemática difícil verificada con Lean

 (leanprover-community.github.io)
1 puntos por GN⁺ 2024-04-24 | 1 comentarios | Compartir por WhatsApp
  • La parte difícil de la demostración de consistencia de New Foundations, la teoría de conjuntos propuesta por Quine en 1937, fue verificada con Lean, y el teorema central está resumido en ConNF/Model/Result.lean
  • El enfoque usa el resultado de que la consistencia de New Foundations y la de Tangled Type Theory (TTT) son equivalentes, construyendo formalmente dentro de Lean un modelo de TTT
  • El modelo de TTT es difícil de construir debido a la extensionalidad, que exige que los conjuntos queden determinados de manera única por elementos de tipos inferiores
  • Para construir el modelo se usan el tipo base, los t-set, las permutaciones admisibles, un support pequeño y la preferred extension; además, para controlar el tamaño de los tipos con μ se necesita el freedom of action theorem
  • El kernel de Lean revisa la prueba formalizada, pero no garantiza que los enunciados formales coincidan con el significado pretendido en inglés, por lo que la interpretación del resultado requiere revisar cuidadosamente la traducción

Verificación de consistencia de New Foundations completada con Lean

  • En 1937, Quine propuso la teoría de conjuntos New Foundations, y Randall Holmes ha sostenido desde 2010 que contaba con una demostración de su consistencia
  • Este proyecto se centra en verificar con el demostrador interactivo de teoremas Lean la parte difícil de la prueba de Holmes para mostrar la consistencia de New Foundations
  • La prueba ya está completada y el enunciado del teorema puede consultarse en ConNF/Model/Result.lean
  • También se ofrecen materiales relacionados

Ejecutar el código localmente

  • Para ejecutarlo en local, basta con instalar elan, clonar el repositorio y luego correr el siguiente comando desde la raíz del repositorio
lake exe cache get
  • Después, el código puede revisarse en un editor como Visual Studio Code, y desde la línea de comandos puede compilarse directamente con lake build

La conexión entre New Foundations y TTT

  • Se sabe que New Foundations es consistente si y solo si Tangled Type Theory (TTT) es consistente
  • El proyecto construyó formalmente en Lean un modelo de TTT y, a partir de eso, obtiene en el papel la conclusión de la consistencia de New Foundations, es decir, Con(NF)
  • El trabajo se basó en varios documentos de prueba de Holmes, pero hizo falta introducir muchos cambios y añadidos para adaptarlo a la teoría de tipos de Lean

Base de la verificación en Lean y precauciones de interpretación

  • El proyecto depende de mathlib, la biblioteca matemática comunitaria escrita para Lean
  • Gracias a mathlib, dentro del proyecto se pueden usar resultados familiares sobre cardinales y grupos sin volver a demostrarlos
  • Las definiciones y teoremas de mathlib y de este proyecto son verificados por el kernel de confianza de Lean
    • El kernel de Lean verifica computacionalmente que la prueba construida sea realmente correcta
  • Sin embargo, Lean no puede comprobar si un enunciado formal coincide con su equivalente pretendido en inglés
    • Al extraer conclusiones del código, hay que revisar con cuidado la traducción entre la descripción en inglés y el enunciado formal

Estructura y dificultades de Tangled Type Theory

  • TTT es una teoría de conjuntos multiestrato con igualdad = y relación de pertenencia ∈
  • Los estratos (sorts) están indexados por un ordinal límite λ, y los elementos de λ se llaman índices de tipo
  • Las condiciones de formación de fórmulas están restringidas por el tipo
    • x = y está bien formado cuando x e y tienen el mismo tipo
    • x ∈ y está bien formado cuando el tipo de x es menor que el de y
  • La dificultad central proviene del axioma de extensionalidad de TTT
    • Un conjunto de tipo α debe quedar determinado de manera única por elementos de cualquier tipo β < α
    • Por ejemplo, si dos conjuntos de tipo α son distintos, entonces para todo β < α deben tener elementos distintos de tipo β
  • Debido a este requisito, construir un modelo de TTT es más complicado que construir un modelo ordinario de teoría de conjuntos

Etapas principales de la construcción del modelo

  • Construcción del tipo base

    • Se toma λ como un ordinal límite, κ > λ como un ordinal regular, y μ > κ como un cardinal fuertemente límite con cofinalidad al menos κ
    • A los conjuntos de tamaño menor que κ se les llama small
    • Primero se construye el base type del nivel -1, un tipo auxiliar situado por debajo de todos los tipos del modelo
    • A los elementos de este tipo se les llama atoms, pero no en el sentido de atom de ZFU o NFU
    • Hay μ atoms, particionados en litters de tamaño κ

  • t-set y permutaciones admisibles

    • En cada nivel de tipo α se construye una colección que será el conjunto de elementos del modelo TTT, llamada t-set
    • Al mismo tiempo se construye el grupo de permutaciones que actúa sobre los t-set, las allowable permutations
    • La relación de pertenencia se preserva bajo la acción de las allowable permutations
    • Cada t-set se define de modo que tenga un support respecto de la acción de las allowable permutations
    • El support es un conjunto pequeño de objetos llamados addresses
    • Si una allowable permutation fija todos los elementos del support, entonces también fija ese t-set

  • Ajustar la extensionalidad con preferred extension

    • Cada t-set del nivel α tiene una preferred extension de algún tipo con β < α
    • A partir de los elementos del t-set puede recuperarse cuál es la extensión preferida, y las extensiones de otros tipos inferiores se derivan de esa β-extension
    • Esta estructura se usa para satisfacer el axioma de extensionalidad de TTT

  • Control del tamaño de los tipos

    • Para construir cada tipo α se necesitan supuestos como que el tamaño de todo tipo β < α sea exactamente μ
    • Es fácil demostrar que la colección de t-set del nivel α tiene tamaño al menos μ, así que hay que mostrar que tiene a lo sumo μ elementos
    • Para ello se demuestra que no hay demasiadas descripciones esencialmente distintas de tangles bajo la acción de las allowable permutations
    • Este paso requiere el lema técnico freedom of action theorem, que permite construir las allowable permutations
    • El resultado principal de esta sección está en ConNF.mk_tSet

  • Cierre inductivo y verificación de axiomas

    • El proceso anterior se ejecuta recursivamente para generar el tipo de los tangles en todos los niveles α
    • En teoría de conjuntos esta etapa es sencilla, pero en teoría de tipos exige mucho trabajo porque varias hipótesis inductivas necesarias están entrelazadas
    • Después se verifica que la construcción sea realmente un modelo de TTT comprobando que satisface una axiomatización finita de la teoría
    • El proyecto usa una axiomatización finita de TTT obtenida al traducir la axiomatización finita del esquema de comprensión de NF de Hailperin
    • El archivo final de resultados está en results file
    • Esta elección es arbitraria, y con la infraestructura ya construida también sería fácil demostrar otras axiomatizaciones finitas

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-04-24
Comentarios en Hacker News

  • Creo que el riesgo de que una demostración hecha en Lean esté mal es muy pequeño
    Aun así, independientemente de bugs en Lean, hay un riesgo bien conocido tanto en verificación de software como en matemáticas: leer con precisión la conclusión para confirmar que realmente se demostró la proposición necesaria
    Leí con cuidado la conclusión final de Wilshaw y me parece que efectivamente demuestra lo que había que demostrar

    • El artículo dice algo parecido: el kernel de confianza de Lean verificó todas las definiciones y teoremas de mathlib y de este proyecto, y comprobó computacionalmente que la demostración que construimos es realmente correcta
      Pero Lean no puede verificar si los enunciados de definiciones y teoremas coinciden con la formulación en inglés que se pretendía, así que al extraer conclusiones del código de este proyecto hay que tener cuidado con la traducción al lenguaje natural

    • El problema que menciono también se conecta con preocupaciones sobre las bibliotecas: cuando se usa algún concepto definido, hay que estar seguro de que esa definición es la correcta, es decir, de que de verdad se probó lo que hacía falta
      La formalización de Wilshaw sí usa bibliotecas, pero no es vulnerable a esta objeción. Lo que se probó es que cierto concepto definido satisface un conjunto específico de fórmulas de lógica de primer orden, y si existe un predicado que satisface esas fórmulas, entonces NF es consistente

    • Otro riesgo son los bugs del propio Lean. Tampoco sería algo sin precedentes en asistentes de prueba 1
      Puede que sea difícil toparse con uno por accidente, pero colaboraciones masivas donde personas al azar completan pasos, como en 3, siguen creciendo. Puede llegar a ser razonable preocuparse por un escenario en el que alguien entorpezca el proceso llenando un paso con ayuda de un bug descubierto por esa persona

    • Desde la perspectiva de los fundamentos, también es importante que esta demostración sea una prueba de equiconsistencia entre NF y el kernel de Lean. El kernel de Lean en sí es revisado por humanos
      Un demostrador de teoremas mecanizado funciona preservando el nivel de corrección que fue inyectado por humanos u otros sistemas externos

  • Si no me equivoco, este parece ser el primer caso en que un asistente de pruebas resuelve el estatus de una demostración difícil que llevaba años en una situación ambigua
    Ha habido proyectos que verificaron demostraciones ya existentes donde software no confiable se encargaba de una gran parte computacional, como el teorema de los cuatro colores en Coq, pero esta parece ser la primera vez que el estatus epistemológico mismo del resultado era incierto para la comunidad matemática más amplia

  • ¿Alguien podría explicar a grandes rasgos qué tiene de especial o novedosa la formalización de la teoría de conjuntos “New Foundations” en comparación con otras formalizaciones?
    O también serviría algún enlace con una explicación legible para un estudiante de licenciatura en matemáticas o un profesional de ingeniería

    • Acabo de editar el artículo de Wikipedia y ahora debería ser algo más fácil de leer: https://en.wikipedia.org/wiki/New_Foundations
      Para mí, el punto clave es la existencia del conjunto universal. En mi caso de uso, los sistemas de tipos de lenguajes de programación, ese conjunto universal es muy útil
      Los distintos atajos de los sistemas tradicionales, como universos acumulativos o type-in-type, no me resultan satisfactorios. En cambio, aquí basta con comprobar que la firma de tipos está estratificada y luego se puede olvidar que los tipos tienen niveles numéricos
    • Lo que me gusta mucho estéticamente de NF es cómo ajusta el axioma de selección de subconjuntos para que el “conjunto de todos los conjuntos” no produzca la paradoja de Russell
      Básicamente exige que el predicado usado para elegir subconjuntos respete un sistema de tipos muy liviano. “x no es elemento de sí mismo” no es una pregunta bien tipada en un sistema de tipos razonable y, en particular, tampoco satisface el requisito de “estratificación” de NF, así que no se puede construir el conjunto paradójico de Russell de todos los conjuntos que no se contienen a sí mismos
    • Una cosa “buena” de NF es que solo tiene dos axiomas/esquemas de axiomas: 1) los conjuntos con los mismos elementos son iguales, 2) a cualquier propiedad estratificable le corresponde el conjunto de todas las cosas que tienen esa propiedad
      La definición de “estratificable” tampoco es tan complicada. En cambio, ZF tiene ocho axiomas/esquemas de axiomas que parecen bastante más ad hoc

  • Llegué a este texto porque tenía curiosidad por la diferencia fundamental entre Coq y Lean, y por si operan sobre la misma clase de lógica 1
    Casi no entendí esa discusión y en realidad no uso ninguno de los dos. Si alguien quiere ampliar sobre eso o compararlos con otros asistentes de prueba, me interesaría leerlo

    1 https://proofassistants.stackexchange.com/questions/153/what...

  • Parece que quienes defienden Lean a veces exageran un poco su forma de expresarlo. Lean no es un método de demostración superior, como a menudo se da a entender, sino una forma alternativa de demostrar
    Si intentas aprender Lean, pronto descubres que es un lenguaje de programación y un sistema con sus propios bugs, y que depende muchísimo de varias capas de bibliotecas escritas por otros humanos. Esas bibliotecas incluyen elecciones de diseño, y también pueden tener huecos o errores
    Por eso no estoy de acuerdo con frases como “Lean dijo que esa demostración es buena”. Una forma más precisa y honesta de decirlo sería que matemáticos humanos verificaron la demostración escrita, y que humanos la tradujeron a Lean y también fue verificada ahí. No me parece exacto decir que Lean ofrece la única validación dorada, o al menos nunca he visto una explicación convincente de eso. El subtítulo, “Digitalización de la demostración de Randall Holmes”, me parece la forma más precisa de decirlo

    • Considero que una demostración verificada por máquina en un sistema fuerte como Lean es muy superior a una demostración revisada solo por humanos. Los humanos son asombrosos, pero se aburren y a veces pasan por alto detalles
      Esto no es solo una afirmación teórica. La gente leyó los Elementos de Euclides durante más de 2 mil años antes de darse cuenta de que faltaba un axioma. Es el tipo de error básico que un sistema funcional de verificación mecánica de demostraciones habría detectado de inmediato
      También pasa con frecuencia que demostraciones matemáticas publicadas más tarde resultan estar equivocadas. A medida que las matemáticas se vuelven más sofisticadas, se hace cada vez más difícil que los humanos verifiquen correctamente todos los pasos. Las máquinas todavía no son tan buenas como los humanos para generar demostraciones, pero para verificarlas no tienen comparación
      También hay sistemas que “compiten” con Lean, así que no diría que Lean sea “el único camino verdadero”. Por ejemplo, también me gusta Metamath. Pero esa “competencia” entre sistemas merece comillas. Cada uno tiene ventajas y desventajas distintas, y hay mucha gente a la que le gustan varios sistemas, los usa o contribuye a ellos. Todos pueden verificar teoremas con un nivel de rigor que para los humanos sería irreal

    • Puede haber bugs, pero entiendo que lo único en lo que hay que confiar es en el kernel
      Si “varias capas de bibliotecas escritas por otros humanos” se refiere a mathlib, entonces no creo que eso sea correcto. Al final, el código de mathlib también se compila a código que procesa el kernel
      El borrador del artículo en el sitio web 0 también refuerza este punto: Lean es un proyecto grande, pero para garantizar que una demostración aceptada sea correcta, solo hay que confiar en el kernel. Aunque una táctica produzca un término de demostración incorrecto, el kernel tiene la oportunidad de detectar ese error antes de aceptar la demostración

    • La diferencia es que en Lean solo tienes que confiar en el kernel. Todo lo demás se construye encima. Si el kernel es sólido, entonces todo lo demás también lo es
      Eso es muy distinto de un lenguaje de programación común. En un lenguaje común pueden entrar bugs en cualquier momento. Y también es muy distinto de las matemáticas, donde cualquier lema auxiliar puede contener errores

    • Lo genial de un demostrador de teoremas es que, suponiendo que el kernel esté bien, una demostración incorrecta ni siquiera compila
      En lo que respecta a demostraciones, no hay bugs que aparezcan solo en tiempo de ejecución como en el software tradicional. No existe tiempo de ejecución en ese sentido
      Lean también puede usarse como lenguaje de programación “normal”, y ahí sí existe el riesgo de bugs en tiempo de ejecución, pero aquí no estamos hablando de eso

    • Estás entendiendo mal los demostradores de teoremas. Esto no es algo del nivel de “toda abstracción tiene fugas”. No necesitas confiar en las bibliotecas, solo en el kernel
      Confiar en el kernel tampoco es trivial, pero comparado con una demostración informal sí es un salto enorme. En una demostración informal realmente tienes que confiar en la “biblioteca”, es decir, en la cultura y en el conocimiento de otras personas, porque no hay una manera práctica de reducirlo realmente hasta los axiomas

  • ¿Murió ZFC y viva NF?
    Como matemático aficionado que usa conjuntos principalmente como lenguaje común para describir otras cosas, no tengo claro qué implicaciones tendría esto para áreas más amplias de las matemáticas. Más aún si la utilidad de NF es parecida a la de ZFC y sus variantes existentes
    ¿Se espera que NF llegue a ser tan popular como ZFC en demostración mecánica? La existencia del conjunto universal se siente más intuitiva, así que al menos esta demostración reavivó mi interés personal por la formalización

    • Desde una perspectiva ingenua de aficionado, como todo modelo de ZFC puede extenderse a un modelo de NF, este resultado de consistencia relativa parece hacer que NF sea al menos tan útil como ZFC
      Pero no creo que NF se vuelva mucho más útil salvo que ocurra una de estas dos cosas

      1. Se demuestre que NF es inconsistente. Entonces ZFC también lo sería. Las estrellas del cielo nocturno empezarían a apagarse una por una ;)

      2. Se demuestre que ZFC es inconsistente. Entonces todavía quedaría abierta la posibilidad de que NF sea consistente. Habría que tener suerte

      Claro, es muy posible que me esté perdiendo ventajas más prácticas de “calidad de vida” de NF, como poder hablar de clases propias o evitar la paradoja de Russell con fórmulas estratificadas

    • No hay ninguna intención de impulsar NF como sistema fundacional independiente. NF es un sistema bastante peculiar
      Aun así, si alguien quisiera promoverlo, este resultado de consistencia al menos dice que, en el sentido de riesgo de llegar a una contradicción, no es mayor que en ZFC

  • Esto realmente me encanta
    Me pregunto si al final esto llevará a demostraciones colaborativas y a “corrección de bugs”, y si las matemáticas terminarán pareciéndose a un proceso como el del código en GitHub

  • Ojalá tuviera tiempo libre para seguir el proyecto mathlib. Es realmente increíble
    ¿Hay alguna forma de participar aunque sea de manera muy informal?

  • No soy de este campo, pero ¿no existía el teorema de Gödel de que ningún sistema suficientemente fuerte puede demostrar su propia consistencia?

    • Probablemente estás pensando en los teoremas de incompletitud de Gödel: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
      Aun así, aunque un sistema X no puede demostrar su propia consistencia, un sistema más fuerte Y sí puede demostrar la consistencia de X. Y otro sistema aún más fuerte podría demostrar la consistencia de Y. Así se forma una cadena en la que cada sistema demuestra la consistencia de sistemas más débiles.
      Eso no prueba que el sistema sea absolutamente consistente. Si Y es inconsistente, entonces podría demostrarse tanto que X es consistente como que X es inconsistente. Aun así, sigue teniendo valor. Después de todo, una de las razones por las que usamos Y es que no conocemos contradicciones dentro de él. Los sistemas formales a menudo pueden ser sutilmente inconsistentes, así que “consistente bajo la suposición de que otro sistema es consistente” es mucho mejor que “no hay ninguna prueba de consistencia en absoluto”
    • Aquí no se está demostrando que el sistema pruebe su propia consistencia. La consistencia se demuestra en otro sistema más fuerte
    • Lo interesante es que, incluso si un sistema fuerte pudiera demostrar su propia consistencia, eso por sí solo no nos diría nada.
      Un sistema inconsistente también puede demostrar su propia consistencia. Por lo tanto, aunque un sistema tenga una prueba interna de que es consistente, eso todavía no nos dice si realmente lo es
    • Esta prueba puede entenderse como: “si Lean 4 es consistente, entonces New Foundations también es consistente”. No contradice los teoremas de incompletitud de Gödel
    • Aquí el sistema no parece intentar demostrar sus propios supuestos fundamentales, sino construir sobre un conjunto de supuestos ya existentes. Da la impresión de que el teorema que tienes en mente no aplicaría

  • También vale la pena ver la discusión en Reddit en la que participó una de las personas que lo hizo 0

    https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...