La consistencia de New Foundations: una prueba matemática difícil demostrada con Lean

Here is a summary of the key points from the given article, organized using Markdown:

Demostración de la consistencia de la teoría de conjuntos New Foundations

• Randall Holmes ha afirmado desde después de 2010 haber demostrado la consistencia de la teoría de conjuntos "New Foundations (NF)", propuesta por Quine en 1937
• Este repositorio demuestra que NF efectivamente no tiene contradicciones al verificar las partes difíciles de la prueba de Holmes usando el demostrador interactivo de teoremas Lean
• La prueba ya está completa, y la proposición del teorema puede encontrarse en ConNF/Model/Result.lean

Objetivo

• Se sabe que NF es consistente si y solo si Tangled Type Theory (TTT) es consistente
• Se demuestra la consistencia de NF construyendo formalmente en Lean un modelo de TTT
• El trabajo se basa en varias versiones de la prueba de Holmes, pero hubo muchos cambios y agregados para hacerla compatible con la teoría de tipos de Lean
• Este proyecto depende de mathlib, la biblioteca matemática comunitaria escrita en Lean, por lo que puede usar directamente resultados conocidos sobre cardinales o grupos sin tener que demostrarlos desde cero
• El kernel confiable de Lean ha verificado todas las definiciones y teoremas de mathlib y de este proyecto, pero Lean no puede comprobar si las descripciones de definiciones y teoremas coinciden con la explicación en inglés que se pretende, así que hay que tener cuidado con la traducción entre el código del proyecto y el inglés al extraer conclusiones

Teoría de tipos enredados (TTT)

• TTT es una teoría de conjuntos multisorte con la relación de igualdad = y la relación de pertenencia ∈
• Las sortes están indexadas por un ordinal límite λ, y a los elementos de λ se les llama índices de tipo
• La fórmula x = y está bien formada cuando x e y tienen el mismo tipo, y la fórmula x ∈ y está bien formada cuando x puede tener cualquier tipo menor que y
• Uno de los axiomas de TTT es la extensionalidad: un conjunto de tipo α queda determinado de manera única por sus elementos de cualquier tipo β con β < α
• Por ejemplo, si dos conjuntos de tipo α son distintos, entonces para todo β < α tienen elementos de tipo β distintos entre sí, y esta propiedad hace difícil construir modelos de TTT

Estrategia

• La construcción del modelo usa, a grandes rasgos, la siguiente estrategia:

  • Construcción del tipo base

    • Se fija λ como un ordinal límite, κ > λ como un ordinal regular, y μ > κ como un cardinal límite fuerte con cofinalidad al menos κ
    • A los conjuntos menores que κ se les llama pequeños
    • En el nivel -1 se construye un tipo auxiliar llamado tipo base, que queda por debajo de todos los tipos que finalmente formarán parte del modelo
    • A los elementos de este tipo se les llama átomos (no en el sentido de ZFU o NFU), hay μ átomos y están divididos en litters de tamaño κ

  • Construcción de cada tipo

    • En cada nivel de tipo α se produce una colección de elementos modelo para el modelo pretendido de TTT, a veces llamados t-conjuntos
    • Se genera un grupo de permutaciones llamadas permutaciones permisibles, que actúan sobre los t-conjuntos
    • La relación de pertenencia se preserva bajo la acción de las permutaciones permisibles
    • Se exige que cada t-conjunto tenga un soporte bajo la acción de las permutaciones permisibles; este soporte es un pequeño conjunto de objetos llamados direcciones, de modo que siempre que una permutación permisible fija todos los elementos del soporte, también fija el t-conjunto
    • A cada t-conjunto del nivel α se le da una extensión preferida de tipo β para cada β < α, y a partir de los elementos del t-conjunto puede recuperarse qué extensiones se prefieren
    • Las extensiones de estos t-conjuntos en otros subtipos pueden inferirse a partir de la β-extensión, lo que permite satisfacer el axioma de extensionalidad de TTT

  • Control del tamaño de cada tipo

    • Cada tipo α solo puede construirse bajo la hipótesis de que todos los tipos β < α tienen cardinalidad exactamente μ, además de otras hipótesis
    • Es fácil demostrar en el nivel α que la colección de t-conjuntos tiene cardinalidad al menos μ, por lo que hay que mostrar que este conjunto tiene como mucho μ elementos
    • Esto puede lograrse mostrando que no existen tantas descripciones fundamentalmente distintas de objetos enredados bajo la acción de las permutaciones permisibles
    • Para ello se necesita el teorema de libertad de acción, un lema técnico que permite construir permutaciones permisibles
    • El resultado principal de esta sección está aquí

  • Cierre de la inducción

    • Al ejecutar recursivamente el proceso anterior, se pueden generar tipos enredados en todos los niveles de tipo α
    • En teoría de conjuntos este es un paso fácil, pero en teoría de tipos requiere mucho trabajo debido a la interconexión de las diversas hipótesis inductivas necesarias
    • Luego se verifica si nuestra construcción realmente produce un modelo de TTT al satisfacer una axiomatización finita de la teoría
    • Se eligió convertir la axiomatización finita de Hailperin para el esquema de comprensión de NF en una axiomatización finita de TTT, y se presenta en el archivo de resultados
    • Sin embargo, esta elección es arbitraria, y con la infraestructura ya preparada pueden demostrarse fácilmente otras axiomatizaciones finitas

