Positive Instantial Neighbourhood logic

Este artigo introduz a Lógica de Vizinhança Instancial Positiva (PINL), um sistema modal livre de negação com modalidades de caixa e diamante independentes, e estabelece sua completude por meio de semântica de vizinhança persistente, semântica algébrica usando 2-DLIos e uma representação bitopológica canônica.

O essencial

Imagine que você é um detetive tentando entender uma cidade misteriosa chamada Mundo. Nesta cidade, cada pessoa (ou "mundo") tem um Bairro pessoal.

Na lógica tradicional, um detetive poderia perguntar: "Todos neste bairro seguem as regras?" ou "Existe pelo menos uma pessoa aqui que quebrou as regras?".

Este artigo apresenta uma nova maneira, mais detalhada, de investigar esses bairros, chamada Lógica de Vizinhança Instancial Positiva (PINL). Veja como ela funciona, dividida em conceitos simples:

1. A Regra do "Sem Negação" (O Toque Positivo)

Normalmente, os detetives usam "Não" e "Não é o caso" para resolver casos. Por exemplo, "Não é o caso que todos sejam inocentes".
No entanto, este artigo decide banir a palavra "Não". Os detetives só podem dizer o que é verdade, não o que não é.

• A Analogia: Imagine que você está descrevendo uma cesta de frutas. Você pode dizer, "Há uma maçã" ou "Há uma banana". Mas você não pode dizer, "Não há uma laranja". Você só pode descrever o que está realmente presente.
• O Resultado: Como não podem usar o "Não", as duas principais ferramentas do detetive — o Box (que verifica se todos em um grupo fazem algo) e o Diamond (que verifica se alguém em um grupo faz algo) — tornam-se duas ferramentas completamente separadas. Elos não podem mais ser usados para definir um ao outro.

2. As Duas Ferramentas Especiais: O Box e o Diamond

Nesta nova lógica, os detetives usam duas lentes especiais para observar um bairro:

• A Lente Box (□): Esta lente pergunta: "Existe um grupo específico de pessoas neste bairro onde todos seguem a regra principal, e indivíduos específicos também estão presentes para provar que existem?"
  • Exemplo: "Existe um grupo de pessoas onde todos estão usando chapéu (a regra principal) e, especificamente, há uma pessoa alta e uma pessoa baixa nesse grupo?"
• A Lente Diamond (♢): Esta lente pergunta: "É verdade que para cada grupo possível que pudéssemos escolher, ou o grupo é inteiramente composto por pessoas que quebram uma regra específica, OU o grupo contém pelo menos uma pessoa que segue a regra principal?"
  • Exemplo: "Não importa qual grupo de pessoas você escolha, ou eles são todos mentirosos, ou pelo menos um deles está dizendo a verdade."

3. O Problema com o Mapa "Padrão"

Os autores tentaram construir um mapa perfeito (um "modelo canônico") desta cidade usando estas regras. Mas eles encontraram um obstáculo.

• A Falha: No mapa padrão, os bairros são apenas listas não rotuladas de pessoas. Se uma lista de pessoas se encaixa na descrição para a ferramenta "Box", o mapa pode acidentalmente usar essa mesma lista para satisfazer a ferramenta "Diamond", mesmo que não devesse. É como usar uma foto de uma "Pessoa Alta" para provar que uma "Pessoa Baixa" existe apenas porque elas estão na mesma foto.
• A Correção: Para resolver isso, os autores criaram um Mapa Tipado. Em vez de apenas uma lista de pessoas, cada bairro no mapa vem com um Rótulo.
  • A Analogia: Imagine que cada grupo de pessoas na cidade tem uma etiqueta de identificação. Um grupo é rotulado como "Grupo para a Ferramenta Box" e outro é rotulado como "Grupo para a Ferramenta Diamond". Isso evita que o detetive se confunda e use o grupo errado para o trabalho errado.

4. O "Livro de Receitas" Algébrico

O artigo também traduz essas regras lógicas em um "Livro de Receitas" matemático chamado 2-DLIO.

• Pense nisso como um livro de culinária onde os ingredientes são afirmações lógicas.
• O livro tem dois conjuntos de instruções (receitas): um conjunto para os ingredientes do Box e um conjunto para os ingredientes do Diamond.
• Os autores provaram que, se você seguir as regras da sua lógica (PINL), você está essencialmente seguindo as regras deste Livro de Receitas específico. Eles mostraram que a "Álgebra de Lindenbaum" (que é apenas uma forma sofisticada de dizer "a coleção de todas as possíveis receitas lógicas") se encaixa perfeitamente neste livro.

