Implication semilattice of 990 quasigroup equational laws

1. O Problema e o Contexto Histórico

O artigo retoma e conclui um trabalho iniciado há 135 anos por Ernst Schröder (na década de 1890). O objetivo original de Schröder era refutar uma afirmação de Charles Sanders Peirce de que "todos os reticulados são distributivos". Para isso, Schröder analisou um conjunto de 990 leis equacionais em quasigrupos, análogas à associatividade.

• Objetivo: Identificar um reticulado não distributivo que surja naturalmente de um problema matemático.
• O Objeto de Estudo: Quasigrupos, que são análogos não associativos de grupos. Um quasigrupo é um conjunto equipado com uma operação binária ($*$) e operações de divisão conjugada à direita ($//$) e à esquerda ($\\$), onde as multiplicações à direita e à esquerda são bijetivas.
• A Estrutura das Leis: As leis equacionais têm a forma $\forall x, y, z, \quad x?y?z = \alpha?\beta?\gamma$, onde os operadores $?$ são escolhidos entre \{*, //, \\} e as variáveis $\alpha, \beta, \gamma$ são permutações de $x, y, z$. As associações podem ser $(x?y)?z$ ou $x?(y?z)$.
• O Desafio: Schröder estudou subconjuntos específicos dessas leis e mostrou que o reticulado formado por eles falha na lei distributiva. No entanto, ele não classificou todas as implicações lógicas entre as 990 equações. O trabalho de Le Floch visa completar essa classificação.

2. Metodologia

O autor utilizou uma abordagem computacional rigorosa, baseada no Equational Theories Project (Projeto de Teorias Equacionais), combinando prova automática de teoremas e construção de modelos.

• Ferramentas Automatizadas:
  • Prover9: Um provador de teoremas automático usado para encontrar provas de implicações (se $A \implies B$).
  • Mace4: Um construtor de modelos usado para encontrar contraexemplos finitos (quasigrupos que satisfazem $A$ mas não $B$), provando que uma implicação é falsa.
• Estratégia de Busca:
  1. Para cada par de equações (ou conjuntos de equações), o sistema tenta provar a implicação. Se falhar, busca um contraexemplo finito.
  2. Diferentemente de projetos anteriores em magmas (onde alguns contraexemplos exigiam modelos infinitos), neste contexto de quasigrupos, todas as não-implicações admitiram contraexemplos finitos, o que permitiu uma verificação completa e automática.
  3. Scripts Python foram desenvolvidos para gerar as 990 equações, gerenciar as classes de equivalência e calcular o fecho lógico (conjuntos "bons" ou good subsets).
• Definições Chave:
  • Subconjuntos "Bons" (Good Subsets): Conjuntos de leis fechados sob consequências lógicas.
  • Operações no Reticulado:
    • Soma lógica ($A + B$): O menor conjunto "bom" contendo $A \cup B$.
    • Produto ($AB$): A interseção $A \cap B$.
    • Implicação ($A \implies B$): Ocorre se $B \subset A$.

3. Principais Contribuições e Resultados

O trabalho mapeou completamente a estrutura de implicações entre as 990 leis, resultando nas seguintes descobertas:

A. Classificação das Varieties de Quasigrupos

O autor identificou 114 variedades distintas de quasigrupos descritas por subconjuntos dessas leis. Elas foram categorizadas pelo número mínimo de equações necessárias para caracterizá-las:

1. 1 variedade: O conjunto vazio (todos os quasigrupos).
2. 47 variedades: Descritas por uma única equação.
   • O artigo lista 47 representantes de classes de equivalência.
   • Exemplos notáveis incluem:
     • Comutatividade ($x*y = y*x$).
     • Quasigrupos semi-simétricos (onde as três operações coincidem).
     • Leis que implicam linearidade (isomorfismo a estruturas sobre módulos gaussianos ou grupos booleanos).
3. 50 variedades: Requerem exatamente duas equações (não redutíveis a uma).
4. 15 variedades: Requerem exatamente três equações.
5. 1 variedade: Requer pelo menos quatro equações.

B. A Variedade de Quatro Equações

Um dos resultados mais significativos é a identificação de uma variedade que não pode ser definida por menos de quatro equações. Ela é descrita pelo conjunto:

1. $x * (y // z) = y * (x // z)$
2. $x * (y \backslash z) = z * (y \backslash x)$
3. $x // (y \backslash z) = y // (x \backslash z)$
4. $x \backslash (y * z) = y \backslash (x * z)$

Esta variedade é de interesse particular e representa o "ponto mais profundo" da estrutura lógica encontrada.

C. O Reticulado de Implicações

O autor construiu o semirreticulado de implicação completo.

• Foram determinados todos os 114 conjuntos fechados logicamente.
• A estrutura inclui o famoso reticulado de cinco elementos não distributivo identificado por Schröder como um subconjunto menor, mas agora inserido em um contexto muito mais amplo e completo.
• Fornece tabelas completas de quais conjuntos de equações implicam quais outros.

4. Significado e Impacto

• Conclusão de um Problema Histórico: O trabalho finaliza a investigação iniciada por Schröder, transformando uma lista de equações em uma estrutura algébrica completa e compreensível.
• Validação de Métodos Computacionais: Demonstra a eficácia de provaradores de teoremas (ATP) e construtores de modelos na classificação de estruturas algébricas complexas, especialmente quando combinados com a garantia de que contraexemplos finitos são suficientes para refutar implicações.
• Novas Classificações Algébricas: Oferece uma taxonomia detalhada de quasigrupos baseada em leis equacionais específicas, muitas das quais possuem interpretações geométricas ou algébricas profundas (como ações de grupos booleanos ou automorfismos de ordem 3).
• Recursos Abertos: O artigo é acompanhado por arquivos de dados (JSON e TXT) e scripts Python que permitem a reprodução dos resultados e a exploração das 990 equações e suas 114 variedades, servindo como base para futuras pesquisas em álgebra universal.

Em resumo, Bruno Le Floch não apenas "fechou o caso" de Schröder, mas forneceu um mapa completo das relações lógicas entre leis fundamentais de quasigrupos, revelando uma estrutura rica de 114 variedades e confirmando a existência de estruturas não distributivas complexas dentro desse domínio.