💻 computer science

Labelled Sequent Calculi for Propositional Team Logics

Este artigo apresenta cálculos de sequente rotulados sãos e completos com regras estruturais admissíveis e procedimentos de busca de prova terminantes para quatro lógicas de equipe proposicionais, incluindo a lógica inquisitiva básica e a lógica de dependência intuicionista proposicional, juntamente com suas extensões de disjunção tensor.

Autores originais: Fausto Barbero, Marianna Girlando, Valentin Müller, Fan Yang

Publicado 2026-07-01

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Fausto Barbero, Marianna Girlando, Valentin Müller, Fan Yang

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você esteja tentando resolver um enigma de lógica. Da maneira tradicional de fazer isso (chamada de "semântica tarskiana"), você olha para o enigma a partir de apenas um ângulo específico. Você pergunta: "Esta afirmação é verdadeira bem aqui, neste único lugar?"

Mas os autores deste artigo estão trabalhando com um tipo diferente de lógica chamado Semântica de Equipes (Team Semantics). Em vez de olhar para um único lugar, imagine que você está olhando para uma equipe inteira de pessoas paradas juntas. Você não está perguntando se uma afirmação é verdadeira para apenas uma pessoa; você está perguntando se ela é verdadeira para todo o grupo agindo em conjunto.

Essa abordagem de "equipe" é usada em cenários do mundo real, como descobrir como as variáveis dependem umas das outras em um banco de dados (ex: "O preço depende da cor?") ou entender o significado de perguntas na linguagem (ex: "É verdade que está chovendo OU é verdade que está nevando?").

O Problema: Como Provar Coisas Sobre Equipes

Os autores queriam criar um conjunto de regras (uma "calculadora") para provar se afirmações sobre essas equipes são verdadeiras ou falsas. Eles chamam isso de Cálculos de Sequentes Rotulados (Labelled Sequent Calculi).

Pense em um "sequente" como uma balança de pratos. De um lado, você tem uma lista de fatos que conhece (o estado atual da equipe). Do outro lado, você tem uma conclusão que deseja provar. O objetivo é mostrar que, se os fatos à esquerda forem verdadeiros, a conclusão à direita também deve ser verdadeira.

O artigo apresenta quatro "calculadoras" (sistemas de prova) específicas para quatro tipos diferentes de lógica de equipe:

Lógica Inquisitiva Básica: A lógica de equipe padrão para perguntas.
Lógica de Dependência Intuicionista Proposicional: Lógica de equipe que lida com "dependência" (como "A depende de B").
Duas Versões Estendidas: Estas adicionam uma "Disjunção Tensor" especial (uma forma sofisticada de dizer "dividir a equipe em dois grupos separados para verificar coisas diferentes").

As Ferramentas: Rótulos como Membros da Equipe

Para fazer esses cálculos funcionarem, os autores usam rótulos.

Imagine que cada membro da sua equipe tem um crachá.
Alguns crachás são para indivíduos (pessoas únicas).
Outros crachás são para grupos (a equipe inteira).
As regras permitem que você diga coisas como "O grupo x é o mesmo que o grupo y" ou "O grupo x é um subconjunto do grupo y".

O artigo apresenta dois tipos principais desses cálculos:

1. A Calculadora "Detalhada" (G(L))

Esta versão é muito precisa. Ela usa rótulos complexos que podem representar equipes, suas uniões (mesclando duas equipes) e suas interseções (encontrando a sobreposição entre duas equipes).

Analogia: Isso é como um GPS de alta tecnologia que rastreia cada carro em um congestionamento, suas posções exatas e como eles se fundem ou se dividem em faixas. É matematicamente rigoroso e espelha exatamente como as equipes se comportam no mundo real.
O Problema: Devido ao fato de rastrear tantos detalhes, é difícil dizer se o GPS irá parar de calcular em algum momento (ele pode rodar para sempre).

2. A Calculadora "Terminável" (G*(L))

Para corrigir esse problema de "rodar para sempre", os autores criaram uma versão simplificada.

Analogia: Em vez de rastrear cada movimento de cada carro, este GPS apenas diz: "Temos uma lista de 5 carros. Vamos verificar todas as combinações possíveis desses 5 carros".
O Truque: Eles assumem que existe um número finito de "estados" possíveis (como um número finito de condições climáticas possíveis). Como o número de possibilidades é limitado, a calculadora é garantida de parar depois de um tempo. Ela irá encontrar uma prova (Sucesso!) ou atingir um ponto onde mais nenhuma regra se aplica (Falha/Contra-exemplo).
Por que isso importa: Isso garante que você possa sempre escrever um programa de computador para decidir se uma afirmação é verdadeira ou falsa nessas lógicas.

