The calculus of neo-Peircean relations

1. Problema e Contexto

O artigo aborda o Cálculo de Relações (CR), introduzido por De Morgan e Peirce no século XIX como uma extensão da álgebra de classes de Boole. O CR é uma linguagem matemática rigorosa para combinar relações usando operações algébricas, mas possui limitações históricas fundamentais:

• Baixa Expressividade: O CR tradicional é estritamente menos expressivo que a Lógica de Primeira Ordem (LPO/FOL), pois carece de quantificadores.
• Incompletude Axiomática: Em 1941, Tarski questionou se o CR possuía uma axiomatização completa. Respostas posteriores (teoremas de "no-go") mostraram que não existe uma axiomatização finita completa para o CR ou para muitos de seus fragmentos.
• Dependência de Sintaxe Tradicional: O CR tradicional baseia-se em sintaxe cartesiana (árvores de termos), que exige tratamento explícito de variáveis, escopos e substituições, o que pode ser burocrático e difícil de automatizar.

O objetivo do artigo é superar essas limitações criando um sistema que mantenha os benefícios do CR (sem quantificadores explícitos, provas puramente equacionais) mas que seja tão expressivo quanto a LPO e possua uma axiomatização completa e finita.

2. Metodologia

Os autores propõem uma mudança de paradigma da sintaxe tradicional (cartesiana) para uma sintaxe diagramática (monoidal), utilizando diagramas de cordas (string diagrams). A metodologia baseia-se na teoria das categorias, especificamente na combinação de estruturas algébricas conhecidas:

1. Transição para Relações Arbitrárias: Em vez de focar apenas em relações binárias ($X \times X$), o sistema lida com relações de aridade e coaridade arbitrárias ($X^n \times X^m$).
2. Estruturas Categóricas Fundamentais:
   • Bicategorias Cartesianas: Capturam a fragmento existencial-conjuntivo da lógica (quantificadores existenciais e conjunção). Utilizam estruturas de comonoides (cópia e descarte) que são adjuntos à esquerda dos monoides.
   • Bicategorias Cocartesianas: Capturam o fragmento universal-disjuntivo (quantificadores universais e disjunção). São o "negativo fotográfico" das cartesianas.
   • Bicategorias Lineares: Unificam as duas composições anteriores (composição branca e preta) através da distributividade linear, uma propriedade conhecida de Peirce.
3. Bicategorias de Primeira Ordem (fo-bicategories): O núcleo da contribuição é a definição de uma nova estrutura que combina as propriedades das bicategorias cartesianas, cocartesianas e lineares. Isso inclui:
   • Adjunção Linear: A relação entre os monoides/comonoides brancos e pretos é estabelecida via adjunção linear.
   • Leis de Frobenius Lineares: Equações que governam a interação entre as estruturas brancas e pretas.
   • Semântica de Funtores: A semântica é dada por funtores que mapeiam a categoria livre gerada pelos diagramas para a categoria de conjuntos e relações ($Rel$).

3. Principais Contribuições

O Cálculo das Relações Neo-Peirceanas (NPR)

Os autores introduzem o NPR, um cálculo de diagramas de cordas onde:

• Sintaxe: Não há variáveis nem quantificadores. A lógica é expressa através da topologia dos diagramas (conectividade, cores branca e preta, espelhamento).
• Operações:
  • Branco (White): Representa a lógica clássica existencial/conjuntiva (cópia, descarte, composição usual).
  • Preto (Black): Representa a lógica universal/disjuntiva (dual do branco).
  • Adição de Cores: A negação é representada pela inversão de cores (negativo fotográfico) e o espelhamento representa a relação inversa.
• Expressividade: O NPR é tão expressivo quanto a Lógica de Primeira Ordem (LPO) completa.

Axiomatização Completa

O artigo prova que o sistema de axiomas das fo-bicategories (Bicategorias de Primeira Ordem) fornece uma axiomatização completa e finita para a LPO.

• Isso contorna os teoremas de impossibilidade de Tarski e Monk, pois o NPR não é apenas uma reescrita do CR, mas uma extensão mais expressiva que permite capturar a LPO inteira através da interação de estruturas algébricas.
• A prova de completude é uma adaptação diagramática da prova de Henkin para o teorema da completude de Gödel.

Tratamento de Modelos Vazios

Uma inovação significativa é a permissão de modelos com domínio vazio.

• Na LPO clássica, domínios vazios são frequentemente proibidos. No NPR, modelos vazios correspondem naturalmente à lógica proposicional.
• Isso permite uma generalização do teorema da completude de Gödel, cobrindo tanto teorias não triviais (domínio não vazio) quanto teorias triviais (domínio vazio, equivalentes à lógica proposicional).

Conexões Históricas e Teóricas

• Peirce: O sistema valida e formaliza as intuições de Charles S. Peirce sobre seus Existential Graphs (Gráficos Existenciais), mostrando que as equações de Frobenius e a distributividade linear já estavam presentes em seus trabalhos, mas agora têm fundamentação categórica sólida.
• Tarski e Quine: O sistema fornece uma codificação completa para o Cálculo de Relações de Tarski e para a Lógica de Funtores de Predicados de Quine (PFL), resolvendo a questão da axiomatizabilidade de Tarski ao mudar a sintaxe.

4. Resultados Chave

1. Teorema da Completude (Teorema 3.5): Para quaisquer termos $c$ e $d$, a inclusão semântica ($c \leq d$) é equivalente à inclusão sintática derivável ($c \lesssim d$) usando os axiomas das fo-bicategories.
2. Correspondência com LPO: Existe uma codificação semântica preservadora entre fórmulas de LPO e diagramas do NPR, e vice-versa.
3. Prova de Completude: A prova demonstra que qualquer teoria não contraditória possui um modelo, dividindo o caso em:
   • Teorias não triviais (usando a construção de modelos de Henkin).
   • Teorias triviais (domínio vazio, onde o sistema se reduz ao cálculo de estruturas de inferência profunda para lógica proposicional).
4. Simplificação de Casos de Borda: O sistema lida naturalmente com casos como a negação de quantificadores e a interação entre variáveis livres e ligadas sem a necessidade de renomeação de variáveis (alpha-conversion) ou substituição evitativa de captura.

5. Significado e Impacto

• Para a Lógica: O trabalho oferece uma nova fundação para a LPO baseada em álgebra e diagramas, eliminando a necessidade de quantificadores explícitos e variáveis, o que simplifica a teoria e a implementação em assistentes de prova.
• Para a Ciência da Computação:
  • Assistentes de Prova: A natureza puramente equacional e diagramática torna o sistema ideal para automação e verificação formal.
  • Semântica de Linguagens de Programação: Oferece ferramentas para modelar linguagens com efeitos, computação quântica (onde a cópia de dados é proibida, exigindo estruturas lineares) e sistemas distribuídos.
  • Bancos de Dados: Pode impactar a teoria de consultas e otimização de consultas, dada a relação histórica entre álgebra relacional e LPO.
• Para a Teoria das Categorias: Introduz as fo-bicategories como uma nova estrutura unificadora que combina lógica, álgebra e topologia, servindo como um "código de cores" para a lógica clássica.

Em resumo, o artigo demonstra que, ao abandonar a sintaxe cartesiana tradicional em favor de uma sintaxe diagramática baseada em bicategorias lineares e cartesianas, é possível recuperar a completude axiomática perdida no Cálculo de Relações clássico, criando um sistema unificado, expressivo e matematicamente elegante para a Lógica de Primeira Ordem.