Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

Resumo Técnico: Rumo à Semântica Proposicional Automatizada: Semântica de Comportamento-Inferencial para K3 e LP de 3 Dimensões

Enunciado do Problema
A automação do raciocínio lógico está bem estabelecida (por exemplo, via resolução, provadores de teoremas e assistentes interativos como Rocq e Lean), mas a provisão automatizada de semântica de base teórica-provatória (P-tS) para tal raciocínio permanece um desafio em aberto. Enquanto sistemas como o MUltlog podem gerar automaticamente cálculos sequentes, tabelas de verdade e sistemas de dedução natural para quaisquer lógicas de valores finitos a partir de tabelas de verdade metalógicas, eles carecem da capacidade inversa: gerar especificações de significado provatorial para os conectivos dentro desses sistemas. As abordagens de P-tS existentes, como a validade teórica-provatória ou a semântica de extensão de base, são frequentemente dependentes do cálculo, impedindo a comparação dos significados dos conectivos entre diferentes lógicas (por exemplo, clássica vs. intuicionista). O artigo visa integrar a abordagem da Semântica de Comportamento-Inferencial (I-bS) — que modela os significados dos conectivos por meio de seu comportamento inferencial mínimo — ao framework do MUltlog para automatizar a geração de P-tS para lógicas de múltiplos valores.

Metodologia
O artigo estende o framework I-bS, anteriormente limitado a cálculos sequentes de 2 dimensões, para cálculos sequentes de n dimensões. A metodologia procede através das seguintes etapas:

1. Aparelho Formal: O autor define sequentes de $n$ dimensões como $n$-tuplas de multiconjuntos de fórmulas. Para interpretá-los sem recorrer a valores de verdade metalógicos, adotam uma leitura multilateralista. Para sequentes de 3 dimensões (especificamente para a lógica de Kleene Forte, K3, e a Lógica do Paradoxo, LP), isso envolve três atos de fala: asserção (dimensão 1), suspensão de julgamento (dimensão 2) e negação (dimensão 3).
2. Relação de Derivabilidade Mínima: Para isolar o significado dos conectivos das características estruturais de um cálculo específico, o autor define uma relação de derivabilidade mínima consistindo em Identidade ($Id_3$) e uma regra de Corte restrita ($Cut_2$). Isso evita os efeitos de "confundimento" das regras estruturais completas (como Contração e Fraqueza) encontradas em cálculos padrão.
3. Definibilidade e Comportamento Inferencial: Seguindo uma definição no estilo de Belnap, um conectivo é definido se ele estende conservativamente o cálculo base e é unicamente inter-derivável com um correspondente. A métrica central é o comportamento inferencial ($ib$), uma função que rastreia as localizações horizontais (dimensões) e as aplicações de regras de um conectivo durante sua prova de definibilidade.
4. Extensão de Significado: Para comparar conectivos através de diferentes dimensionalidades (por exemplo, 2D clássico vs. 3D paraconsistente), o artigo introduz a extensão de significado. Um conectivo de $m$ dimensões estende o significado de um conectivo de $n$ dimensões ($m > n$) se o comportamento inferencial deste último for conservativamente preservado dentro de um fragmento de $n$ dimensões do primeiro.

Contribuições Principais e Resultados
O artigo aplica este framework estendido a duas lógicas de 3 valores: K3 e LP, utilizando os cálculos sequentes de 3 dimensões gerados pelo MUltlog.

• Cláusulas Semânticas para K3/LP: O autor prova a unicidade e a conservatividade para as versões multiplicativa e aditiva dos conectivos de K3 em relação à relação mínima $\{Id_3, Cut_2\}$. Ele deriva cláusulas semânticas distintas para cada versão de conectivo (por exemplo, conjunção multiplicativa $\otimes$ vs. conjunção aditiva $\sqcap$), demonstrando que os cálculos padrão de K3 confundem conectivos semanticamente distintos devido às suas regras estruturais.
• Identidade dos Significados de K3 e LP: Um resultado central é que os conectivos de K3 e LP possuem significados idênticos. Embora K3 e LP difiram em seus valores designados (K3 designa apenas a dimensão 3; LP designa as dimensões 2 e 3), suas propriedades de derivabilidade vertical e regras operacionais são idênticas. Consequentemente, seus comportamentos inferenciais em provas de definibilidade são idênticos, gerando as mesmas cláusulas semânticas.
• Extensão de Significado da Lógica Clássica: O artigo demonstra que os conectivos de 3 dimensões de K3 e LP são extensões de significado de seus correspondentes clássicos em LK (2 dimensões). Ao projetar as cláusulas semânticas de 3 dimensões sobre a 1ª e a 3ª dimensões (removendo a 2ª dimensão), as regras resultantes são sintaticamente idênticas às cláusulas semânticas dos conectivos de LK clássico. Isso confirma que os conectivos de K3/LP estendem conservativamente os significados clássicos sem alterá-los.
• Tratamento de Regras Estruturais: A análise revela que restrições de contexto (por exemplo, limitar o número de fórmulas nos componentes do sequente) são necessárias para manter o comportamento inferencial mínimo. Sem essas restrições, as regras estruturais padrão (como a Contração) alterariam o comportamento inferencial, efetivamente mudando o significado dos conectivos.

Significância e Alegações
O artigo afirma fornecer o primeiro estudo de caso fundamental para estender o I-bS para dimensões superiores a duas. Sua principal significância reside em:

1. Comparação entre Cálculos: Estabelece um mecanismo para comparar os significados dos conectivos entre lógicas de diferentes dimensionalidades, abordando uma lacuna na literatura anterior de P-tS que tinha dificuldade em comparar lógicas com diferentes propriedades estruturais.
2. Validação do Pluralismo Lógico: A descoberta de que K3 e LP compartilham significados de conectivos idênticos apoia uma visão teórica-provatorial de pluralismo lógico, onde diferentes lógicas podem compartilhar os mesmos significados de conectivos, apesar de possuírem diferentes valores designados ou condições de validade.
3. Caminho para a Automação: Ao mapear com sucesso cálculos de 3 dimensões para o I-bS, o artigo lança as bases para integrar o I-bS ao MUltlog. O objetivo final é automatizar a geração de cláusulas semânticas para qualquer lógica de múltiplos valores. O autor observa que, embora o presente trabalho seja um estudo de caso manual, o framework é desenhado para ser implementado computacionalmente, permitindo potencialmente a geração automatizada de semântica teórica-provatória para quaisquer lógicas de múltiplos valores.

O autor permanece modesto quanto à automação imediata de todo o processo, reconhecendo que gerar as provas de definibilidade necessárias para cálculos arbitrários de $n$ dimensões permanece um desafio computacional, embora o framework teórico já esteja estabelecido.