As Regras Principais do Jogo

O artigo prova que seus cálculos são Sons (Sound) e Completos (Complete):

Sons: Se a calculadora diz "Verdadeiro", é realmente Verdadeiro. (A calculadora não mente).
Completos: Se algo é realmente Verdadeiro, a calculadora pode eventualmente encontrar uma prova para isso. (A calculadora não deixa passar nada).

Eles também provaram que os cálculos possuem regras admissíveis.

Enfraquecimento (Weakening): Você pode adicionar fatos extras e inúteis à sua lista sem quebrar a lógica.
Contração (Contraction): Se você listar o mesmo fato duas vezes, pode tratá-lo como se estivesse listado apenas uma vez.
Corte (Cut): Se você prova que A leva a B, e B leva a C, você pode saltar diretamente para "A leva a C" sem mostrar o passo intermediário.

O Desafio do "Tensor"

Uma das partes mais difíceis deste artigo foi lidar com a Disjunção Tensor (a regra de "divisão").

A Analogia: Imagine que você tem uma equipe de detetives.
- A lógica padrão diz: "A equipe inteira resolve o caso se todos concordarem com a resposta".
- A lógica Tensor diz: "A equipe resolve o caso se pudermos dividir eles em dois grupos, onde o Grupo A resolve parte do caso e o Grupo B resolve o restante".
Os autores tiveram que inventar uma regra especial (chamada regra fin) para lidar com isso. Como eles assumiram que o número de "mundos" (avaliações) é finito, eles puderam dizer: "Cada equipe é apenas uma combinação desses mundos específicos e limitados". Isso permitiu que eles simulassem o comportamento de divisão matematicamente.

Resumo

Em suma, os autores construíram dois conjuntos de livros de regras para resolver enigmas lógicos envolvendo grupos de pessoas (equipes):

Um livro de regras detalhado e matematicamente perfeito que lida com interações complexas de grupos, mas é difícil de automatizar.
Um livro de regras simplificado e com garantia de término, que assume um número limitado de possibilidades, permitindo que computadores verifiquem automaticamente se uma afirmação é verdadeira ou falsa.

Eles provaram que ambos os livros de regras são confiáveis (sons) e cobrem todas as verdades (completos) para as lógicas específicas que estudaram.

Resumo Técnico: Cálculos de Sequentes Rotulados para Lógicas de Equipes Proposicionais

Problema
O artigo aborda os desafios proof-teóricos associados às lógicas proposicionais baseadas em semântica de equipes (team semantics). Embora as propriedades semânticas das lógicas de equipe de fechamento descendente (downward-closed) — especificamente a lógica inquisitiva básica (InqB), a lógica de dependência intuicionista proposicional (PID) e suas extensões com disjunção tensor (InqB $\lor$ e PID $\lor$ ) — sejam bem compreendidas, sua prova-teoria permanece subdesenvolvida. Os sistemas de prova analíticos existentes para essas lógicas, como os cálculos de display multi-tipo ou os cálculos de sequentes de inferência profunda, frequentemente envolvem enriquecimentos estruturais complexos de sequentes de estilo Gentzen. Os autores identificam a necessidade de cálculos de sequentes rotulados modulares que possam lidar com as condições de satisfação específicas da semântica de equipes, particularmente o comportamento da disjunção tensor ( $\lor$ ) e dos átomos de dependência, garantindo propriedades como a admissibilidade do corte (cut-admissibility) e a busca de prova terminável.

Metodologia
Os autores desenvolvem duas famílias de cálculos de sequentes rotulados para as quatro lógicas alvo:

Cálculos Rotulados Gerais ( $G(L)$ ): Estes sistemas utilizam rótulos construídos a partir de conjuntos infinitos de variáveis de equipe ( $S$ para equipes de um elemento, $A$ para equipes arbitrárias) combinados com operações teóricas de conjuntos (união $\cup$ e interseção $\cap$ ). Os rótulos representam equipes arbitrárias, equipes de um elemento e suas combinações. Os cálculos incluem:
- Sequentes Iniciais e Regras Lógicas: Espelham as condições de satisfação definidas na semântica de equipes (ex: regras para $\land$ , $\lor$ , $\to$ e a disjunção tensor).
- Regras de Ordem: Um conjunto de regras que formaliza as propriedades teóricas de conjuntos das equipes (ex: transitividade, união, interseção e a propriedade da equipe vazia).
- Regras Especiais: Uma regra chamada fin é introduzida para lidar com a suposição de que o conjunto de variáveis proposicionais $P$ é finito. Esta regra permite que o sistema descreva qualquer equipe como uma união de $2^{|P|}$ avaliações, o que é crucial para simular a disjunção tensor sobre fórmulas clássicas.
- Modularidade: Os sistemas são projetados de tal forma que os cálculos para PID e PID $\lor$ são obtidos pela adição de regras específicas para átomos de dependência aos cálculos para InqB e InqB $\lor$ .
Cálculos Termináveis ( $G^\star(L)$ ): Para facilitar a busca de prova automatizada, os autores introduzem uma variante simplificada onde os rótulos são definidos como conjuntos finitos de variáveis em vez de termos complexos envolvendo uniões e interseções. Esta abordagem elimina a necessidade de átomos relacionais e regras de ordem, substituindo-os por regras que operam diretamente no conjunto de variáveis em um rótulo.

Contribuições Principais e Resultados

Correção e Completude: Os autores provam que os cálculos gerais $G(L)$ são corretos (sound) e completos em relação às correspondentes semânticas de equipe e axiomatizações de estilo Hilbert. Isso é alcançado demonstrando a admissibilidade de regras estruturais (enfraquecimento, contração, corte) e estabelecendo a admissibilidade de regras derivadas (como mp para modus ponens e flat para a planaridade de fórmulas clássicas).
Admissibilidade do Corte: Um resultado técnico central é a prova da admissibilidade do corte para todos os quatro cálculos. A prova procede por indução sobre o rank da fórmula do corte e a altura da derivação, utilizando uma ordenação lexicográfica que considera tanto a complexidade da fórmula quanto o rótulo.
Busca de Prova Terminável: O artigo apresenta algoritmos de busca de prova termináveis e explícitos para os cálculos simplificados $G^\star(L)$ . O algoritmo constrói uma árvore de busca de prova de baixo para cima (root-first). É provado que ele termina porque o número de fórmulas rotuladas possíveis é finito (dado um conjunto finito de variáveis proposicionais e um conjunto finito de subfórmulas).
Procedimentos de Decisão: A natureza terminável dos cálculos $G^\star(L)$ implica que os problemas de satisfatibilidade e validade para InqB, PID, InqB $\lor$ e PID $\lor$ são decidíveis. Os autores fornecem uma construção de contramodelo a partir de qualquer ramo saturado (aberto) da árvore de busca de prova, garantindo a completude do procedimento de busca.

Significância e Alegações
O artigo alega que sua principal contribuição reside em fornecer os primeiros cálculos de sequentes rotulados corretos e completos para toda a gama de lógicas de equipe proposicionais, incluindo a disjunção tensor e átomos de dependência. Os autores destacam duas vantagens distintas de sua abordagem:

Modularidade: Os sistemas de prova podem ser adaptados para diferentes conjuntos de conectivos ou átomos simplesmente adicionando ou removendo regras, uma característica não presente nos cálculos estruturados mais rígidos encontrados na literatura anterior.
Terminação e Decisão: Ao simplificar a estrutura do rótulo em $G^\star(L)$ , os autores fornecem um procedimento de decisão concreto para estas lógicas, um passo significativo para o raciocínio automatizado em semântica de equipes.

Os autores observam que, embora os cálculos gerais $G(L)$ possam gerar provas mais curtas devido a regras de premissa fixa e à capacidade de raciocinar sobre subconjuntos arbitrários via variáveis, os cálculos simplificados $G^\star(L)$ são essenciais para estabelecer a terminação. O trabalho é restrito a linguagens com finitamente muitos átomos proposicionais, uma condição necessária para a regra fin e para a terminação da busca de prova na presença de disjunção tensor. O artigo conclui identificando trabalhos futuros, incluindo a extensão destes sistemas para linguagens com infinitos átomos e o desenvolvimento de sistemas de prova para outras classes de lógicas de equipe, como aquelas sem implicação intuicionista ou aquelas que possuem a propriedade de fechamento por união.