Opinión de GN⁺

• Esta prueba es un resultado muy significativo porque demuestra formalmente la consistencia de la teoría de conjuntos NF, que hasta ahora solo se conocía en un nivel muy abstracto. No solo es importante desde el punto de vista de la matemática pura, sino que también muestra un avance real en el desarrollo de asistentes de prueba y en la demostración automática de teoremas
• El trabajo de formalización con Lean garantiza la exactitud y completitud de la prueba, pero al mismo tiempo puede ser difícil de entender para los matemáticos porque está escrito en un lenguaje que no les resulta familiar. Debería ir acompañado de un esfuerzo por explicar con claridad en lenguaje natural las ideas centrales de la prueba
• También parece faltar una explicación intuitiva del trasfondo teórico, como por qué se necesita el peculiar axioma de extensionalidad de TTT o cuál es su relación con otras teorías de conjuntos. Además de la prueba formal, sería útil complementar con una discusión del contexto filosófico e histórico para mejorar la comprensión de la teoría NF
• También parecen interesantes futuros temas de investigación, como la relación entre el modelo construido y los modelos de la teoría de conjuntos ZFC estándar, o cómo la consistencia de NF se conecta con la consistencia de otros sistemas axiomáticos
• Un caso como este, en el que una prueba tan compleja se formaliza con Lean, puede servir de ejemplo para la automatización de pruebas en otras áreas de las matemáticas. Si se intentaran trabajos similares sobre teoremas cuyos procesos de demostración aún no son bien conocidos, el impacto en la comunidad matemática podría ser grande

[GN⁺]

Comentarios de Hacker News

• Hay muy poco riesgo de que una demostración hecha con Lean sea incorrecta. Sin embargo, independientemente de los errores de Lean, hay que leer con cuidado la conclusión y verificar que realmente sea lo que se demostró, un problema conocido tanto en verificación de software como en matemáticas.
• Este parece ser el primer caso en que se usa un asistente de demostración para resolver el estado de una demostración difícil. Antes hubo proyectos que verificaban demostraciones existentes que incluían elementos de cálculo a gran escala procesados con software no confiable, pero este parece ser el primer caso en que el estatus epistemológico del resultado era incierto dentro de la comunidad matemática.
• Se plantea curiosidad sobre las diferencias fundamentales entre Coq y Lean, y sobre si operan dentro del mismo tipo de lógica. En la discusión relacionada se mencionan cosas difíciles de entender.
• Los defensores de Lean tienden a exagerar demasiado la idea de que Lean es un método de demostración superior. Lean es solo un método alternativo de demostración y, como lenguaje de programación y sistema, tiene sus propios errores y depende en gran medida de varias capas de bibliotecas escritas por otras personas.
• Más que decir que Lean dijo que la demostración es buena, sería más preciso y honesto decir que la demostración escrita fue verificada por matemáticos humanos y luego convertida a Lean, donde también fue verificada. No es exacto decir que Lean proporciona una verificación única y definitiva, o al menos no he visto una explicación que lo afirme de esa manera.
• Se pide una explicación general, en un formato que pueda leer un estudiante de licenciatura en matemáticas o un profesional de ingeniería, sobre qué tiene de especial o novedosa la formalización de la teoría de conjuntos "New Foundations" en comparación con otras formalizaciones.
• Se preguntan si este enfoque eventualmente llevará a demostraciones colaborativas y a la "corrección de bugs", haciendo que las matemáticas se parezcan a un proceso similar al del código en GitHub.
• Según el teorema de Gödel, todo sistema suficientemente poderoso no puede demostrar su propia consistencia; se hace una pregunta al respecto.
• Quisiera seguir de cerca el proyecto mathlib, pero no tengo tiempo. Me pregunto si hay alguna forma de participar de manera muy pasiva.