A consistência de New Foundations — uma prova matemática difícil verificada em Lean
(leanprover-community.github.io)- A parte difícil da prova de consistência da teoria dos conjuntos New Foundations, proposta por Quine em 1937, foi verificada em Lean, e o teorema central está organizado em
ConNF/Model/Result.lean - A abordagem usa o resultado de que a consistência de New Foundations e da Tangled Type Theory (TTT) são equivalentes, construindo formalmente um modelo de TTT dentro do Lean
- O modelo de TTT é difícil de construir por causa da extensionalidade, que exige que conjuntos sejam determinados unicamente por elementos de tipos mais baixos
- A construção do modelo usa tipo base, t-sets, permutações admissíveis, support pequeno e preferred extension; para controlar o tamanho dos tipos em μ, é necessário o freedom of action theorem
- O kernel do Lean verifica a prova formalizada, mas não garante que a sentença formal corresponda ao significado pretendido em inglês, então a interpretação do resultado exige revisão da tradução
Verificação da consistência de New Foundations concluída em Lean
- Em 1937, Quine propôs a teoria dos conjuntos New Foundations, e Randall Holmes afirma desde 2010 ter uma prova de sua consistência
- Este projeto foca em verificar, com o assistente interativo de provas Lean, a parte difícil da prova de Holmes para demonstrar a consistência de New Foundations
- A prova foi concluída, e a formulação do teorema pode ser vista em
ConNF/Model/Result.lean - Materiais relacionados também foram disponibilizados
Executando o código localmente
- Para executar localmente, instale o elan, clone o repositório e, na raiz do projeto, execute o seguinte comando
lake exe cache get
- Depois disso, o código pode ser explorado em um editor como o Visual Studio Code e também pode ser compilado diretamente pela linha de comando com
lake build
A ligação entre New Foundations e TTT
- Sabe-se que New Foundations é consistente se, e somente se, a Tangled Type Theory (TTT) for consistente
- O resultado relacionado está no teorema 1 de Holmes
- O projeto construiu formalmente em Lean um modelo de TTT e, a partir disso, obtém no papel a conclusão da consistência de New Foundations, isto é, Con(NF)
- O trabalho foi baseado em vários documentos de prova de Holmes, mas foram necessárias muitas mudanças e adições para adequá-lo à teoria dos tipos do Lean
Base da verificação em Lean e cuidados de interpretação
- O projeto depende da biblioteca matemática comunitária mathlib, escrita em Lean
- Graças ao mathlib, resultados familiares sobre cardinais e grupos podem ser usados no projeto sem precisar ser provados novamente
- As definições e os teoremas do mathlib e deste projeto são verificados pelo kernel confiável do Lean
- O kernel do Lean verifica computacionalmente se a prova construída é de fato correta
- Ainda assim, o Lean não consegue verificar se a sentença formal coincide com o equivalente em inglês pretendido
- Ao tirar conclusões a partir do código, é preciso examinar com cuidado a tradução entre a descrição em inglês e a sentença formal
Estrutura e dificuldades da Tangled Type Theory
- A TTT é uma teoria dos conjuntos multissortida com igualdade
=e relação de pertinência∈ - Os sorts são indexados por um ordinal limite λ, e os elementos de λ são chamados de índices de tipo
- As condições de formação das fórmulas são restringidas pelos tipos
x = yé bem formada quandoxeytêm o mesmo tipox ∈ yé bem formada quando o tipo dexé menor que o tipo dey
- A principal dificuldade vem do axioma de extensionalidade da TTT
- Um conjunto de tipo α deve ser determinado unicamente por elementos de algum tipo β arbitrário com β < α
- Por exemplo, se dois conjuntos de tipo α são diferentes, então para todo β < α eles devem ter elementos diferentes de tipo β
- Por causa dessa exigência, construir um modelo de TTT é mais difícil do que construir um modelo de teoria dos conjuntos simples
Principais etapas da construção do modelo
-
Construção do tipo base
- Tome λ como um ordinal limite, κ > λ como um ordinal regular e μ > κ como um cardinal fortemente limite de cofinalidade ao menos κ
- Conjuntos de tamanho menor que κ são chamados de small
- Primeiro é construído o tipo base de nível -1, um tipo auxiliar abaixo de todos os tipos do modelo
- Os elementos desse tipo são chamados de atoms, mas não são atoms no sentido de ZFU ou NFU
- Existem μ atoms, particionados em litters de tamanho κ
-
t-sets e permutações admissíveis
- Em cada nível de tipo α, é construída uma coleção que será composta pelos elementos do modelo de TTT, chamada de t-set
- Ao mesmo tempo, é construído o grupo de permutações que atua sobre os t-sets, as allowable permutations
- A relação de pertinência é preservada sob a ação das allowable permutations
- Cada t-set é definido para ter um support em relação à ação das allowable permutations
- O support é um pequeno conjunto de objetos chamados addresses
- Se uma allowable permutation fixa todos os elementos do support, então ela também fixa esse t-set
-
Ajustando a extensionalidade com preferred extension
- Cada t-set de nível α tem uma preferred extension de algum tipo com β < α
- A partir dos elementos do t-set, é possível recuperar qual extension é preferida, e extensões de outros tipos mais baixos são derivadas dessa β-extension
- Essa estrutura é usada para satisfazer o axioma de extensionalidade da TTT
-
Controle do tamanho dos tipos
- Para construir cada tipo α, é preciso assumir, entre outras coisas, que o tamanho de todos os tipos β < α é exatamente μ
- Como é fácil provar que a coleção de t-sets no nível α tem tamanho pelo menos μ, é preciso mostrar que ela tem no máximo μ
- Para isso, mostra-se que não há muitas descrições essencialmente diferentes de tangles sob a ação das allowable permutations
- Essa etapa requer o freedom of action theorem, um lema técnico auxiliar que permite construir as allowable permutations
- O principal resultado desta seção está em ConNF.mk_tSet
-
Fechamento indutivo e verificação dos axiomas
- O processo acima é executado recursivamente para gerar, em cada nível de tipo α, o tipo dos tangles
- Em teoria dos conjuntos, essa é uma etapa simples, mas na teoria dos tipos ela exige muito trabalho porque várias hipóteses indutivas necessárias ficam entrelaçadas
- Depois disso, verifica-se se a construção é um modelo de TTT testando se ela satisfaz uma axiomatização finita da teoria
- O projeto usa uma tradução da axiomatização finita do esquema de compreensão de NF de Hailperin para uma axiomatização finita de TTT
- O arquivo de resultados está em results file
- Essa escolha é arbitrária, e outras axiomatizações finitas também poderiam ser demonstradas facilmente com a infraestrutura já construída
1 comentários
Comentários do Hacker News
Acho que o risco de uma prova em Lean estar errada é muito pequeno
Mas, independentemente de bugs no Lean, há um risco bem conhecido tanto na verificação de software quanto na matemática: é preciso ler a conclusão com precisão para confirmar se a proposição que realmente era necessária foi provada
Li com cuidado a conclusão final de Wilshaw e julgo que ela prova aquilo que de fato precisava ser provado
O artigo diz algo parecido: todas as definições e teoremas do mathlib e deste projeto foram verificados pelo kernel confiável do Lean, e ele verificou computacionalmente que a prova que construímos é de fato correta
Mas o Lean não consegue verificar se as definições e as proposições dos teoremas correspondem às expressões em inglês pretendidas; portanto, ao tirar conclusões a partir do código deste projeto, é preciso ter cuidado com a tradução para o inglês
O problema que mencionei se conecta a preocupações relacionadas a bibliotecas: quando se usa algum conceito definido, é preciso ter certeza de que essa definição está correta, isto é, de que foi realmente provado o que era necessário
A formalização de Wilshaw usou bibliotecas, mas não é vulnerável a essa objeção. O que foi provado é que certo conceito definido satisfaz um conjunto específico de fórmulas de lógica de primeira ordem, e, se existe um predicado que satisfaz essas fórmulas, então NF é consistente
Outro risco são bugs no próprio Lean. Isso não é algo sem precedentes em provadores de teoremas 1
Talvez seja difícil esbarrar nisso por acaso, mas colaborações em larga escala nas quais pessoas aleatórias preenchem etapas, como em 3, estão ficando cada vez maiores. Pode se tornar preocupante a situação em que alguém atrapalhe preenchendo uma etapa com um bug que descobriu
Do ponto de vista dos fundamentos, também é importante que esta prova seja uma prova de equiconsistência entre NF e o kernel do Lean. O próprio kernel do Lean é revisado por humanos
Provadores de teoremas mecanizados preservam o nível de correção injetado por humanos ou por outros sistemas externos
Se não estou enganado, este parece ser o primeiro caso em que o status de uma prova difícil que permaneceu ambíguo por anos foi resolvido por um assistente de prova
Houve projetos que verificaram provas existentes nas quais software não confiável assumia um grande componente computacional, como o teorema das quatro cores em Coq, mas acho que esta é a primeira vez em que o próprio status epistemológico do resultado era incerto para a comunidade matemática mais ampla
Também me vem à mente o Liquid Tensor Experiment
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
É uma situação parecida com a conjectura de Kepler (https://en.m.wikipedia.org/wiki/Kepler_conjecture)
A prova já era conhecida, mas, até ser formalizada, não havia certeza de que estava correta
A próxima parece ser a conjectura abc
Foi alegadamente provada em 2012 e há um artigo de mais de 400 páginas online, mas parece que não há muita gente que aceite essa prova
Alguém poderia explicar, em linhas gerais, o que há de especial ou novo na formalização da teoria dos conjuntos “New Foundations” em comparação com outras formalizações?
Ou então um link com uma explicação que um estudante de graduação em matemática ou um profissional de engenharia consiga ler também serve
Acho que o ponto central é a existência de um conjunto universal. No meu caso de uso, sistemas de tipos para linguagens de programação, esse tipo de conjunto universal é muito útil
Várias soluções de contorno dos sistemas existentes, como universos cumulativos ou type-in-type, não são satisfatórias. Em vez disso, basta verificar se as assinaturas de tipo são estratificadas e depois esquecer que os tipos têm níveis numéricos
Basicamente, exige-se que o predicado usado para escolher subconjuntos obedeça a um sistema de tipos muito leve. “x não é elemento de si mesmo” não é uma pergunta bem tipada em um sistema de tipos razoável e, em particular, também não satisfaz a exigência de “estratificabilidade” de NF; portanto, não é possível formar o conjunto do paradoxo de Russell, isto é, o conjunto de todos os conjuntos que não contêm a si mesmos
A definição de “estratificável” também não é tão complicada. Em contraste, ZF tem oito axiomas/esquemas de axiomas que parecem bastante improvisados
Fui procurar este texto porque queria saber quais são as diferenças fundamentais entre Coq e Lean, e se eles operam sobre o mesmo tipo de lógica 1
Quase não entendi a discussão e não uso nenhum dos dois na prática. Gostaria de ouvir mais explicações relacionadas ou comparações com outros assistentes de prova
1 https://proofassistants.stackexchange.com/questions/153/what...
Há diferenças, e esta discussão também vale a pena 1
1 https://github.com/coq/coq/issues/10871
Acho que os defensores do Lean às vezes exageram um pouco na forma de se expressar. O Lean não é um método de prova superior, como muitas vezes fica implícito, mas sim uma forma alternativa de provar
Ao tentar aprender Lean, você logo percebe que ele é uma linguagem de programação e um sistema com seus próprios bugs, e que depende bastante de várias pilhas de bibliotecas escritas por outros seres humanos. Essas bibliotecas envolvem escolhas e também podem ter lacunas ou bugs
Por isso, discordo de formulações do tipo “o Lean disse que a prova é boa”. Acho que uma formulação mais precisa e honesta é dizer que a prova escrita foi verificada por matemáticos humanos, e que essa prova foi traduzida por humanos para Lean e verificada também lá. A ideia de que o Lean fornece a única verificação de ouro não é necessariamente correta, ou pelo menos nunca vi uma explicação mostrando isso. O subtítulo “digitalização da prova de Randall Holmes” parece ser a formulação mais precisa
Em um sistema forte como o Lean, uma prova verificada por máquina me parece muito superior a uma prova verificada apenas por humanos. Humanos são incríveis, mas ficam entediados e também deixam passar detalhes
Isso não é só uma afirmação teórica. As pessoas leram os Elementos de Euclides por mais de 2 mil anos antes de perceberem axiomas ausentes. É um erro básico do tipo que um sistema de verificação de provas mecânico funcionando corretamente teria revelado imediatamente
Provas matemáticas publicadas também muitas vezes acabam se mostrando incorretas depois. À medida que a matemática fica cada vez mais sofisticada, torna-se cada vez mais difícil para humanos verificar corretamente todas as etapas. Máquinas ainda não são tão boas quanto humanos para gerar provas, mas são incomparáveis na verificação
Também há sistemas que “competem” com o Lean, então eu não diria que o Lean é “o único caminho verdadeiro”. Por exemplo, também gosto do Metamath. Mas essa “competição” entre esses sistemas precisa de aspas. Cada um tem pontos fortes e fracos, e muita gente gosta, usa ou contribui para vários sistemas. Todos conseguem verificar teoremas com um rigor irrealista para humanos
Pode haver bugs, mas entendo que a única coisa em que precisamos confiar é o kernel
Se “várias pilhas de bibliotecas escritas por outros seres humanos” quer dizer a mathlib, acho que isso não está correto. O código da mathlib também acaba sendo compilado para código processado pelo kernel
O rascunho do artigo no site 0 reforça esse ponto: o Lean é um projeto grande, mas, para garantir que uma prova aceita esteja correta, basta confiar no kernel. Mesmo que uma tática produza um termo de prova incorreto, o kernel tem a oportunidade de detectar esse erro antes de aceitar a prova
A diferença é que, no Lean, basta confiar no kernel. O resto é construído sobre ele. Se o kernel é sólido, todo o resto também é sólido
Isso é muito diferente de uma linguagem de programação comum. Em linguagens comuns, bugs podem entrar a qualquer momento. Também é muito diferente da matemática, em que qualquer lema auxiliar pode conter um erro
O legal dos provadores de teoremas é que, assumindo que o kernel esteja correto, uma prova errada nem sequer compila
Quando se trata de provas, não existem bugs que só aparecem em tempo de execução como no software tradicional. Não há tempo de execução nesse sentido
Também dá para usar Lean como uma linguagem de programação “normal”, e nesse caso há risco de bugs em tempo de execução, mas não é disso que se trata aqui
Você está entendendo mal os provadores de teoremas. Isso não é uma questão do tipo “toda abstração vaza”. Não é preciso confiar nas bibliotecas; basta confiar no kernel
Confiar no kernel também não é algo trivial, mas é um salto enorme em relação a provas informais. Em provas informais, de fato é preciso confiar na “biblioteca”, ou seja, na cultura e no conhecimento de outras pessoas, porque não há uma maneira prática de reduzir tudo efetivamente até os axiomas
ZFC morreu e viva o NF?
Como matemático amador que usa conjuntos principalmente como uma linguagem comum para descrever outras coisas, não sei bem quais são as implicações disso para a matemática em sentido mais amplo. Especialmente se a utilidade do NF for parecida com a do ZFC existente e suas variantes
Espera-se que o NF se torne tão popular quanto o ZFC em provas mecanizadas? A existência de um conjunto universal parece mais intuitiva, então pelo menos essa prova reacendeu meu interesse pessoal por formalização
Do ponto de vista de um amador ingênuo, como todo modelo de ZFC pode ser estendido para um modelo de NF, esse resultado de consistência relativa parece tornar o NF pelo menos tão útil quanto o ZFC
Mas acho que o NF não se tornará muito útil a menos que uma destas coisas aconteça
Provar que o NF é contraditório. Então o ZFC também é contraditório. As estrelas no céu noturno começam a se apagar uma a uma ;)
Provar que o ZFC é contraditório. Então ainda resta a possibilidade de o NF ser consistente. É torcer pela sorte
Claro, é bem possível que eu esteja deixando passar vantagens mais práticas de “qualidade de vida” do NF, como poder falar de classes próprias ou evitar o paradoxo de Russell com fórmulas estratificadas
Não há nenhuma intenção de promover o NF como um sistema fundacional independente. O NF é um sistema bastante peculiar
Ainda assim, se alguém quiser promovê-lo, esse resultado de consistência pelo menos permite dizer que o risco não é maior do que chegar a uma contradição a partir do ZFC
Gostei muito disso
Fico pensando se no fim isso não levará a provas colaborativas e “correção de bugs”, fazendo a matemática virar um processo parecido com código no GitHub
Queria ter tempo livre para acompanhar o projeto mathlib. É muito legal
Existe alguma forma de participar, mesmo que bem de leve?
Você pode começar pelo Natural numbers game
https://adam.math.hhu.de/#/g/leanprover-community/NNG4
Não sou da área, mas não existia o teorema de Gödel, segundo o qual todo sistema suficientemente forte não consegue demonstrar sua própria consistência?
Porém, embora um sistema X não possa provar sua própria consistência, um sistema Y mais forte pode provar a consistência de X. E outro sistema mais forte ainda pode provar a consistência de Y. Assim se forma uma cadeia em que cada sistema prova a consistência de um sistema mais fraco
Isso não prova que o sistema seja absolutamente consistente. Se Y for contraditório, ele pode provar tanto que X é consistente quanto que X é contraditório. Ainda assim, tem valor. Afinal, uma das razões pelas quais usamos Y é justamente que não conhecemos contradições dentro dele. Sistemas formais muitas vezes podem ser contraditórios de maneiras sutis, então “consistente sob a suposição de que outro sistema é consistente” é muito melhor do que “sem nenhuma prova de consistência”
Um sistema contraditório também pode provar sua própria consistência. Portanto, mesmo que um sistema tenha uma prova de que ele próprio é consistente, ainda assim não sabemos se ele é de fato consistente
Também vale conferir a discussão no Reddit com a participação de uma das pessoas que o criou 0
https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...