Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

Resumo Técnico: Quatro Paradoxos e um Assistente de Prova

Declaração do Problema
O artigo aborda os limites fundamentais do Cálculo de Construções Indutivas (CIC), a teoria de tipos que sustenta o assistente de prova Rocq (anteriormente Coq). Embora a consistência do CIC seja bem estabelecida, as decisões de design específicas que previnem inconsistências — particularmente no que diz respeito à impredicatividade, restrições de universo e eliminação grande — são frequentemente tratadas como restrições de engenharia abstratas. A biblioteca coq-paradoxes, distribuída com o Rocq, contém quatro derivações mecanizadas de False (Burali-Forti, Diaconescu, Reynolds e Hurkens) que dependem de hipóteses rejeitadas pelo núcleo do Rocq. O problema central é interpretar essas derivações não meramente como curiosidades históricas ou inconsistências isoladas, mas como uma "especificação negativa" que delimita com precisão onde o núcleo deve traçar suas linhas para manter a correção.

Metodologia
O artigo emprega uma leitura atenta do código-fonte dentro da biblioteca coq-paradoxes, analisando especificamente quatro arquivos: BuraliForti.v, diaconescu.v, Reynolds.v e Hurkens_Set.v. A metodologia envolve:

1. Desconstrução da Mecânica Compartilhada: Analisar Logics.v para entender o predicado de acessibilidade (ACC) e a infraestrutura de boa fundação utilizadas por múltiplos paradoxos.
2. Rastreamento das Derivações: Seguir os passos lógicos em cada arquivo para identificar a hipótese específica (por exemplo, um tipo universal de relações, um princípio de escolha ou uma injeção de Prop para uma única proposição) que leva a uma contradição.
3. Mapeamento para Rejeições do Núcleo: Correlacionar o ponto de contradição na formalização com o mecanismo específico no núcleo do Rocq (aritmética de universos, regras de eliminação ou verificações de impredicatividade) que impede a construção de ser compilada.
4. Síntese de Decisões de Design: Agregar as descobertas para extrair três condições de fronteira unificadas que governam o comportamento do núcleo.

Principais Contribuições e Resultados

O artigo analisa quatro paradoxos específicos, demonstrando como cada um expõe uma vulnerabilidade distinta na teoria de tipos se certas escolhas de design fossem alteradas:

1. Paradoxo de Burali-Forti (BuraliForti.v):

   • Mecanismo: Assume um tipo universal de relações $A_0$ e uma injeção $i_0$ que mapeia relações para elementos de $A_0$. Isso permite a construção de um "ordinal de todos os ordinais" ($\Omega$) que é embutido em si mesmo.
   • Rejeição pelo Núcleo: O paradoxo depende de instanciar $A_0$ com ele mesmo. O núcleo do Rocq impõe estratificação estrita de universos ($Type_j < Type_i$) para impedir que um tipo contenha sua própria imagem. A construção aciona um erro de "Inconsistência de Universo" porque o nível de universo exigido para o tipo interno deve ser pelo menos tão grande quanto o tipo externo, violando as restrições cumulativas do núcleo.
   • Resultado: Estabelece a necessidade de restrições de hierarquia de universos para impedir definições de tipos autorreferenciais que levam a contradições de ponto fixo.

2. Paradoxo de Diaconescu (diaconescu.v):

   • Mecanismo: Usa uma versão tipada do Axioma da Escolha (Tchoice) sobre uma relação de equivalência em bool definida por uma proposição $P$. A função de escolha $f: bool \to bool$ é usada para decidir $P$ comparando $f(\text{true})$ e $f(\text{false})$.
   • Rejeição pelo Núcleo: O argumento extrai uma decisão computacional (uma função em Set) de uma prova existencial em Prop. Isso constitui "eliminação grande" de Prop para Set.
   • Resultado: Demonstra que permitir o Axioma da Escolha em Set (ou eliminação grande de Prop para Set) força a Lei do Terceiro Excluído (LEM) no sistema construtivo. O núcleo restringe a eliminação grande para impedir essa importação de lógica clássica para a camada computacional.

3. Paradoxo de Reynolds (Reynolds.v):

   • Mecanismo: Reformula o resultado de Reynolds de que o Sistema F não possui um modelo teórico de conjuntos. Assume uma injeção $I: Prop \to Heyt$ (onde $Heyt$ é uma única proposição) e constrói uma pré-álgebra inicial (codificação de Church) para um funtor $\Phi$. Usando o teorema do ponto fixo de Lawvere, deriva um ponto fixo para a negação, levando a False.
   • Rejeição pelo Núcleo: A construção depende da impredicatividade de Prop (quantificando sobre todas as proposições dentro de Prop). No entanto, o paradoxo requer uma injeção de Prop para uma única proposição, o que o núcleo rejeita por motivos de universo antes que a contradição lógica possa ser alcançada.
   • Resultado: Destaca o papel da impredicatividade em Prop. Embora Prop seja impredicativo, o núcleo impede as injeções estruturais específicas que permitiriam que o argumento diagonal de Cantor colapsasse o universo de proposições.

4. Paradoxo de Hurkens (Hurkens_Set.v):

   • Mecanismo: Uma adaptação da simplificação de Hurkens do paradoxo de Girard. Assume um retração entre Prop e bool (via negação dupla) e usa a impredicatividade de Set (se habilitada) combinada com eliminação grande para construir uma relação bem-fundada autorreferencial que leva a False.
   • Rejeição pelo Núcleo: O paradoxo requer tanto impredicatividade em Set quanto eliminação grande (extração de booleanos de conteúdo proposicional). O núcleo padrão do Rocq mantém Set predicativo e restringe a eliminação grande de Prop.
   • Resultado: Mostra que a combinação de impredicatividade e eliminação grande em Set é inconsistente com a lógica clássica (LEM). A decisão do núcleo de manter Set predicativo e restringir a eliminação é a salvaguarda.

Significado e Alegações

O artigo argumenta que o pacote coq-paradoxes serve como uma especificação negativa do núcleo do Rocq. Em vez de apenas listar inconsistências, o pacote fornece uma prova formal por exemplo falho da correção do núcleo.

• Três Condições de Fronteira: O artigo sintetiza os quatro paradoxos em três decisões de design específicas impostas pelo núcleo:

  1. Hierarquia de Universos: Impede que tipos quantifiquem sobre si mesmos de uma maneira que crie pontos fixos (Burali-Forti).
  2. Posicionamento da Impredicatividade: Confina a quantificação impredicativa a Prop (e opcionalmente a Set com ressalvas), impedindo as contradições de Reynolds e Hurkens.
  3. Disciplina da Eliminação Grande: Restringe a extração de conteúdo computacional (como bool ou funções em Set) de provas proposicionais, impedindo as contradições de Diaconescu e Hurkens.

• Papel Meta-matemático: O artigo alega que o pacote é uma peça única de meta-matemática escrita dentro do sistema que documenta. Ele não prova teoremas para aplicação, mas prova a insatisfatibilidade de hipóteses específicas. A "recusa" do núcleo é mostrada como uma consequência de políticas uniformes (aritmética de universos, regras de eliminação) em vez de correções ad hoc.

• Conclusão: O significado reside em demonstrar que a recusa do núcleo do Rocq em compilar essas construções não é arbitrária, mas é o mecanismo estrutural preciso necessário para manter a consistência do CIC. O pacote valida que as decisões de design do núcleo são tomadas pelas "razões certas", efetivamente traçando a fronteira do sistema de fora para dentro.