5. O Mapa Final: A Cidade Bitopológica

Finalmente, os autores construíram uma versão grandiosa do mapa da cidade chamada Espaço Bitopológico.

• Este mapa possui duas camadas de geografia:
  1. Uma Camada Positiva (mostrando onde as coisas estão).
  2. Uma Camada Negativa (mostrando onde as coisas não estão, mas descritas sem usar a palavra "Não" — em vez disso, descreve a "contra-teoria" ou a lista de coisas que falharam).
• A Grande Conquista: Eles provaram que o "Livro de Receitas" (a álgebra) e este "Mapa de Cidade de Duas Camadas" (a topologia) são, na verdade, a mesma coisa, apenas vistos de ângulos diferentes. Se você conhece as receitas, pode construir a cidade; e se você olha para a cidade, pode ler as receitas.

Resumo

Este artigo cria uma nova versão "Sem Negação" de um sistema lógico para vizinhanças. Ele resolve um problema complexo onde as duas principais ferramentas (Box e Diamond) se confundem, construindo um mapa rotulado e "tipado". Ele então prova que este sistema lógico é matematicamente sólido ao mostrar que ele corresponde perfeitamente a um tipo específico de livro de receitas algébrico e a um mapa de cidade de duas camadas.

O que o artigo NÃO faz:

• Ele não aplica isso a sistemas de computação reais, diagnósticos médicos ou casos jurídicos.
• Ele não afirma resolver completamente o problema da "dualidade" (ele chama isso de um "primeiro passo" para uma teoria futura).
• Ele não combina as ferramentas Box e Diamond em uma única ferramenta; ele as mantém separadas por enquanto.

Resumo técnico

Resumo Técnico: Lógica de Vizinhança Instancial Positiva (PINL)

Enunciado do Problema
A Lógica de Vizinhança Instancial (INL) é uma linguagem modal para quadros de vizinhança, permitindo que fórmulas expressem não apenas condições de escopo universal, mas também informações existenciais sobre "tipos de mundos" (instâncias) ocorrendo dentro de uma vizinhança. Embora a INL clássica e sua dualidade coalgebraica (envolvendo Álgebras Booleanas com Operadores Instanciais, ou BAIOs) sejam bem desenvolvidas, existe uma lacuna na literatura em relação a uma versão positiva (livre de negação) sistemática desta lógica.

A ausência de negação clássica na lógica positiva impede a interdefinibilidade dos operadores caixa ($\Box$) e diamante ($\Diamond$). Consequentemente, uma versão positiva da INL não pode ser tratada meramente como um fragmento da INL clássica; ela requer um sistema de prova distinto, uma semântica de vizinhança positiva adequada, uma semântica algébrica baseada em reticulados distributivos e uma representação canônica. O artigo aborda a falta desses componentes fundamentais para uma lógica de vizinhança instancial positiva e de dois lados.

Metodologia
Os autores desenvolvem a lógica, denominada Lógica de Vizinhança Instancial Positiva (PINL), através de uma abordagem multifacetada combinando teoria de provas, teoria dos modelos, álgebra e topologia:

1. Sintaxe e Sistema de Prova: A linguagem da PINL é construída sobre uma base proposicional de reticulados distributivos limitados (usando $\top, \bot, \land, \lor$) em vez da lógica proposicional clássica. Ela introduz dois operadores instanciais primitivos e independentes: um do tipo caixa $\Box(\phi_1, \dots, \phi_n; \psi)$ e um do tipo diamante $\Diamond(\phi_1, \dots, \phi_n; \psi)$. Um sistema de prova baseado em sequentes é formulado com axiomas para reticulados distributivos limitados e axiomas modais específicos para $\Box$ e $\Diamond$ que refletem sua natureza independente.
2. Semântica (Modelos de Dois Lados Persistentes): A lógica é interpretada sobre modelos de vizinhança de dois lados persistentes. Estas estruturas consistem em um conjunto parcialmente ordenado $(W, \leq)$ e duas funções de vizinhança, $N_\Box$ e $N_\Diamond$, que mapeiam mundos para conjuntos de aumentos (upsets). Crucialmente, $N_\Box$ é monótona ascendente (preservando a ordem), enquanto $N_\Diamond$ é monótona descendente. A verdade é definida via condições de testemunho (witness) para $\Box$ (existência de uma vizinhança satisfazendo as fórmulas de escopo e instância) e condições de co-testemunho (co-witness) para $\Diamond$ (satisfação universal de uma disjunção de condições).
3. Construção Canônica e Semântica Tipada: Uma prova de completude canônica direta para a semântica persistente padrão é obstruída pela natureza extensional das vizinhanças (aumentos não rotulados podem acidentalmente testemunhar múltiplas fórmulas). Para superar isso, os autores introduzem uma semântica de vizinhança persistente tipada auxiliar. Neste cenário, as vizinhanças são rotuladas pelo tipo de fórmula modal específica que pretendem testemunhar ou refutar. Um modelo é construído a partir de pares de teorias primas $(a_1, a_2)$, onde $a_1$ é uma teoria e $a_2$ é uma contra-teoria. Um Lema de Verdade é estabelecido para este modelo tipado, provando que a verdade semântica coincide com a membresia no componente positivo do par primo.
4. Semântica Algébrica (2-DLIOs): O artigo introduz 2-DLIOs (reticulados distributivos limitados equipados com duas famílias de operações instanciais, $(f_n)$ para $\Box$ e $(g_n)$ para $\Diamond$) como o correspondente algébrico. Mostra-se que o álgebra de Lindenbaum da PINL é uma 2-DLIO.
5. Representação Bitopológica: Os autores constroem um espaço PINL bitopológico canônico derivado dos pares de teorias primas. Este espaço é equipado com duas topologias ($\tau_+$ gerada por conjuntos de membresia positiva $U_\phi$ e $\tau_-$ gerada por conjuntos de membresia negativa $V_\phi$). Demonstra-se que a álgebra dos abertos positivos admissíveis neste espaço é isomórfica ao 2-DLIO de Lindenbaum.

Contribuições Principais e Resultados

• Sistema Formal: Definição da linguagem e de um sistema de prova completo para a PINL, tratando $\Box$ e $\Diamond$ como primitivos independentes com esquemas de axiomas distintos.
• Completude: Prova de correção e completude da PINL em relação aos modelos de vizinhança de dois lados persistentes. Isto é alcançado através da semântica tipada auxiliar, que resolve as dificuldades técnicas da construção canônica na ausência de negação.
• Caracterização Algébrica: Introdução de 2-DLIOs como a semântica algébrica para a PINL. O artigo prova a correção e completude algébrica, demonstrando que a álgebra de Lindenbaum da PINL é uma 2-DLIO.
• Representação Canônica: Construção do espaço bitopológico canônico da PINL. O artigo prova que a álgebra dos abertos positivos admissíveis deste espaço é isomórfica ao 2-DLIO de Lindenbaum. Isto fornece uma representação canônica de abertos admissíveis para a lógica.
• Separação de Preocupações: O trabalho isola explicitamente o fragmento positivo e de operadores independentes da INL, distinguindo-o do framework booleano clássico e do framework completo de DLIO onde axiomas de interação podem existir.

Significância e Escopo
O artigo afirma fornecer o primeiro desenvolvimento sistemático de uma versão positiva e livre de negação da lógica de vizinhança instancial. Ele preenche uma lacuna específica na literatura ao estabelecer o sistema de prova, a semântica e os fundamentos algébricos para esta lógica.

Os autores declaram explicitamente que o escopo é limitado a um teorema de representação canônica, e não a um teorema de dualidade categórica completo. Embora o trabalho sente as bases para uma futura teoria de dualidade (especificamente uma dualidade do tipo Priestley ou bitopológica para 2-DLIOs), o presente artigo não define a categoria necessária de espaços PINL descritivos, morfismos ou tratamentos funcionais. Da mesma forma, o artigo observa que uma versão "geométrica" da INL (envolvendo continuidade de Scott) é sugerida pela literatura, mas é deixada para trabalhos futuros.

A significância reside em unir a lógica modal positiva, a semântica de vizinhança e a teoria de reticulados distributivos, oferecendo um framework rigoroso para raciocinar sobre propriedades instanciais sem negação clássica, e fornecendo as ferramentas algébricas e topológicas necessárias para futuras pesquisas de dualidade.