Resumo Técnico: Semântica Doutrinal da Lógica de Primeira Ordem Direcionada

1. Declaração do Problema

O artigo aborda o desafio de formalizar a igualdade direcionada dentro de um quadro lógico. Enquanto a perspectiva categórica de Lawvere caracterizou com sucesso a igualdade clássica como um adjunto esquerdo à contração, essa abordagem depende da simetria. Na teoria dos tipos direcionada, onde os tipos são interpretados como categorias (ou pré-ordens) em vez de grupoides (ou conjuntos), a igualdade torna-se uma relação assimétrica (por exemplo, uma reescrita $a \to b$ ou uma ordem $a \le b$).

A dificuldade central reside no manuseio da variância (polaridade). Em um cenário direcionado, uma variável pode aparecer em uma posição "negativa" (contravariante, por exemplo, a fonte de um morfismo) ou em uma posição "positiva" (covariante, por exemplo, o alvo). As regras lógicas padrão para igualdade (reflexividade e a regra J/eliminação) falham neste contexto porque assumem implicitamente a simetria ou permitem que variáveis apareçam em ambas as polaridades simultaneamente de maneiras que derivariam a simetria ($a \le b \vdash b \le a$), o que é inválido na lógica direcionada. Tentativas anteriores de teoria dos tipos direcionada frequentemente lutam com essas restrições de polaridade, particularmente no contexto da lógica irrelevante para provas (onde a igualdade é uma proposição, e não um tipo com múltiplos habitantes).

2. Metodologia

Os autores desenvolvem uma lógica de primeira ordem direcionada (dFOL) e sua semântica doutrinal generalizando o quadro de hiperdoctrinas de Lawvere.

Sintaxe: Contextos Polarizados

A sintaxe introduz um contexto polarizado $[\Theta \mid \Delta \mid \Gamma]$, particionando variáveis em três conjuntos com base em sua variância:

• $\Theta$ (Negativo): Variáveis que aparecem apenas em posições contravariantes.
• $\Gamma$ (Positivo): Variáveis que aparecem apenas em posições covariantes.
• $\Delta$ (Dinatural): Variáveis que aparecem em ambas as posições (ou permitidas para serem tratadas como tal).

Recursos sintáticos chave incluem:

• Igualdade Direcionada ($\le_A$): Uma relação primitiva $s \le_A t$ onde $s$ é tipada no contexto negativo e $t$ no contexto positivo.
• Implicação Polarizada: A implicação $\psi \Rightarrow \phi$ troca a polaridade do contexto para $\psi$ (movendo-o da esquerda para a direita do turno), refletindo a contravariância do primeiro argumento.
• Quantificadores Polarizados: Quantificadores ($\forall^p, \exists^p$) são indexados por polaridade $p \in \{-, \Delta, +\}$ para rastrear a variância da variável ligada.
• Regras de Substituição: Um mecanismo de substituição especializado (Definição 2.7) trata o reindexamento de termos através de contextos polarizados, garantindo que variáveis dinaturais sejam substituídas consistentemente.

Semântica: Doutrinas Direcionadas

A semântica é capturada via doutrinas direcionadas, uma generalização das doutrinas de Lawvere.

• Categoria Base: Em vez de uma categoria padrão de tipos, a base é uma categoria de polarização $ndp(\mathcal{C})$, cujos objetos são triplas $(\Theta, \Delta, \Gamma)$ e morfismos respeitam a estrutura de variância.
• Estrutura Fibrada: Um functor $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ mapeia contextos polarizados para posets de fórmulas.
• Condições Chave:
  • Sem-Variância-Dinatural (ndv): Uma condição garantindo que variáveis dinaturais em predicados surjam apenas da colapso de variáveis positivas e negativas, prevenindo tipos "terceiros" de variância.
  • Adjunções Relativas: A igualdade direcionada é caracterizada não como um adjunto esquerdo padrão, mas como um adjunto esquerdo relativo a uma operação semelhante à contração que colapsa duas variáveis de polaridade oposta em uma única variável dinatural. Isso captura a restrição sintática que previne a derivação da simetria.
  • Implicação Polarizada: Caracterizada como um coadjunto relativo.

