Resumo Técnico: Semântica de Comportamento de Inferência para Todas as Conectivas em Cálculos Sequentes Bidimensionais

1. Enunciado do Problema

O artigo aborda um desafio central da Semântica de Prova-Teórica (P-tS): como fornecer explicações semânticas invariantes de significado para conectivas lógicas através de diferentes sistemas lógicos (por exemplo, lógicas clássica, intuicionista, linear e dual-intuicionista). As abordagens tradicionais, como a Semântica de Modelo-Teórica (M-tS) e a Semântica de Extensão de Base (B-eS), frequentemente sofrem de "globalismo", onde mudar a lógica exige mudar o significado das conectivas (por exemplo, o 'e' clássico versus o 'e' intuicionista). Isso leva a uma situação em que os desacordos lógicos são reduzidos a meros problemas de comunicação devido a definições divergentes, em vez de desacordos substantivos sobre conceitos compartilhados.

O problema específico que este artigo aborda é a falta de uma implementação técnica sistemática da Semântica de Comportamento de Inferência (I-bS), uma abordagem recente proposta por Nagler [Nag26]. Embora a I-bS ofereça um arcabouço promissor para isolar o "comportamento de inferência mínimo" de uma conectiva para definir seu significado, ela carecia anteriormente de uma avaliação técnica abrangente através do espaço de possíveis regras de conectivas. O artigo visa validar a I-bS aplicando-a a um vasto conjunto não estruturado de conectivas candidatas para determinar quais, se houver, possuem significados mínimos distintos, independentes de regras estruturais específicas (como enfraquecimento ou contração).

2. Metodologia

O estudo emprega uma abordagem rigorosa e orientada por dados para medir o "significado" das conectivas com base em seu uso inferencial em um cenário mínimo.

2.1 Objeto de Investigação: Todas as* Conectivas

Os autores definem o escopo da investigação como todas as conectivas*: pares de regras operacionais formuláveis em cálculos sequentes bidimensionais sujeitos às seguintes restrições:

• Regras Operacionais: Devem ser separadas, explícitas e simétricas (Definição 3).
• Restrições: No máximo duas sequentes de premissas e no máximo duas fórmulas ativas por regra.
• Espaço Total: Isso resulta em exatamente 10.816 pares de regras sintaticamente únicos (combinações de formas de premissas e posições de fórmulas ativas).

2.2 Ambiente de Teste: Relação de Derivabilidade Mínima

Para isolar o significado de uma conectiva das características estruturais de lógicas específicas, os autores utilizam um cálculo de fundo mínimo consistindo em:

• Identidade ($Id_{pr}$): Restrita apenas a fórmulas primitivas.
• Corte ($Cut_{cd}$): Uma regra de Corte que diferencia contextos.
• Suposições Estruturais: O cálculo assume Troca (multiconjuntos), mas exclui Enfraquecimento e Contração. Isso representa o "núcleo subestrutural" comum a muitas lógicas.

2.3 Dispositivo de Medição: Comportamento de Inferência

A métrica central é o comportamento de inferência, definido como o padrão sintático que uma conectiva exibe quando sua definibilidade é provada dentro do cálculo mínimo.

• Critérios de Definibilidade: Seguindo Belnap [Bel62], uma conectiva é definível se sua adição ao cálculo resultar em uma extensão conservativa (nenhum novo teorema sem a conectiva) e unicidade (a conectiva é unicamente determinada até o isomorfismo).
• Cláusula Semântica: O "significado" de uma conectiva é identificado como seu par de regra operacional mínimo que produz o perfil de comportamento de inferência mínimo (a lista mais curta de posições de componentes ocupadas pela conectiva e suas fórmulas ativas durante uma prova de definibilidade).

2.4 Geração e Análise de Dados

Os autores filtram sistematicamente os 10.816 candidatos:

1. Filtro 1 (Formulabilidade): Todos os 10.816 pares de regras.
2. Filtro 2 (Conservatividade): Provando a eliminação de Corte para os casos positivos e construindo contraexemplos para os não conservativos. Isso reduz o conjunto para 376 conectivas conservativas.
3. Filtro 3 (Unicidade): Estabelecendo interderivabilidade horizontal e vertical. Isso reduz ainda mais o conjunto para 150 conectivas unicamente definíveis.
4. Análise de Minimalidade: Entre as 150 conectivas definíveis, os autores distinguem entre conectivas "mínimas" e "bloatnectives" (conectivas equivalentes com redundâncias sintáticas). Ao aplicar critérios para a minimalidade do tipo de premissa (menor cardinalidade de sequentes de premissas), eles isolam as cláusulas semânticas verdadeiramente mínimas.

3. Contribuições Principais e Resultados

3.1 Identificação de 21 Conectivas Minimamente Significativas

