A consistência de New Foundations – uma prova matemática intrincada demonstrada com Lean

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

Prova da consistência da teoria dos conjuntos New Foundations

• Randall Holmes vem afirmando, desde depois de 2010, ter provado a consistência da teoria dos conjuntos "New Foundations(NF)", proposta por Quine em 1937
• Neste repositório, prova-se que a NF é de fato livre de contradições ao verificar as partes difíceis da prova de Holmes usando o provador interativo de teoremas Lean
• A prova agora está concluída, e a proposição do teorema pode ser encontrada em ConNF/Model/Result.lean

Objetivo

• Sabe-se que a NF é consistente se, e somente se, a Tangled Type Theory (TTT) for consistente
• Prova-se a consistência da NF construindo formalmente, em Lean, um modelo da TTT
• O trabalho se baseia em várias versões da prova de Holmes, mas houve muitas mudanças e acréscimos para torná-la compatível com a teoria dos tipos de Lean
• Este projeto depende da mathlib, a biblioteca matemática comunitária escrita em Lean, o que permite usar diretamente resultados conhecidos sobre cardinais, grupos etc., sem precisar prová-los do zero
• Embora todas as definições e teoremas da mathlib e deste projeto tenham sido verificados pelo kernel confiável do Lean, o Lean não pode verificar se as descrições de definições e teoremas correspondem à explicação em inglês pretendida; portanto, é preciso cuidado ao tirar conclusões a partir do código deste projeto e de sua tradução para a linguagem natural

Teoria dos Tipos Emaranhados (TTT)

• A TTT é uma teoria dos conjuntos multissortida com a relação de igualdade "=" e a relação de pertinência "∈"
• As sortes são indexadas por um ordinal limite λ, e os elementos de λ são chamados de índices de tipo
• A fórmula "x = y" é bem formada quando x e y têm o mesmo tipo, e a fórmula "x ∈ y" é bem formada quando x pode ter qualquer tipo menor que o de y
• Um dos axiomas da TTT é a extensionalidade: um conjunto do tipo α é determinado de forma única pelos elementos de qualquer tipo β tal que β < α
• Por exemplo, se dois conjuntos do tipo α forem diferentes, então, para todo β < α, eles terão elementos diferentes do tipo β, e essa propriedade torna difícil construir um modelo da TTT

Estratégia

• A construção do modelo usa, em linhas gerais, a seguinte estratégia:

  • Construção do tipo de base

    • Define-se λ como um ordinal limite, κ > λ como um ordinal regular, e μ > κ como um cardinal fortemente limite com cofinalidade de pelo menos κ
    • Conjuntos menores que κ são chamados de pequenos
    • No nível -1, constrói-se um tipo auxiliar chamado tipo de base, que fica abaixo de todos os tipos que acabarão fazendo parte do modelo
    • Os elementos desse tipo são chamados de átomos (não átomos no sentido de ZFU ou NFU), há μ átomos, e eles são particionados em litters de tamanho κ

  • Construção de cada tipo

    • Em cada nível de tipo α, produz-se uma coleção de elementos do modelo pretendido da TTT, às vezes chamados de t-conjuntos
    • Gera-se um grupo de permutações chamado de permutações permissíveis, que age sobre os t-conjuntos
    • A relação de pertinência é preservada sob a ação das permutações permissíveis
    • Exige-se que cada t-conjunto tenha, sob a ação das permutações permissíveis, um suporte, isto é, um pequeno conjunto de objetos chamados endereços, tal que sempre que uma permutação permissível fixa todos os elementos do suporte, ela também fixa o t-conjunto
    • Para cada t-conjunto no nível α, fornece-se uma extensão preferida de tipo β < α, e a partir dos elementos do t-conjunto é possível recuperar qual extensão é preferida
    • As extensões desse t-conjunto em outros subtipos podem ser inferidas a partir da extensão β, o que permite satisfazer o axioma de extensionalidade da TTT

  • Controle do tamanho de cada tipo

    • Cada tipo α só pode ser construído sob a suposição de que todos os tipos β < α têm cardinalidade exatamente μ, além de outras hipóteses
    • É fácil provar que, no nível α, a coleção de t-conjuntos tem cardinalidade pelo menos μ, portanto é preciso mostrar que esse conjunto tem no máximo μ elementos
    • Isso pode ser feito mostrando que não existem tantas descrições fundamentalmente diferentes do emaranhamento sob a ação das permutações permissíveis
    • Para isso, é necessário um lema técnico, o teorema da liberdade de ação, que permite construir permutações permissíveis
    • O principal resultado desta seção está aqui

  • Fechamento da indução

    • Executando o processo acima recursivamente, é possível gerar tipos emaranhados em todos os níveis de tipo α
    • Em teoria dos conjuntos esse é um passo simples, mas em teoria dos tipos ele exige muito trabalho por causa da interdependência entre as várias hipóteses indutivas necessárias
    • Em seguida, verifica-se se nossa construção realmente gera um modelo da TTT que satisfaça uma axiomatização finita da teoria
    • Escolheu-se converter a axiomatização finita de Hailperin para o esquema de compreensão da NF em uma axiomatização finita da TTT, e isso é apresentado no arquivo de resultado
    • No entanto, essa escolha é arbitrária, e seria fácil provar outras axiomatizações finitas usando a infraestrutura já preparada