3. Contribuições Chave

1. Sintaxe da dFOL: Um sistema preciso de dedução natural para lógica de primeira ordem com igualdade direcionada, apresentando um sistema rigoroso de polaridades inspirado na dinaturalidade. Este sistema proíbe explicitamente a derivação da simetria para igualdade direcionada enquanto mantém conectivos lógicos padrão.
2. Caracterização da Igualdade Direcionada: O artigo generaliza o "igualdade como adjunto esquerdo" de Lawvere para igualdade direcionada como adjunto esquerdo relativo. Isso fornece uma propriedade universal categórica precisa para igualdade direcionada que leva em conta a assimetria da relação.
3. Doutrinas Direcionadas: A introdução de doutrinas direcionadas como um quadro semântico. Os autores provam que a sintaxe da dFOL é sólida e completa em relação a esta semântica.
4. Completude de Pré-ordem: Um resultado específico de completude é provado para o fragmento clássico da dFOL em relação ao modelo padrão de pré-ordens ($\mathbf{Preord}$). Isso estabelece que qualquer implicação válida em todos os modelos de pré-ordem é derivável na sintaxe.
5. Manuseio da Polaridade: O artigo demonstra como gerenciar variância em um cenário irrelevante para provas, distinguindo-o de teorias de tipos direcionadas relevantes para provas (como aquelas em $\mathbf{Cat}$) usando fibrados posetais e fibras com valores em posets.

4. Resultados

• Sólidade e Completude: Os autores estabelecem uma bi-adjunção entre a categoria de teorias ($\mathbf{Theory}$) e a 2-categoria de doutrinas direcionadas ($\mathbf{DDoctrine}$). Isso implica que a dFOL é a linguagem interna das doutrinas direcionadas.
• Completude para Pré-ordens: Usando uma construção ao estilo de Henkin adaptada para contextos polarizados, o artigo prova que o fragmento clássico da dFOL é completo em relação ao modelo de pré-ordens. A construção define o domínio do modelo como o conjunto de termos fechados ordenados pela derivabilidade da igualdade direcionada ($\le_A$).
• Regras Derivadas: O sistema suporta regras derivadas para transitividade, reflexividade e congruência da igualdade direcionada, bem como regras de interação entre quantificadores polarizados e implicação.
• Contraexemplos: O artigo ilustra que a simetria ($a \le b \vdash b \le a$) não é derivável, e o modelo de pré-ordem serve como um contra-modelo para tais derivações.

5. Significado e Alegações

O artigo afirma avançar o trabalho de Lawvere sobre o papel da variância e dos funtores hom na lógica. Especificamente:

• Fornece uma caracterização sintática e semântica precisa da igualdade direcionada em um cenário irrelevante para provas, preenchendo uma lacuna entre a lógica clássica e a teoria dos tipos direcionada.
• Generaliza o conceito de igualdade como um adjunto para o caso direcionado via adjunções relativas, oferecendo uma nova ferramenta categórica para entender estruturas direcionadas.
• Demonstra que a lógica direcionada pode ser tratada com técnicas lógicas padrão (como completude de Henkin) gerenciando cuidadosamente polaridades através de contextos polarizados, em vez de exigir maquinaria geométrica complexa ou de alta categoria.
• O trabalho é posicionado como um passo fundamental para o raciocínio sobre sistemas de reescrita e fenômenos direcionados (processos, transições) dentro de um quadro lógico, distinto das abordagens relevantes para provas da Teoria dos Tipos Homotópica.

Os autores afirmam explicitamente que seu foco é no caso irrelevante para provas, justificado pela natureza da lógica de reescrita (onde uma reescrita acontece ou não) e pelo uso de fibrados posetais na lógica categórica. Eles não afirmam resolver a complexidade total da teoria dos tipos direcionada dependente, mas fornecem uma base robusta para o caso de primeira ordem baseado em pré-ordens.