O resultado primário é a identificação de exatamente 21 conectivas minimamente significativas. Estas correspondem a constantes lógicas familiares e seus conversos/inversos, mas com distinções precisas entre versões aditivas (reticuladas) e multiplicativas (grupais):

• Nulárias: Falso ($\bot$) e Verdadeiro ($\top$).
• Unárias: Duas formas de negação (Negação Intuicionista $\neg$ e Dual-Intuicionista $\sim$), e uma negação inversa "trivial".
• Binárias:
  • Conjunção: Aditiva ($\sqcap$) e Multiplicativa ($\otimes$).
  • Disjunção: Aditiva ($\sqcup$) e Multiplicativa ($\oplus$).
  • Implicação: Direita Aditiva ($\rightsquigarrow$), Direita Multiplicativa ($\to$), Esquerda Aditiva e Esquerda Multiplicativa.
  • Conversos e Inversos: Cada uma das acima possui cláusulas semânticas distintas para seus conversos (troca de componentes) e inversos.

3.2 Cláusulas Semânticas e Arcabouços

O artigo fornece cláusulas semânticas explícitas (pares de regras mínimas) para cada uma das 21 conectivas. Crucialmente, demonstra que esses significados são independentes da lógica. Por exemplo, a cláusula semântica para a conjunção multiplicativa ($\otimes$) é a mesma, quer ela apareça na Lógica Linear, na Lógica Clássica ou na Lógica Intuicionista. As diferenças em como essas conectivas se comportam em lógicas completas (por exemplo, a equivalência de $\otimes$ e $\sqcap$ na Lógica Clássica) são atribuídas a recursos estruturais (como Contração e Enfraquecimento), e não a uma mudança no significado central da conectiva.

3.3 Inter-relações Semânticas entre Lógicas

O estudo mapeia a compatibilidade semântica dessas 21 conectivas através de várias lógicas:

• Lógica Clássica (LK): Conflui as versões aditivas e multiplicativas de conjunção, disjunção e implicação. Também conflui as duas formas de negação.
• Lógica Intuicionista (LJ): É compatível com as versões aditivas de conjunção e disjunção, e com a implicação "direita", mas captura apenas metade do significado da negação clássica (especificamente $\neg_{min}$, excluindo $\sim_{min}$).
• Lógica Dual-Intuicionista (LDJ): Captura a outra metade da negação clássica ($\sim_{min}$) e os duais das outras conectivas.
• Lógica Linear (LL): Distingue todas as 21 conectivas, tratando-as como semanticamente distintas.

3.4 Validação da I-bS

O artigo afirma validar a estrutura da Semântica de Comportamento de Inferência ao demonstrar que, quando aplicada a uma busca cega e exaustiva de regras possíveis sem viés para qualquer lógica específica, a teoria converge naturalmente para as conectivas padrão encontradas nos sistemas lógicos estabelecidos. O fato de que o "ruído" (os outros 10.795 pares de regras) é filtrado como não definível ou não mínimo serve como um "teste de sanidade" para a teoria.

4. Significância e Alegações

O artigo posiciona suas descobertas como uma verificação do arcabouço de Semântica de Comportamento de Inferência. Sua significância reside em:

1. Independência de Lógica: Fornece um método para definir significados de conectivas que são invariantes entre diferentes lógicas. Mudar a lógica (por exemplo, adicionar Enfraquecimento) não muda o significado da conectiva; apenas muda o contexto estrutural no qual a conectiva opera.
2. Resolução da Mudança de Significado: Oferece uma explicação semântica para o porquê de as lógicas clássica e intuicionista parecerem discordar. Elas não necessariamente discordam sobre o significado de "e" ou "ou"; em vez disso, diferem em quais conectivas mínimas permitem que interajam e quais regras estruturais permitem. Por exemplo, o "e" clássico é uma conflação de dois significados mínimos distintos ($\otimes$ e $\sqınd$); enquanto o "e" intuicionista é estritamente $\sqınd$.
3. Frugalidade Ontológica: O método não requer modelos ou bases externas, baseando-se apenas no núcleo subestrutural do sistema de prova.
4. Exaustividade: Ao cobrir todo o espaço de regras formuláveis sob as restrições dadas, o artigo afirma ter fornecido uma taxonomia completa de significados de conectivas mínimas em cálculos sequentes bidimensionais.

Os autores mantêm a modéstia quanto ao escopo, observando que os resultados são relativos às restrições específicas (duas premissas, duas fórmulas ativas, cálculo mínimo específico) e que trabalhos futuros podem explorar cálculos multidimensionais, quantificação ou relações de derivabilidade mínima alternativas. No entanto, dentro do escopo definido, o artigo afirma que a I-bS isola com sucesso os significados primitivos das conectivas lógicas.