Opinião do GN⁺

• Esta prova é um resultado muito significativo por formalizar a consistência da teoria dos conjuntos NF, algo que até agora era conhecido apenas em um nível muito abstrato. Isso é importante não só do ponto de vista da matemática pura, mas também como exemplo de avanço real em assistentes de prova e prova automática de teoremas
• O trabalho de formalização com Lean garante a exatidão e a completude da prova, mas ao mesmo tempo pode ser difícil de compreender para matemáticos por estar escrito em uma linguagem com a qual eles não estão familiarizados. Será importante avançar em paralelo na explicação clara, em linguagem natural, das ideias centrais da prova
• Também faltam explicações intuitivas sobre a teoria de fundo, como por que o estranho axioma de extensionalidade da TTT é necessário e qual é sua relação com outras teorias dos conjuntos. Se a prova formal vier acompanhada de uma discussão sobre o contexto filosófico e histórico, a compreensão da teoria NF poderá aumentar ainda mais
• Também parecem interessantes temas de pesquisa futuros, como a relação entre o modelo construído e modelos da teoria dos conjuntos ZFC, ou como a consistência da NF se conecta à consistência de outros sistemas axiomáticos
• Um caso como este, de formalização em Lean de uma prova tão complexa, pode servir de exemplo para a automação de provas em outras áreas da matemática. Se trabalhos semelhantes forem tentados para teoremas cujo processo de prova ainda não é bem conhecido, o impacto sobre a comunidade matemática pode ser grande

[GN⁺]

Comentários do Hacker News

• O risco de uma prova feita com Lean estar errada é muito pequeno. No entanto, independentemente de bugs no Lean, ainda é preciso ler a conclusão com cuidado e verificar se o que de fato foi provado corresponde ao que se afirma, um problema conhecido em verificação de software e em matemática.
• Este parece ser o primeiro caso em que um assistente de provas foi usado para resolver o status de uma prova difícil. Antes, houve projetos que verificaram provas existentes com grandes componentes computacionais processados por software não confiável, mas este parece ser o primeiro caso em que o status epistemológico do resultado era incerto na comunidade matemática.
• Surgem dúvidas sobre as diferenças fundamentais entre Coq e Lean e se eles operam dentro do mesmo tipo de lógica. Em discussões relacionadas, são mencionados conteúdos difíceis de entender.
• Defensores do Lean tendem a enfatizar demais a ideia de que Lean seria um método superior de prova. Lean é apenas um método alternativo de prova, e, como linguagem de programação e sistema, tem seus próprios bugs e depende fortemente de várias camadas de bibliotecas escritas por outras pessoas.
• Em vez de dizer que o Lean afirmou que a prova é boa, seria mais preciso e honesto dizer que a prova escrita foi verificada por matemáticos humanos e convertida para Lean, onde também foi verificada. A descrição de que Lean fornece a verificação única e dourada não é precisa, ou pelo menos não vi ninguém descrevendo dessa forma.
• Pede-se uma explicação geral, acessível a estudantes de graduação em matemática ou profissionais de engenharia, sobre o que há de especial ou novo na formalização da teoria dos conjuntos "New Foundations" em comparação com outras formalizações.
• Há curiosidade sobre se essa abordagem acabará levando a provas colaborativas e a "correções de bugs", transformando a matemática em um processo semelhante ao código no GitHub.
• Segundo o teorema de Gödel, todo sistema suficientemente poderoso não pode demonstrar sua própria consistência; isso é questionado aqui.
• Gostaria de continuar acompanhando o projeto mathlib, mas não tem tempo. Pergunta se existe alguma forma de participar de maneira bem passiva.